1
$\begingroup$

First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms:

  • Tautologies

  • $\forall x \alpha \rightarrow \alpha_t^x$, where $t$ is substitutable for $x$ in $\alpha$.

  • $\forall x (\alpha \rightarrow \beta)\rightarrow(\forall x \alpha \rightarrow \forall x \beta)$

  • $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$

And if the language includes equality,

  • $x=x$
  • $x=y \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in zero or more places by $y$.

The problem is $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$. I'm really stuck on this problem. I mean, intuitively it makes sense ... $Py$ doesn't rely on $x$ and we know that there is an $x$ that satisfies $Qx$... thus it is intuitively obvious that $\exists x (Py \land Qx)$. The thing is, I can't figure out a sequence of deductions to arrive there (formally). Can somebody give me a hand? I've been staring at this problem for too long now.

$\endgroup$
  • 1
    $\begingroup$ Is $\exists$ short for something? There no axioms which include $\exists$. $\endgroup$ – Git Gud Nov 18 '14 at 1:21
  • $\begingroup$ Yes $\exists x$ is short for $\neg \forall x \neg$ $\endgroup$ – Bobby Lee Nov 18 '14 at 3:19
2
$\begingroup$

In your comment there is the key to the solution : $\exists x$ in Enderton's proof system is an abbreviation for $\lnot \forall \lnot$.

1) $Py∧∃xQx$ --- assumed

2) $Py \land \lnot \forall x \lnot Qx$ --- abbreviation

3) $\lnot (Py \rightarrow \forall x \lnot Qx)$ --- with the tautology : $(\alpha \land \lnot \beta) \leftrightarrow \lnot (\alpha \rightarrow \beta)$

4) $\lnot \forall x(Py \rightarrow \lnot Qx)$ --- by EXAMPLE (Q2A) [page 121] : if $x$ does not occur free in $\alpha$, then $\vdash (α → ∀xβ) ↔ ∀x(α → β)$ : $x$ is not free in $Py$.

5) $\exists x \lnot (Py \rightarrow \lnot Qx)$ --- by abbreviation

6) $\exists x (Py \land Qx)$ --- with the tautology : $(\alpha \land \beta) \leftrightarrow \lnot (\alpha \rightarrow \lnot \beta)$

7) $\vdash Py∧∃xQx → ∃x(Py∧Qx)$ --- by Deduction Theorem.

$\endgroup$

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.