Give an equational proof of $ \vdash (\forall x)(A \rightarrow B) \equiv ((\exists x) A) \rightarrow B$
I tried and used ping pong theorem to split it into two implications to prove
$$ \vdash (\forall x)(A \rightarrow B) \rightarrow (((\exists x)A) \rightarrow B)$$
and
$$ \vdash (((\exists x)A) \rightarrow B) \rightarrow (\forall x)(A \rightarrow B) $$
But still couldn't figure it out.
Lists of axioms and theorems.
On
It is all to horrible, dare your lecturer to prove it himself.
Equational proofs are more complex than Hilbert style (modus ponens only proofs)
Hilbert style (modus ponens only proofs) are more complex than the normal natural deduction proofs.
And in Natural deduction the proof goes as follows:
I presume that there is no x free in B and for sanity's sake I will use Ax to indicate that A can contain x.
At is just shorthand for A(x:=t) , Au for A(x:=u), Vx stands for $\forall x$ and Ex for $\exists x$
1. | |______ (Vx)(Ax -> B) Assumption for conditional proof
2. | | |____ (Ex)AX Assumption for conditional proof
3. | | | |_t At Assumption for existentional elimination proof
4. | | | | At -> B 1 Universal elimination
5. | | | | B 3,4 modus ponens
.. | | | <------------------------------------------ end of sub proof
6. | | | B 2,3-5 existentional elimination
.. | | <------------------------------------------- end of sub proof
7. | | ((Ex)AX) -> B 2-6 conditional proof
.. | <---------------------------------------------- end of sub proof
8. | ((Vx)(Ax -> B)) -> ((Ex)AX) -> B ) 1-7 conditional proof
9. | |______ ((Ex)AX) -> B ) Assumption for conditional proof
10 | | |___u variable for universal introduction
11 | | | |__ Au Assumption conditional proof
12 | | | | (Ex)AX 11 existentional introduction
13 | | | | B 9,11 modus ponens
.. | | | <------------------------------------------ end of sub proof
14 | | | At -> B 11-13 conditional proof
.. | | <-------------------------------------------- end of sub proof
15 | | (Vx)(Ax -> B) 10-14 Universal introduction
.. | <---------------------------------------------- end of sub proof
16 | ((Ex)AX) -> B ) -> ((Vx)(Ax -> B)) 9-15 conditional proof
17 | ((Vx)(Ax -> B)) <-> ((Ex)AX) -> B ) 8,16 Equivalence introduction
But this is an natural deduction proof.
And you are asked to transform it in an equational proof?
I could tell you to first transform the proof above into an Hilbert style (modus ponens only) proof and then transform that in an equational proof.
but that would even be to hard for me so to be honnest I don't give you a 5% chance to succeed.
Just dare your lecturer to do it.
If he manages it, publish the proof here, (then I can also learn from it) and if he fails, (what I would not find improbable) he should never have asked you.
All the best.
(Like the other answer, I will assume that $\;x\;$ is not free in $\;B\;$. Otherwise this is not a theorem: take for example $\;A := x > 2\;$ and $\;B := x > 0\;$, which leads to a statement that is false for $\;x \le 0\;$.)
(I will use a slightly different quantification notation, to save on parentheses.)
If you only want to use the axioms and theorems from the photos you provided, then you seem to be missing something: there is no axiom about $\;\exists\;$. So I will assume you are allowed to use, e.g., the following definition the of $\;\exists\;$: $$ \tag{0} \langle \exists x :: A \rangle \;\equiv\; \lnot \langle \forall x :: \lnot A \rangle $$
Using $(0)$, the proof is simply as follows:
\begin{align} & \langle \forall x :: A \to B \rangle \\ \equiv & \qquad \text{"by (2.4.11) -- working towards (6.4.2),} \\ & \qquad \phantom{\text{"}}\text{which seems the key rule to use here"} \\ & \langle \forall x :: \lnot A \lor B \rangle \\ \equiv & \qquad \text{"by symmetry (6) -- still towards (6.4.2)"} \\ & \langle \forall x :: B \lor \lnot A \rangle \\ \equiv & \qquad \text{"by (6.4.2), using the assumption that $\;x\;$ is not free in $\;B\;$"} \\ & B \lor \langle \forall x :: \lnot A \rangle \\ \equiv & \qquad \text{"introduce double negation (2.4.4)} \\ & \qquad \phantom{\text{"}}\text{-- to match the RHS of (0): we work towards $\;\exists\;$"} \\ & B \lor \lnot \lnot \langle \forall x :: \lnot A \rangle \\ \equiv & \qquad \text{"by duality (0)"} \\ & B \lor \lnot \langle \exists x :: A \rangle \\ \equiv & \qquad \text{"by symmetry (6) -- to reintroduce $\;\to\;$"} \\ & \lnot \langle \exists x :: A \rangle \lor B \\ \equiv & \qquad \text{"reintroduce $\;\to\;$ by (2.4.11)"} \\ & \langle \exists x :: A \rangle \to B \\ \end{align}
which completes this proof.
(To make this formally complete, we must of course use symmetry $(2)$, Leibniz $(2.1.16)$ and $(6.1.11)$, and transitivity $(1.4.13(c))$ many times, but fortunately that is implicit in the above proof format designed by Edsger W. Dijkstra and Wim Feijen. See EWD1300 for more details.)