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$
2
  • $\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, 2016 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, 2016 at 20:46

1 Answer 1

Reset to default
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$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .