How do I make proofs with long formulae more readable without sacrificing clarity?

Question

A lot of things I'm trying to prove just now are turning into "notational hell", which I think makes them very hard to read. I've tried to cut down on this by assuming my reader will understand what definitions are in play, modularising my proofs and skipping explanation of steps that I hope are obvious. I've also tried relabeling formulae with short names (i.e., $\def\val#1{V_\pli(#1)}\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\def\pli{\mathscr{I}}\def\aa{\p_1,\,\p_2,\,\ldots,\,\p_n\s\q}\def\ab{\p_1,\,\p_2,\,\ldots,\,\p_n\ns\q}\def\ba{\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\def\bb{\ns\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots)):=\,\s Q),$ but for proofs of any length it seems to be more confusing than helpful. How do I make proofs more readable without sacrificing clarity?

Example Proof

Let $\p$ and $\q$ be wffs and $n\in\mathbb{N}$ (please note that $0\not\in\mathbb{N}$). We want to show $\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q$ iff $\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))$.

In (L1) I prove both directions of the biconditional, which I don't think I need to do because we're dealing with "=" - is this correct? I also think that (L1) is so basic that "by inspection" is appropriate - is that fair?

Lemma 1 (L1)

We want to show by induction that for some PL-interpretation, $\pli,$ $\val{\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$ iff $\val{\p_n}=\val{\p_{n-1}}=\cdots=\val{\p_1}=1$ and $\val{\q}=0$.

Base Case

• If $\val{\p\to\q}=0$ then, by definition, $\val{\p}=1$ and $\val{\q}=0$. If $\val{\p}=1$ and $\val{\q}=0$, then, by definition, $\val{\p\to\q}=0$

Induction Hypothesis (IH)

• Assume for some arbitrary $k\in\mathbb{N}$ that $\val{p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$ and $\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1$ and $\val{\q}=0$

Induction Step

• If $\val{\p_{k+1}\to(p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots)))}=0,$ then, as we know $\val{p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$ from the (IH), $\val{\p_{k+1}}=1$. From the (IH) $\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1$ and $\val{\q}=0$, thus $\val{\p_{k+1}}=\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1$ and $\val{\q}=0$

• Let $\val{\p_{k+1}}=1$. From the (IH) $\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1,$ $\val{\q}=0,$ and $\val{p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0,$ thus $\val{\p_{k+1}\to(p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots)))}=0$

Proof of First Direction (P1)

1. For reductio, suppose it is not the case that $\aa\implies\ba$

2. It follows from (1) that there exists an $\def\pli{\mathscr{I}}\pli$ such that $\def\aa{\p_1,\,\p_2,\,\ldots,\,\p_n\s\q}\def\ab{\p_1,\,\p_2,\,\ldots,\,\p_n\ns\q}\def\ba{\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\def\bb{\ns\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\aa$ and $\bb$

3. It follows from (2) that $\def\val#1{V_\pli(#1)}\val{\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$

4. From (L1), the valuation on (3) can only occur when $\val{\p_n}=\val{\p_{n-1}}=\cdots=\val{\p_1}=1$ and $\val{\q}=0$

5. It follows from (4) that $\ab$, which contradicts (2) and proves our first direction

Proof of Second Direction (P2)

1. For reductio, suppose it's not the case that $\ba\implies\aa$

2. It follows from (1) that there exists an $\pli$ such that $\ba\text{ and }\ab$

3. From (2) we have $\ab$, thus, $\val{\p_n}=\val{\p_{n-1}}=\cdots=\val{\p_1}=1$ and $\val{\q}=0$

4. It follows from (3) and (L1) that $\bb\text{,}$ which contradicts (2) and proves our second direction

(P1) and (P2) prove both directions of the biconditional, hence $\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q$ iff $\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))\,\square.$

Main suggestion

Instead of

We want to show $\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q$ iff $\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))$

try it like this:

We want to show that $$\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q \tag{1}$$ if and only if $$\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots)).\tag{2}$$

After that, instead of repeating the long formulas every time, just call them $(1)$ and $(2)$:

For reductio, suppose it's not the case that $(2)\implies (1)$. Then there must exist an $\mathscr I$ such that $(2)$ holds but $(1)$ does not.

Lesser suggestions

1. Abbreviate $$\phi_n\to(\phi_{n-1}\to(\cdots\to(\phi_1\to\q)\cdots))$$ as $$\Phi_n.$$ (Don't use $Q$. Why would you use $Q$?)

   Instead of $$V_\mathscr{I}({p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))})=0$$ you can now write $$V_\mathscr{I}({p_k\to\Phi_{k-1}})=0$$ and the reader won't miss that the first variable is a $p$ and not a $\phi$.

   You said abbreviating seems “more confusing than helpful”. It's not.

2. Abbreviate $\phi_1,\phi_2,\ldots,\phi_n$ as $\vec\phi$.

3. Abbreviate $$V_\mathscr{I}(\phi_n)=V_\mathscr{I}(\phi_{n-1})=\cdots=V_\mathscr{I}(\phi_1)=1$$ as $$V_\mathscr{I}(\phi_i) = 1\quad (i=1\ldots n)$$ or perhaps $$V_\mathscr{I}(\phi_{1\ldots n}) = 1.$$

4. You're abbreviating the wrong things. You don't need to abbreviate “if and only if” as “iff”, or “Lemma 1” as “L1”. The goal here is not to remove all the normal English from your proof. These abbreviations are more confusing than helpful.

Don't make the reader compare two long formulas to make sure they are the same, or to wonder why they are not. Design your notation to highlight the differences between similar formulas.

Notation, like language, is flexible. There are no rules; you are allowed to make things up. $\vec\phi$ is not really a vector. It doesn't matter. You can explain it briefly: “We will abbreviate $\phi_1,\phi_2,\ldots,\phi_n$ as $\vec\phi$.” Nobody will be confused or forget what it means. My suggestion $V_\mathscr{I}(\phi_{1\ldots n})$ is not standard. It doesn't matter; the meaning is clear.

Orthogonal suggestions

1. You're not using TeX correctly. You don't need to keep repeating \defs. Once you \def a new control sequence, the definition remains in force until the end of the group, or the document. Define the important macros once, at the beginning of the file, or in an \included file.

2. Define better macros. The structure of the macros should follow the syntactic structure of your formulas. Instead of typing out

   \def\aa{\p_1,\,\p_2,\,\ldots,\,\p_n\s\q}
   \def\ab{\p_1,\,\p_2,\,\ldots,\,\p_n\ns\q}
   \def\ba{\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}  
   \def\bb{\ns\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))
   

   try it this way:

   \def\ps{\p_1,\,\p_2,\,\ldots,\,\p_n}
   \def\aa{\ps\s\psi}
   \def\ab{\ps\ns\psi}
   \def\pformn{\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\psi)\cdots))}
   % now you don't need \ba or \bb, just use \s\pformn and \ns\pformn