Logical equivalence of a given formula

Is it true that
a(x)⇒∀yφ(x,y)≡∀y(a(x)⇒φ(x,y)),
a(x) \Rightarrow \forall{y} \varphi(x,y) \equiv \forall{y} \left( a(x) \Rightarrow \varphi(x,y) \right),

where a(x)a(x) is a quantifier free formula with only one free variable xx and φ(x,y)\varphi(x,y) is a quantifier free formula with free variables x,yx,y ?

In my opinion it’s true, but I need to clarify this fact.

=================

=================

2 Answers
2

=================

Suppose the one on the left is false. Then we have an mm such that a(m)a(m) while ¬ϕ(m,n)\neg\phi(m,n) for some nn, making a(m)→ϕ(m,n)a(m) \to \phi(m,n) false, and thus also ∀y(a(m)→ϕ(m,y)\forall y (a(m) \to \phi(m,y) and also ∀y(a(x)→ϕ(x,y)\forall y (a(x) \to \phi(x,y) – the one on the right – false.

Now do the same thing for the case where the one on the left is true, and show that the one on the right also is, proving the biconditional.

Check out this page on Wiki, on the section “Implication” under “converting to prenex normal form”.

a(x)⟹∀y φ(x,y)≡¬a(x)∨∀y φ(x,y)≡∀y (¬a(x)∨φ(x,y)≡∀y (a(x)⟹φ(x,y))\begin{align}
a(x) \implies \forall y~ \varphi(x, y)
&\equiv \lnot a(x) \lor \forall y~ \varphi(x, y) \\
&\equiv \forall y~ (\lnot a(x) \lor \varphi(x, y) \\
&\equiv \forall y~ (a(x) \implies \varphi(x, y))
\end{align}

Using B∨∀yA(y)≡∀y B∨A(y)B \lor \forall y A(y) \equiv \forall y ~ B \lor A(y) which is the generalization of B∨(A(0)∧A(1)∧A(2)…)≡(B∨A(0))∧(B∨A(1))∧(B∨A(2))…B \lor (A(0) \land A(1) \land A(2) \dots) \equiv (B \lor A(0)) \land (B \lor A(1)) \land (B \lor A(2)) \dots