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.

  • $\begingroup$ 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.) $\endgroup$
    – Ken
    Jul 15, 2015 at 16:10

2 Answers 2


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.