How to properly write long logical formulas?

Question

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) \\
 & \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}

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? Thanks.

Addition

The above formula renders as

Answer 1

Leslia 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.