4
$\begingroup$

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.

  • 2
    Not one of those axioms/theorems even mentions $\exists$, so what can you use about $\exists$?2011-11-16
  • 2
    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.2011-11-16
  • 2
    Note: This is question 3 of [this assignment](http://www.student.cs.uwaterloo.ca/~cs245/assign4.pdf).2011-11-16

2 Answers 2