Théories d'auto-vérification - Self-verifying theories

Les théories d'auto-vérification sont des systèmes arithmétiques cohérents du premier ordre , beaucoup plus faibles que l'arithmétique de Peano , qui sont capables de prouver leur propre cohérence . Dan Willard a été le premier à étudier leurs propriétés, et il a décrit une famille de tels systèmes. D'après le théorème d'incomplétude de Gödel , ces systèmes ne peuvent pas contenir la théorie de l'arithmétique de Peano ni son fragment faible de l' arithmétique de Robinson ; néanmoins, ils peuvent contenir des théorèmes forts.

Dans les grandes lignes, la clé de la construction par Willard de son système est de formaliser suffisamment la machinerie de Gödel pour parler de prouvabilité en interne sans pouvoir formaliser la diagonalisation . La diagonalisation dépend de la capacité de prouver que la multiplication est une fonction totale (et dans les versions antérieures du résultat, l'addition également). L'addition et la multiplication ne sont pas des symboles de fonction du langage de Willard ; au lieu de cela, la soustraction et la division le sont, les prédicats d'addition et de multiplication étant définis en fonction de ceux-ci. Ici, on ne peut prouver la phrase exprimant la totalité de la multiplication : ${\displaystyle \Pi _{2}^{0}}$

${\displaystyle (\forall x,y)\ (\exists z)\ {\rm {multiply}}(x,y,z).}$

où est le prédicat à trois places qui représente . Lorsque les opérations sont exprimées de cette manière, la prouvabilité d'une phrase donnée peut être codée comme une phrase arithmétique décrivant la fin d'un tableau analytique . La prouvabilité de la cohérence peut alors être simplement ajoutée en tant qu'axiome. Le système résultant peut être prouvé cohérent au moyen d'un argument de cohérence relative par rapport à l'arithmétique ordinaire. ${\displaystyle {\rm {multiplier}}}$${\style d'affichage z/y=x}$

On peut en outre ajouter n'importe quelle phrase arithmétique vraie à la théorie tout en conservant la cohérence de la théorie. ${\displaystyle \Pi _{1}^{0}}$

Les références

• Solovay, Robert M. (9 octobre 1989). "Injecter des incohérences dans les modèles de PA" . Annales de logique pure et appliquée . 44 (1–2) : 101–132. doi : 10.1016/0168-0072(89)90048-1 .
• Willard, Dan E. (juin 2001). « Systèmes d'axiome d'auto-vérification, le théorème d'incomplétude et les principes de réflexion connexes » . Le Journal de la Logique Symbolique . 66 (2) : 536-596. doi : 10.2307/2695030 .
• Willard, Dan E. (mars 2002). "Comment étendre les tableaux sémantiques et les versions sans coupure du deuxième théorème d'incomplétude presque jusqu'au Q arithmétique de Robinson" . Le Journal de la Logique Symbolique . 67 (1) : 465-496. doi : 10.2178/jsl/1190150055 .

Liens externes

• La page d'accueil de Dan Willard .

Cet article lié à la logique est un bout . Vous pouvez aider Wikipedia en l' étendant .

• v
• t
• e