Natural deduction

There are introduction and elimination rules for quantifiers.

Existential

Introduction

(P a) ∃x. (P x)

Elimination

∃x . (P x) [(P c)] . . B B

c is a constant local to the rule (no assumptions on c, arbitrary element).

Examples

(Prime 5) ∃x. (Prime x)

(Greater 5 3) ∃y. (Greater 5 y) ∃x.∃y. (Greater x y)

∃x . ((P x) ∧ (Q x)) (P a) ∧(Q a) (Q a) ∃ x. (Q x) ∃x. (Q x) (∃x . ((P x) ∧ (Q x))) ⇒ ∃x. (Q x)

Universal

Introduction

(P c) ∀x. (P x)

c is a constant local to the rule (no assumptions on c, arbitrary element).

Elimination

∀x. (P x) (P a)

Examples

∀x . ((P x) ∧ (Q x)) (P a) ∧(Q a) (Q a) ∀ x. (Q x) ∀x. (Q x) (∀x . ((P x) ∧ (Q x))) ⇒ ∀x. (Q x)

∀x . (P x) (P a) (P a) ∨ (Q a) ∀ x. (P x) ∨ (Q x) ∀x. ((P x) ∨ (Q x)) (∀x. (P x)) ⇒ (∀x . ((P x) ∨ (Q x)))

Quantification over a set

These inference rules give a semantics for the quantifiers but do not have any hypothesis on the set on which the quantification is done. A first hypothesis on this set we can add is the fact that such a set is non-empty. Under this hypothesis, we can prove the formula (∀x. (P x)) ⇒ ∃x. (P x):

∀x. (P x) (P a) ∃x. (P x)

Exercises

G1. Prove that (∃x. ∀y. (P x y)) ⇒ (∀y. ∃x. (P x y)).

G2. Prove that (∀y. ∃x. (P x y)) ⇒ (∃x. ∀y. (P x y)).

G3. Prove that (¬(∃x. (P x))) ⇒ (∀x. ¬(P x)).

G4. Prove that (∀x. ¬(P x)) ⇒ ¬ (∃ x. (P x)).

G5. Prove that (∃x. ¬(P x)) ⇒ ¬(∀x. (P x)).

G6. Prove in classical logic that ¬(∀x. (P x)) ⇒ (∃x. ¬(P x)).

G7. Prove in classical logic that ((∀x. (P x)) ⇒ Q) ⇒ ∃x. ((P x) ⇒ Q).

G8. Prove that (∃x. ((P x) ⇒ Q)) ⇒ ((∀x. (P x)) ⇒ Q).

G9. Prove that ((∃x. (P x)) ⇒ Q) ⇒ ∀x. ((P x) ⇒ Q).

G10. Prove that (∀x. ((P x) ⇒ Q)) ⇒ ((∃x. (P x)) ⇒ Q).

G11. Prove that (Q ⇒ (∀x. (P x))) ⇒ ∀x. (Q ⇒ (P x)) .

G12. Prove that (∀x. (Q ⇒ (P x))) ⇒ (Q ⇒ (∀x. (P x))).

G13. Prove in classical logic that (Q ⇒ (∃x. (P x))) ⇒ (∃x. (Q ⇒ (P x))).

G14. Prove that (∃x. Q ⇒ (P x)) ⇒ (Q ⇒ (∃x. (P x))).

G15. Prove that ((∀x. (P x)) ∨ Q) ⇒ (∀x. (P x) ∨ Q).

G16. Prove in classical logic that (∀x. ((P x) ∨ Q)) ⇒ ((∀x. (P x)) ∨ Q).

G17. Prove that ((∃x. (P x)) ∨ Q) ⇒ ∃x. ((P x) ∨ Q).

G18. Prove that (∃x. ((P x) ∨ Q)) ⇒ (∃x. (P x)) ∨ Q.

*G19. Prove that (P a) ⇒ ((∀x. ((P x) ⇒ (Q x))) ⇒ (Q a)).

*G20. Prove that (∃x. ((P x) ⇒ (Q x))) ⇒ ((∀x. (P x)) ⇒ (∃x. (Q x))).

*G21. Prove that (∀x. (P x) ⇒ (Q x)) ⇒ ((∃x. (P x)) ⇒ (∃x. (Q x))) .

*G22. Prove that (∃x. ((P x) ∧ (Q x))) ⇒ (∃x. ((Q x) ∧ (P x))) .

Monica Nesi