Déduction naturelle.

Cette page s'adresse principalement à des étudiants en MPI ou en L2 d'informatique théorique, et regroupe des exercices de construction d'arbre de preuve en logique propositionnelle et du premier ordre.
Deux prérequis à son utilisation :

• avoir eu un cours sur le calcul des prédicat, la logique du premier ordre, et les arbres de preuve en déduction naturelle
• avoir entendu parler de notation préfixe (ou polonaise) pour décrire une formule.

Dans les sections ci-dessous, les séquents à prouver apparaissent par difficulté approximative croissante.

Logique des prédicats

On commence tranquillement avec des formules utilisant uniquement ∧

• ★ A ⊢ A ∧ A
• ★ A ∧ A ⊢ A
• ★ A ∧ B ⊢ B ∧ A (Commutativité de ∧)
• ★ A ∧ B ⊢ A ∧ A
• ★★ (A ∧ B) ∧ C ⊢ A ∧ (B ∧ C) (Associativité de ∧)

On poursuit en ajoutant un peu d'implication…

• ★ ⊢ A ➝ A
• ★ ⊢ A ➝ A ∧ A
• ★ ⊢ A ∧ B ➝ B ∧ A (commutativité de ∧)
• ★ A ∧ (A ➝ B) ⊢ B (Modus Ponens)
• ★(A ∧ B) ➝ (A ➝ B)
• ★A ➝ (B ➝ (A ∧ B))
• ★★ ⊢ A ➝ (B➝A)
• ★★ (A ➝ B) ∧ (B ➝ C) ⊢ A ➝ C (Syllogisme Barbara)
• ★★ (A ➝ B) ➝ C ⊢ (A ∧ B) ➝ C

Disjonctons un peu…

• ★ ⊢ A ➝ (A ∨ A)
• ★ ⊢ (A ∨ A) ➝ A
• ★ ⊢ (A ∧ B) ➝ (A ∨ B)
• ★ ⊢ (B ∨ A) ➝ (A ∨ B) (Commutativité de ∨)
• ★★(A ∨ B) ∨ C ⊢ A ∨ (B ∨ C) (Associativité de ∨)
• ★★(A ∨ B) ∧ C ⊢ (A ∧ C) ∨ (B ∧ C) (Distributivité de ∧ sur ∨, 1)
• ★★(A ∧ C) ∨ (B ∧ C) ⊢ (A ∨ B) ∧ C (Distributivité de ∧ sur ∨, 2)
• ★★(A ∧ B) ∨ C ⊢ (A ∨ C) ∧ (B ∨ C) (Distributivité de ∨ sur ∧, 1)
• ★★(A ∨ C) ∧ (B ∨ C) ⊢ (A ∧ B) ∨ C (Distributivité de ∨ sur ∧, 2)

Soyons négatif…

• ★ ⊢ A ➝ ¬¬A (Introduction de la double négation)
• ★★ ⊢ ¬A ➝ ¬(A ∧ B)
• ★★ (A ➝ ⊥) ⊢ ¬A
• ★★ A ➝ B ⊢ ¬B ➝ ¬A (Contraposée)
• ★★ ⊢ (¬A ∨ ¬B)➝ ¬(A ∧ B)
• ★★ ⊢ ¬(A ∧ B) ➝ (¬A ∨ ¬B)
• ★★★ ⊢ ¬¬A ➝ A (Élimination de la double négation)

Quelques preuves plus délicates

• ★★★★ (¬A ➝ ⊥) ⊢ A (Raisonnement par l'absurde à partir de Logique Intuitionniste + Tiers Exclu)
• ★★★★ ⊢ A ∨ ¬A (Tiers Exclu)
• ★★★★ ⊢ A ∨ ¬A (Tiers exclu à partir de Logique Intuitionniste + Raisonnement par contraposée)
• ★★★★ ⊢ (A➝B)➝A➝A (Loi de Pierce à partir de Logique Intuitionniste + Raisonnement par l'absurde)

Logique du premier ordre

Pour tout…

• ★ ∀z.P(z) ⊢ P(x)
• ★ ∀z.(P(z) ∧ Q(z)) ⊢ ∀z.P(z)
• ★ ∀z.P(z) ⊢ ∀z.(P(z) ∨ Q(z))
• ★ Inversion de deux ∀
• ★ e*e=e (en théorie des groupes)
• ★★★ u=e → u*u=u (en théorie des groupes)
• ★★★★ u*u=u → u=e (en théorie des groupes)
• ★★★★★ Unicité de l'inverse (en théorie des groupes)
• ★★ f(0)=0 → f(f(0))=0 (en logique égalitaire)
• ★★ 0+0=0 (avec l'axiomatique de Peano)
• ★★★★ 0+1=1 (avec l'axiomatique de Peano)
• ★★★★★ 1+1=2 (avec l'axiomatique de Peano)

Il existe…

• ★ P(x) ⊢ ∃z.P(z)
• ★ ∃z.(P(z) ∧ Q(z)) ⊢ ∃z.P(z)
• ★ ∃z.P(z) ⊢ ∃z.(P(z) ∨ Q(z))
• ★★★ Inversion de deux ∃

Un peu de tout…

• ★ ∃x.(x=0) (avec l'axiomatique de Peano)
• ★ ∀z.P(z) ⊢ ∃z.P(z)
• ★★ Inversion de ∀ et ∃
• ★★ ∃z.¬P(z) ⊢ ¬∀z.P(z)
• ★★ ∀z.¬P(z) ⊢ ¬∃z.P(z)
• ★★ ¬∃z.P(z) ⊢ ∀z.¬P(z)
• ★★★ ¬∀z.P(z) ⊢ ∃z.¬P(z)
• ★★ ∀x.∃y.x*y=x (en théorie des groupes)
• ★★ ∀x.∃y.x*y=e (en théorie des groupes)
• ★★ ∃y.∀x.x*y=x (en théorie des groupes)