Natural Deduction Proof With Quantifiers

565 Views Asked by At

enter image description here

Here is a natural deduction proof where my answers are in the red.

I have questions on the following lines:

Line 8: Could we introduce an $\lor$ operator here? We have $\exists xQ(x)$ so with $\lor$ introduction we can say have it or anything right, because it is already true?

Line 12 and 13: We eliminate $\exists x (P(x) \rightarrow Q(x))$ on line 1 because there is more than one element in this statement. And we introduce $\exists$ on 13 because we proved that there is only one element that satisfies this.

Anything else in the red look incorrect?

Does the above sound correct? I am struggling with the $\exists$ part of this kind of proofs.

1

There are 1 best solutions below

2
On BEST ANSWER

Line 8 is correct, exactly for the reason you said. But there are other mistakes in your proof, most of them are related to the way to manage the existential quantifier.

The big external box (lines 3-12) is what you do to eliminate the existential quantifier $\exists x$ from premise 1 ($\exists x (P(x) \to Q(x))$). Hence, the formulas in lines 12 and 13 must coincide and line 13, not line 12, is the rule $\exists_\text{elim}$ which closes the box.

So, in line 13, the formula is correct but the inference rule is $\exists_\text{elim}$ (1, 3-12).

Line 3 opens the box for to eliminate the existential quantifier $\exists x$ from premise 1 ($\exists x (P(x) \to Q(x))$), therefore the formula in line 3 (the assumption) must be the one in line 1 without the existential quantifier and with a generic term $c$ instead of $x$, i.e. $P(c) \to Q(c)$.

In line 6, you cannot apply $\to_\text{elim}$ to a formula that is not of the form $A \to B$ (premise 1 has the form $\exists x (A \to B)$, which is not the needed one). The problem is that in your attempt of proof you didn't have such a formula. But now we have it (line 3), so the correct inference rule is $\to_\text{elim}$ (3, 5).

In line 9 the assumption at the beginning of the rule to eliminate the disjunction $P(c) \lor \lnot P(c)$ must be exactly one of the two formulas in the disjunction, in this case $\lnot P(c)$, and not $\lnot P(x)$.

In line 12, the formula is correct but the inference rule is $\lor_\text{elim}$ (4, 5-11). Indeed, the two internal boxes are what you do to eliminate the disjunction in line 4, and line 12 is the rule $\lor_\text{elim}$ that closes the two boxes (and formula in line 12 is the same as the last ones in the two internal boxes, lines 8 and 11).