# Distribution of universal quantifier with free variables.

My question is regarding the validity of the following statement:

$$(\forall a (\phi \implies \psi)) \equiv (\phi \implies \forall a \psi ),$$

provided, of course, there are no free occurrences of $a$ in $\phi$.

I am using the axiom system from Hughes and Cresswell, namely,

(US) $\forall a \phi \implies \phi [a / b]$ (N.B. $\phi[a/b]$ denotes a bound alphabet variant of $\phi$ with no bound $b$, then replacing every free $a$ with free $b$).

(UG) From $\phi \implies \psi$ infer $\phi \implies \forall a \psi$, provided $a$ is not free in $\phi$.

(MP) Modus Ponens.

I also have some modal axioms in play but I assume they are irrelevant. In the book they list as a theorem:

$$(\forall a (\phi \implies \psi)) \implies (\phi \implies \forall a \psi ),$$

provided there are no free occurrences of $a$ in $\phi$. (Which is clearly a straightforward application of (1)+MP and then (2).) I believe the other direction should follow from a rather similar argument, but seeing as the book did not list such a equivalence as a theorem, but merely a one sided implication, I am second guessing myself. Anyway, a sketch:

$$(\phi \implies \forall a \psi ) \quad [1: Assumption]$$ $$(\forall a \psi \implies \psi[a/a] )\quad [2: US]$$ $$(\phi \implies \psi[a/a]) \quad [3: 1+2+MP]$$ $$(\phi \implies \forall a \psi ) \implies (\phi \implies \psi[a/a]) \quad [4: 1+3]$$ $$\forall a(\phi \implies \psi[a/a]) \quad [5: 4+UG]$$

Then since bound alphabetic variants are material equivalents, this delivers the result. Now, I'm a bit new to the whole logic thing so any errors or omissions would be very helpful.

• I'm not familiar with Hughes and Cresswell directly, but the other direction certainly follows if $a$ does not appear anywhere in $\phi$. (It's not enough to suppose there are no free occurrences of $a$ in $\phi$, since $\phi$ could itself contain $\forall a [...]$, and one shouldn't requantify on the same variable.)
– Ken
Jul 15, 2015 at 16:10

My sequences of transformation is as follow:

$$\forall a (\phi \Rightarrow \psi)$$

$$\equiv~ \forall a (\neg\phi \vee \psi)$$ $$\equiv~ \neg\phi \vee \forall a (\psi)$$ $$\equiv~ \phi \Rightarrow \forall a (\psi)$$

Note that from step 2 to 3, since $a$ does not occur free in $\phi$, hence $\forall a (\neg\phi \vee \psi) ~~ \equiv ~~ \neg\phi \vee \forall a (\psi)$.

There is no error in your sketch. My only remark is that in step 5, I would also indicate that MP is used, $[5:4+UG+MP]$ and then from 1 and 5 you get the reversed implication.