How to properly write long logical formulas?

I need to write many mathematical statements written as first order logical formulas. Usually I can't have them on a single line because they tend to be too long. The following one is an example of what I managed to accomplish:

\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) \\
\end{split}
\end{gather}


I'm not very happy with the result, mainly because of the qquads and the ampersands. I cannot use the itemize environment because five levels of nesting is too much for LaTeX. Also, the itemize environment would force me to add the displaystyle command in front of every formula.

So, it there a better way to achieve this?

The above formula renders as

• I would say to use the {tabbing} environment except that you still have to specify math mode in each row. Still, look into it. – Ryan Reich Nov 17 '10 at 11:51
• This is very much like a style that Leslie Lamport advocated for long formulae, but with scaleable logical operators (and, or) at the left. I'll look to see if he's published any Latex code for doing that. – Charles Stewart Nov 17 '10 at 12:11

Leslie Lamport advocated a similar way of breaking the lines, but with placing vees and wedges at the left, giving a sideways tree was to form larger formulae from groups of smaller formulae. He describes this system in How to Write a Long Formula, as part of his TLA (teomporal logic of actions) specification language, together with a Latex style. The style files are supposed to be at his Latex page, but that link comes up blank for me.

Use an array with some adjustments: \> tells to advance by 2em from now on, \< causes going back 2em.

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

\newdimen\longformulasindent
\newenvironment{longformulas}
{\global\longformulasindent=0pt
$$\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}$$