Formal proofs with ∃ ⟨15,02⟩

Here we see how to introduce and eliminate the existential quantifier (∃) in the course of a formal proof.

INTRODUCTION is pretty easy: from P(a) infer ∃xP(x).

ELIMINATION is trickier: from ∃xP(x), name the x that is a P with a new constant, e, to get P(e). Then, if you can show a further sentence Q, which contains no instances of Q, you are entitled to infer Q from ∃xP(x).

We'll see how all this works.

[chrisbrennan]

No in agreement with existential quantifier..😞