Lazi

Extension «représentation de preuve»

Contexte

Comme on le voit dans "Lazi et un tiers exclu sur la finitude d'un calcul en lazi on peut ajouter une extension qui permet de déduire une vérité à partir d'une représentation de preuve. Une telle extension serait-elle possible avec le système de calcul de prédicat classique et la théorie des ensembles ?

Question

Dans le système de calcul de prédicat classique, la théorie des ensembles peut-elle être aussi cohérent si on lui ajoute une extension permetant de déduire une vérité en prenant l'interprétation de la concluion d'une représentation de preuve dans la même mathématique ?

Étude

En reprenant "A Simple Proof of Gödel’s Incompleteness Theorems" de Arindama Singh on voit (page 3) : If ⊢ X, then ⊢ P (⌜X⌝). Où ⌜X⌝ signifie "la représentation de X" et P(x) est la proposition "il existe une représentation de preuve de x".
Avec cette règle supplémentaire, on aurait pour toute proposition X : ⊢ P (⌜X⌝) ⇒ X.

Dans la preuve de Gödel on obtient une proposition A tq ⊢ A ⇔ ¬P(⌜A⌝). On a donc ⊢ ¬A ⇔ P(⌜A⌝). Avec l'extension on aurait ⊢ ¬A ⇒ A, et en raisonnant par l'absurde on déduit A. Mais comme on a If ⊢ X, then ⊢ P (⌜X⌝), on déduit ⊢ P(⌜A⌝), et comme ⊢ ¬A ⇔ P(⌜A⌝), on déduit ⊢ ¬A. On a donc déduit ⊢ A ∧ ¬A, absurde.

Réponse

Non, on obtiendrait une théorie incohérente.