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.

  • 3
    $\begingroup$ Not one of those axioms/theorems even mentions $\exists$, so what can you use about $\exists$? $\endgroup$ – Gerry Myerson Nov 16 '11 at 2:35
  • 2
    $\begingroup$ What is your definition of $\exists x.\phi$? $\lnot(\forall x.\lnot\phi)$? As Gerry pointed out, your axioms/theorems don’t mention $\exists$, so you’ll have to begin by replacing it by its definition in your system. $\endgroup$ – Brian M. Scott Nov 16 '11 at 13:00
  • 2
    $\begingroup$ Note: This is question 3 of this assignment. $\endgroup$ – hmakholm left over Monica Nov 16 '11 at 23:12

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.

  • $\begingroup$ @Badwolf23: Because the inference system above does not have the usual rules of negation introduction and elimination (as written in Wikipedia, for example), I doubt that double negation elimination may be deduced. $\endgroup$ – beroal Nov 18 '11 at 16:16
  • $\begingroup$ Beroal, I am inclined to agree. In that case, of course, the proof system would be defective. $\endgroup$ – JDH Nov 22 '11 at 13:43

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


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.