Les systèmes formels, expliqués honnêtement
Une page interactive plus claire sur les systèmes formels, les axiomes, les dérivations, la cohérence et les raisons de l’incomplétude.
Il s’agit d’un simulateur de système formel simplifié. Il ne démontre pas directement les théorèmes de Gödel. Il vous aide à voir ce que font les axiomes, comment les dérivations se développent et pourquoi « ajouter plus d’axiomes » n’élimine pas magiquement l’incomplétude.
Chaque étape ci-dessous est soit un axiome de départ, soit un énoncé dérivé produit par le moteur simplifié.
Voici les énoncés que le simulateur peut dériver ensuite à partir des axiomes actuels et des énoncés déjà connus.
Un système formel part d’axiomes et utilise des règles d’inférence pour dériver des théorèmes. La question cruciale n’est pas seulement ce qui peut être dérivé, mais aussi ce qui ne peut pas l’être sans briser la cohérence.
Gödel a codé les formules et les preuves sous forme de nombres, puis a construit une phrase disant en substance : « Je ne suis pas démontrable dans ce système ». Si le système est cohérent, cette phrase ne peut pas être démontrée à l’intérieur du système, tout en étant vraie dans l’interprétation visée.
Cette page modélise un petit moteur de règles afin de vous montrer comment les axiomes étendent une théorie. Elle n’implémente ni l’arithmétique du premier ordre complète, ni la numérotation de Gödel, ni une véritable vérification de preuves. C’est un pont conceptuel, pas un assistant de preuve.