Trouver la faute

Exercice · niveau 2 · informatique (MP2I/MPI), chapitre 28 — Déduction naturelle

Énoncé

Chacun de ces trois arbres conclut un séquent faux ou non démontrable. Localiser la faute, la nommer, et dire quelle règle a été mal appliquée. (a), avec $Γ = {p \lor q}$ :

$\frac{Γ ⊢ p \lor q ax \frac{Γ , p ⊢ p ax Γ , p ⊢ q ax}{Γ , p ⊢ p \land q} \land _{i} \frac{Γ , q ⊢ p ax Γ , q ⊢ q ax}{Γ , q ⊢ p \land q} \land _{i}}{Γ ⊢ p \land q} \lor_{e}$

(b) :

$\frac{\frac{{ p \to q , q } ⊢ p ax}{{ p \to q } ⊢ q \to p} \to _{i}}{⊢ ( p \to q ) \to ( q \to p )} \to_{i}$

(c), avec $Σ = {\neg\neg p, \neg p}$ :

$\frac{\frac{Σ ⊢ \neg\neg p ax Σ ⊢ \neg p ax}{Σ ⊢ ⊥} \neg _{e}}{{ \neg\neg p } ⊢ p} \neg_{i}$

Corrigé

(a) Un axiome invoque une formule absente du contexte. La branche du milieu prétend $Γ, p ⊢ q$ par $ax$ , alors que $Γ \cup {p} = {p \lor q, p}$ ne contient pas $q$ . La même faute est commise symétriquement dans la troisième branche, avec $Γ, q ⊢ p$ . Le squelette du $\lor_{e}$ est irréprochable — trois prémisses, contextes enrichis comme il faut — et c'est précisément ce qui rend la faute difficile à voir : elle est dans une feuille, pas dans la structure. Et le séquent conclu est bien faux : $v (p) = F$ , $v (q) = V$ satisfait $p \lor q$ sans satisfaire $p \land q$ .

(b) Même faute, dépouillée. Le séquent ${p \to q, q} ⊢ p$ n'est pas un axiome : $p$ n'appartient pas au contexte. Ici la structure est minimale, donc la faute saute aux yeux — mais c'est exactement la même qu'en (a). Règle de contrôle : un $ax$ ne se lit pas, il se vérifie, en regardant si la conclusion figure littéralement dans le contexte.

(c) La règle a la bonne forme, mais pas la bonne conclusion. La prémisse $Σ ⊢ ⊥$ avec $Σ = {\neg\neg p, \neg p}$ est parfaitement correcte. Mais $\neg_{i}$ appliquée à $Γ, A ⊢ ⊥$ conclut $Γ ⊢ \neg A$ , et non $Γ ⊢ A$ . Ici $A$ vaut $\neg p$ , donc la conclusion légitime est

${\neg\neg p} ⊢ \neg\neg p,$

qui est un axiome et n'apprend rien. La faute est la confusion entre deux règles : $\neg_{i}$ , qui établit une négation par l'absurde, et la règle classique d'absurdité, qui établit une formule positive à partir de la négation. La seconde n'est pas dans la liste du chapitre — c'est le sujet de l'exercice suivant.

Ce que les trois ont en commun. Aucune n'est une faute de stratégie : les trois arbres ont la bonne allure, les bonnes règles au bon endroit, et un lecteur pressé les valide. Les fautes sont locales — un contexte, une conclusion — et se trouvent en vérifiant chaque nœud isolément contre l'énoncé de sa règle. C'est exactement la discipline du chapitre chap:discipline appliquée aux preuves : on ne relit pas, on contrôle.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.