如何正确书写长逻辑公式？

Question

我需要编写许多以一阶逻辑公式形式编写的数学语句。通常我不能将它们放在一行中，因为它们往往太长了。以下是我设法完成的示例：

\begin{gather}
\begin{split}
 & \forall G\left(\phi_1\leftrightarrow\phi_2\right) \\
 & \qquad G\text{ is a group} \\
 & \qquad \exists G_0\exists\mathord{*}\exists e\left(\bigwedge_{i=3}^7\phi_i\right) \\
 & \qquad\qquad G=\left(G_0,\mathord{*}\right) \\
 & \qquad\qquad \mathord{*}:G_0\times G_0\rightarrow G_0 \\
 & \qquad\qquad \mathord{*}\text{ is associative} \\
 & \qquad\qquad e\text{ is the identity of }\mathord{*} \\
 & \qquad\qquad \forall g\left(\phi_8\rightarrow\phi_9\right) \\
 & \qquad\qquad\qquad g\in G_0 \\
 & \qquad\qquad\qquad \exists g'\left(\phi_{10}\land\phi_{11}\right) \\
 & \qquad\qquad\qquad\qquad g'\in G_0 \\
 & \qquad\qquad\qquad\qquad g'\text{ is the inverse of }g\text{ with respect to }\mathord{*} \\
\end{split}
\end{gather}

我对结果不太满意，主要是因为 qquad 和 & 符号。我无法使用 itemize 环境，因为五层嵌套对于 LaTeX 来说太多了。此外，itemize 环境会迫使我在每个公式前面添加 displaystyle 命令。

那么，有没有更好的方法来实现这一点？

上述公式表示为

Answer 1

Leslie Lamport 提倡一种类似的打破线条的方式，但将 V 形和楔形放在左侧，形成一棵横向的树，以便从一组较小的公式中形成更大的公式。他在如何编写长公式，作为其 TLA（动作时间逻辑）规范语言的一部分，以及 Latex 样式。样式文件应该位于他的 Latex 页面，但对于我来说该链接是空白的。

Answer 2

使用array一些调整：\>告诉从现在开始前进 2em，\<导致后退 2em。

\documentclass{article}
\usepackage{amsmath}
\usepackage{array}

\newdimen\longformulasindent
\newenvironment{longformulas}
 {\global\longformulasindent=0pt
  \def\>{\global\advance\longformulasindent2em\relax\hspace{2em}}%
  \def\<{\global\advance\longformulasindent-2em\relax\hspace{-2em}}%
  \renewcommand{\arraystretch}{1.2}% some more room
  \begin{array}{@{}>{\displaystyle\hspace{\longformulasindent}}l@{}}}
 {\end{array}}

\begin{document}

\begin{equation}
\begin{longformulas}
\forall G\left(\phi_1\leftrightarrow\phi_2\right) \\
\> G\text{ is a group} \\
   \exists G_0\exists\mathord{*}\exists e\biggl(\,\bigwedge_{i=3}^7\phi_i\biggr) \\
   \> G=\left(G_0,\mathord{*}\right) \\
      \mathord{*}:G_0\times G_0\rightarrow G_0 \\
      \mathord{*}\text{ is associative} \\
      e\text{ is the identity of }\mathord{*} \\
      \forall g\left(\phi_8\rightarrow\phi_9\right) \\
      \> g\in G_0 \\
          \exists g'\left(\phi_{10}\land\phi_{11}\right) \\
          \> g'\in G_0 \\
             g'\text{ is the inverse of }g\text{ with respect to }\mathord{*} \\
      \< \text{we can even go back} \\
   \< \text{we can even go back} \\
      \> \text{and in again} \\
\end{longformulas}
\end{equation}

\end{document}