Deduzione naturale

Ci sono regole per l'introduzione e l'eliminazione dei quantificatori.

Esistenziale

Introduzione

(P a) ∃x. (P x)

Eliminazione

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

c è una costante locale alla regola.

Esempi

(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)

Universale

Introduzione

(P c) ∀x. (P x)

c è una costante locale alla regola.

Eliminazione

∀x. (P x) (P a)

Esempi

∀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)))

Insieme di quantificazione

Le regole cha abbiamo danno una semantica per i quantificatori ma non fanno alcuna ipotesi sull'insieme su cui quantifichiamo. Una prima ipotesi naturale su questo insieme è che questo insieme non sia vuoto. Usando tale ipotesi possiamo adesso provare la formula (∀x. (P x)) ⇒ ∃x. (P x):

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

Esercizi

G1. Dimostrare che (∃x. ∀y. (P x y)) ⇒ (∀y. ∃x. (P x y)).

G2. Dimostrare che (∀y. ∃x. (P x y)) ⇒ (∃x. ∀y. (P x y)).

G3. Dimostrare che (¬(∃x. (P x))) ⇒ (∀x. ¬(P x)).

G4. Dimostrare che (∀x. ¬(P x)) ⇒ ¬ (∃ x. (P x)).

G5. Dimostrare che (∃x. ¬(P x)) ⇒ ¬(∀x. (P x)).

G6. Dimostrare nella logica classica che ¬(∀x. (P x)) ⇒ (∃x. ¬(P x)).

G7. Dimostrare nella logica classica che ((∀x. (P x)) ⇒ Q) ⇒ ∃x. ((P x) ⇒ Q).

G8. Dimostrare che (∃x. ((P x) ⇒ Q)) ⇒ ((∀x. (P x)) ⇒ Q).

G9. Dimostrare che ((∃x. (P x)) ⇒ Q) ⇒ ∀x. ((P x) ⇒ Q).

G10. Dimostrare che (∀x. ((P x) ⇒ Q)) ⇒ ((∃x. (P x)) ⇒ Q).

G11. Dimostrare che (Q ⇒ (∀x. (P x))) ⇒ ∀x. (Q ⇒ (P x)) .

G12. Dimostrare che (∀x. (Q ⇒ (P x))) ⇒ (Q ⇒ (∀x. (P x))).

G13. Dimostrare nella logica classica che (Q ⇒ (∃x. (P x))) ⇒ (∃x. (Q ⇒ (P x))).

G14. Dimostrare che (∃x. Q ⇒ (P x)) ⇒ (Q ⇒ (∃x. (P x))).

G15. Dimostrare che ((∀x. (P x)) ∨ Q) ⇒ (∀x. (P x) ∨ Q).

G16. Dimostrare nella logica classica che (∀x. ((P x) ∨ Q)) ⇒ ((∀x. (P x)) ∨ Q).

G17. Dimostrare che ((∃x. (P x)) ∨ Q) ⇒ ∃x. ((P x) ∨ Q).

G18. Dimostrare che (∃x. ((P x) ∨ Q)) ⇒ (∃x. (P x)) ∨ Q.

*G19. Dimostrare che (P a) ⇒ ((∀x. ((P x) ⇒ (Q x))) ⇒ (Q a)).

*G20. Dimostrare che (∃x. ((P x) ⇒ (Q x))) ⇒ ((∀x. (P x)) ⇒ (∃x. (Q x))).

*G21. Dimostrare che (∀x. (P x) ⇒ (Q x)) ⇒ ((∃x. (P x)) ⇒ (∃x. (Q x))) .

*G22. Dimostrare che (∃x. ((P x) ∧ (Q x))) ⇒ (∃x. ((Q x) ∧ (P x))) .

Laurent Théry

Last modified: Thu May 23 23:15:07 MEST 2002