1
$\begingroup$

I am trying to prove $\exists x(P\lor Q)\vdash \exists x P \lor \exists x Q$, so I have: $$\begin{array}{r l l} (1) ~&~~ \exists x (P \lor Q) ~&~ \mbox{[premise]} \\ (2) ~&~ \quad (P \lor Q)\lbrace u/x \rbrace ~&~ \mbox{[assumption]} \\ (3) ~&~ \quad P\lbrace u/x \rbrace \lor Q \lbrace u/x \rbrace ~&~ \mbox{[definition of substitution, (2)]} \\ (4) ~&~ \qquad P \lbrace u/x \rbrace ~&~ \mbox{[assumption]} \\ (5) ~&~ \qquad \exists x P ~&~ \mbox{[introduction of existential quantifier, (4)]} \\ (6) ~&~ \qquad \exists x P \lor \exists x Q ~&~ \mbox{[introduction of disjunction, (5)]} \\ (7) ~&~ \quad P \lbrace u/x \rbrace \to \exists x P \lor \exists x Q ~&~ \mbox{[introduction of conditional, (4),(6)]} \\ (8) ~&~ \qquad Q \lbrace u/x \rbrace ~&~ \mbox{[assumption]} \\ (9) ~&~ \qquad \exists x Q ~&~ \mbox{[introduction of existential quantifier, (8)]} \\ (10) ~&~ \qquad \exists x P \lor \exists x Q ~&~ \mbox{[introduction of disjunction, (9)]} \\ (11) ~&~ \quad Q \lbrace u/x \rbrace \to \exists x P \lor \exists x Q ~&~ \mbox{[introduction of conditional, (8),(10)]} \\ (12) ~&~ ~\exists x P \lor \exists x Q ~&~ \mbox{[elimination of conjunction (3), (7), (11)]} \\ (13) ~& \exists x(P\vee Q)~\vdash~ \exists x P \lor \exists x Q ~&~ \mbox{[conclusion, (1), (12)]}\end{array}$$

Here I'm using $P \lbrace u/x \rbrace$ to denote the substitution of $x$ by $u$ in $P$ and the rule for eliminating the existential quantifier: "If $\phi \lbrace u/x \rbrace \to \psi$, then $\exists x \phi \vdash \psi$", provided $u$ is an unused name and $\psi$ does not contain $u$. (Here $\phi$ is $P \lor Q$ and $\psi$ is $\exists x P \lor \exists x Q$)

The problem is I have to express it in tree form using sequents and we've been given the rule for eliminating the extistential quantifier this way: "from $\Gamma \vdash \exists x \phi$ and $\Gamma, \phi \vdash \psi$ it is immediate consequence $\Gamma \vdash \psi$, whenever $x$ is not free in $\Gamma$ nor $\phi$ " (I should have written the first two sequents above a horizontal line and the third one under it, I apologize for that), and I am having difficulties "translating" the deduction I made above into this form. If I take: $$\Gamma \equiv \exists x (P \lor Q) \\ \phi \equiv (P \lor Q) \lbrace u/x \rbrace \\ \psi \equiv \exists x P \lor \exists x Q$$ then I would get to the desired result, I have no problem on proving $\exists x (P \lor Q),(P \lor Q)\lbrace u/x\rbrace \vdash \exists x P \lor \exists x Q$ but the problem for me is the other sequent: $$\exists x (P \lor Q) \vdash \exists x ((P \lor Q) \lbrace u/x \rbrace )$$ I don't know how to justify that sequent. Any advice, hint or attept to solve it is welcome, thanks in advance.

$\endgroup$
  • $\begingroup$ I do not see the problem: with $\Gamma = ∃x(P∨Q)$ we have: $∃x(P∨Q) \vdash ∃x(P∨Q)$ and you have derived: $∃x(P∨Q), (P∨Q) \vdash ∃xP∨∃xQ$. Thus, an application of $\exists$-elim gives you: $∃x(P∨Q) \vdash ∃xP∨∃xQ$. $\endgroup$ – Mauro ALLEGRANZA May 31 '16 at 19:42
  • 1
    $\begingroup$ @MauroALLEGRANZA of course, you're totally right. I don't know what is going on with me, I'm doing so stupid reasonings... anyway, thanks for make it clear. $\endgroup$ – la flaca May 31 '16 at 20:46
1
$\begingroup$

Your proof is correct. Perfect use of substitution and existential elimination.

Now, if you want to prove it by semantic tableaux/tree, just assume the premiss is true and assume the conclusion is false. Then you have to work the quantifiers and the disyunctions with $u/x$ until you get a contradiction in both branches of the tree.

$\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.