First order logic proof question

Question

I have no idea how to begin constructing this proof, and I would appreciate any help!

I need to prove the following, and to make matters worse, without soundness or completness:

$$ \vdash (\forall x. \phi) \rightarrow (\exists x.\phi)$$

I can use the following axioms/theorems:

Ax1 $\langle \forall^\ast (\varphi \rightarrow (\psi \rightarrow \varphi)) \rangle$;

Ax2 $\langle \forall^∗ ((\varphi \rightarrow (\psi \rightarrow \eta)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \eta))) \rangle$;

Ax3 $\langle \forall^∗ (((\neg \varphi) \rightarrow (\neg \psi)) \rightarrow (\psi \rightarrow \varphi)) \rangle$;

Ax4 $\langle \forall^\ast (\forall x.(\varphi \rightarrow \psi)) \rightarrow ((\forall x. \varphi) \rightarrow (\forall x. \psi)) \rangle$;

Ax5 $\langle \forall^\ast (\forall x. \varphi) \rightarrow \varphi^x_t \rangle$ for $t \in \rm{TS}$ a term;

Ax6 $\langle \forall^\ast (\varphi \rightarrow \forall x.\varphi) \rangle$ for $x \notin \operatorname{FV}(\varphi)$; and

MP $\langle \varphi, (\varphi \rightarrow \psi), \psi \rangle$.

and the lemma "Let $\Sigma \vdash \varphi$ and $x \notin \operatorname{FV}(\Sigma)$. Then $\Sigma \vdash \forall x. \varphi$."

Thank you.

---

EDIT [SN]: The original question did not mention the lemma in the final line. I added it based on another question that otherwise is an exact duplicate of this.

Answer 1

As I mention in my answer to the other question, if your axioms are all sentences (so that the universal quantifiers quantify over all variables that appear) and if there are no constant symbols in your language, then it is impossible to make the deduction, since the axioms are all true in the empty structure and the rule of inference is valid for this structure, but the desired deduction is not valid in the empty structure.

So let me assume that that you do not intend that the axioms are fully universally quantified, and the comments in the other question suggest this reading.

Let me first give a deduction in a modified system, where we modify axiom 3 to assert $\langle \forall^∗ ((\varphi \rightarrow (\neg \psi)) \rightarrow (\psi \rightarrow \neg\varphi)) \rangle$, which is similar and simply places the negations in slightly different spots. With this modified axiom, one can make the deduction as follows:

• $\forall x.\varphi(x)$. Assume by hypothesis.
• $[\forall x.\varphi(x)]\to \varphi(t)$, using any fixed term $t$. By axiom 5.
• $\varphi(t)$. By modus ponens.
• $[\forall x.\neg\varphi(x)]\to \neg\varphi(t)$. By axiom 5.
• $[[\forall x.\neg\varphi(x)]\to \neg\varphi(t)]\to [\varphi(t)\to \neg\forall x.\neg\varphi(x)]$. This is an instance of the modified axiom 3.
• $\varphi(t)\to \neg\forall x.\neg\varphi(x)$. By modus ponens.
• $\neg\forall x.\neg\varphi(x)$. By modus ponens.
• $\exists x.\varphi(x)$. By definition of $\exists$.

Thus, we've got $\forall x.\varphi(x)\vdash\exists x.\varphi(x)$, and so by the deduction theorem, $\vdash\forall x.\varphi(x)\to\exists x.\varphi(x)$, as desired.

Now, instead of modifying axiom 3, one can deduce it, if one knows that $\vdash\neg\neg\varphi\to\varphi$. The reason is that to show $A\to\neg B\vdash B\to\neg A$, it suffices to show $A\to\neg B,B\vdash\neg A$, but one has $\vdash(\neg\neg A\to \neg B)\to(B\to \neg A)$ by the original axiom 3, and so now use the fact that $\vdash\neg\neg A\to A$ to get it in a few steps.

Of course, we certainly want $\vdash\neg\neg\varphi\to\varphi$ to be the case, but I confess that looking at it briefly just now I don't see immediately how to do it in the system you have specified. One could simply add it as an axiom, but perhaps there is a clever way to deduce it.

Answer 2

The theorem is already valid in minimal logic. Means neither ~ ~ A -> A nor something equivalent (for example Ax3 in the post) that stands between minimal logic and classical logic is needed. Here is a proof in minimal logic, I am using A -> f for ~A.

 1) A(y) |- A(y) (Id)

 2) f |- f (Id)

 3) A(y) , A(y) -> f |- f (Left -> 1+2)

 4) A(y), forall x(A(x) -> f) |- f (Left forall 3)

 5) forall x A(x), forall x (A(x) -> f) |- f (Left forall 4)

 6) forall x A(x) |- forall x (A(x) -> f) -> f (Right -> 5)

 7) |- forall x A(x) -> (forall x (A(x) -> f) -> f) (Right -> 6)

The above is a Gentzen proof. But the poster gave a Hilbert style calculus. We can turn the above proof into a Hilbert style proof with the axioms of the poster. I guess it will be a bit longer than the Genzten proof. But it will not make use of Ax3.

Best Regards