Déduction naturelle pour la logique propositionnelle.

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.
Deux prérequis à son utilisation :

• avoir eu un cours sur 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.

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)$
• $ (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 ➝ B ⊢ ¬B ➝ ¬A$ (Contraposée)
• $ (A ➝ ⊥) ⊢ ¬A $ (Raisonnement par l'absurde à partir de Logique Intuitionniste + Tiers Exclu)
• $ ⊢ (¬A ∨ ¬B)➝ ¬(A ∧ B)$
• $ ⊢ ¬(A ∧ B) ➝ (¬A ∨ ¬B)$
• $ ⊢ ¬¬A ➝ A$ (Élimination de la double négation)

Quelques preuves plus délicates

• $ ⊢ 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)