Corrigé Centrale 2026 Informatique MPI — Partie D (Q40 à Q42) : Déduction naturelle pour la logique déontique

Sujet officiel du concours Centrale, session 2026, épreuve Informatique MPI. Corrigé rédigé par Ibrahim Alame.

Énoncé

Règles de la déduction naturelle classique (figure 1 du sujet) :

$Γ , A ⊢ A Ax \frac{Γ ⊢ A}{Γ , B ⊢ A} Aff \frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A \land B} I \land$

$\frac{Γ ⊢ A \land B}{Γ ⊢ A} E_{1} \land \frac{Γ ⊢ A \land B}{Γ ⊢ B} E_{2} \land \frac{Γ ⊢ A}{Γ ⊢ A \lor B} I_{1} \lor \frac{Γ ⊢ B}{Γ ⊢ A \lor B} I_{2} \lor$

$\frac{Γ ⊢ A \lor B Γ , A ⊢ C Γ , B ⊢ C}{Γ ⊢ C} E \lor \frac{Γ , A ⊢ B}{Γ ⊢ A \to B} I \to$

$\frac{Γ ⊢ A \to B Γ ⊢ A}{Γ ⊢ B} E \to \frac{Γ , A ⊢ ⊥}{Γ ⊢ \neg A} I \neg \frac{Γ ⊢ A Γ ⊢ \neg A}{Γ ⊢ ⊥} E \neg$

$\frac{Γ , \neg A ⊢ ⊥}{Γ ⊢ A} RAA Γ ⊢ A \lor \neg A TE$

Q40. Arbre de preuve de $⊢ A \to (B \to (A \land B))$ .

Le système $D$ ajoute trois règles pour $□$ (sans contexte pour D1 : les théorèmes sont vrais dans tout monde idéal) :

$\frac{⊢ φ}{⊢ □ φ} D1 \frac{Γ ⊢ □ ( φ \to ψ )}{Γ ⊢ □ φ \to □ ψ} D2 \frac{Γ ⊢ □ φ}{Γ ⊢ \neg □ \neg φ} D3$

Q41. Prouver $⊢ \neg (□ A \land □ \neg A)$ : pas d'obligations contradictoires.
Q42. Prouver $⊢ □ (A \land B) \to (□ A \land □ B)$ et $⊢ (□ A \land □ B) \to □ (A \land B)$ (Q40 utilisable sans en reproduire l'arbre).

Corrigé

Les arbres se lisent de bas en haut : chaque barre est une règle de la figure 1 ou de $D$ , dont le nom est à droite ; une barre sans prémisse est un axiome. On applique les règles telles qu'elles sont écrites, en particulier Ax, qui ne fournit que la dernière hypothèse du contexte : les autres s'obtiennent par Aff. Les longues preuves sont découpées en sous-arbres nommés $Π$ , dont la conclusion est rappelée à l'endroit où ils se greffent. Chacun des arbres ci-dessous a été vérifié règle par règle par un petit vérificateur écrit en Python (contextes ordonnés, Ax sur la dernière hypothèse).

Q40. On introduit les deux implications, puis on prouve la conjonction à partir des deux hypothèses.

$\frac{\frac{\frac{\frac{A ⊢ A Ax}{A , B ⊢ A} Aff A , B ⊢ B Ax}{A , B ⊢ A \land B} I \land}{A ⊢ B \to ( A \land B )} I \to}{⊢ A \to ( B \to ( A \land B ))} I \to$

La règle Ax avec $Γ = A$ donne $A, B ⊢ B$ directement ; pour $A, B ⊢ A$ , on part de $A ⊢ A$ (Ax avec $Γ$ vide) et l'on affaiblit par $B$ . On lit la preuve comme un programme : c'est le type 'a -> 'b -> 'a * 'b de fun a b -> (a, b).

Q41. Notons $H = □ A \land □ \neg A$ . Il suffit de dériver $H ⊢ ⊥$ , puis d'appliquer I $\neg$ (avec $Γ$ vide). L'idée : D3 transforme $□ A$ en $\neg □ \neg A$ , qui contredit directement $□ \neg A$ .

100 % gratuit

La suite du corrigé est sur Adloun

Le corrigé rédigé en entier, question par question, et le tuteur pour poser des questions sur ce sujet.

Voir le corrigé complet, gratuitement

Inscription gratuite en 30 secondes (e-mail, nom d'utilisateur, mot de passe, classe ou profil), sans carte bancaire : arrivée directe sur le corrigé.

Toutes les parties de l'épreuve

Corrigé complet gratuit →