Aller au contenu
Topos Uranos
Français

Systèmes déductifs formels

Résumé

Cette leçon fait du langage de l’unité précédente un instrument pour démontrer. Elle définit ce qu’est un système déductif formel (un langage, des schémas d’axiomes et des règles d’inférence) et présente le premier des deux avec lesquels travaille le cours, le système de Łukasiewicz : trois schémas d’axiomes et le modus ponens comme règle unique. Elle définit avec précision la déduction à partir d’un ensemble de prémisses, le théorème et la relation Γ⊢φ\Gamma \vdash \varphi, déduit ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) en cinq lignes et démontre les propriétés structurelles de la déduction : réflexivité, monotonie, modus ponens entre déductions, coupure et finitude. Elle démontre ensuite, par récurrence forte sur le nombre de lignes, le théorème de déduction et sa réciproque, qui permettent de raisonner avec des déductions sur les déductions, et définit l’équivalence prouvable. Enfin, elle établit sans recourir aux valeurs de vérité la limite de ce système dans une langue dont le seul connecteur est la négation conjointe : un marquage à valeurs 00 et 11, calculé par récurrence sur les formules, que les axiomes de Łukasiewicz et le modus ponens conservent, prouve que certaines formules qui devraient se déduire ne se déduisent pas, et que l’on ne passe même pas de (v1↓v2)(v_{1} \downarrow v_{2}) à (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}). Il en découle la nécessité d’une seconde règle, le remplacement de la double négation, avec laquelle la leçon suivante complète le système.

Objectifs d’apprentissage

  1. Reconnaître les instances des schémas A1, A2 et A3 et décider si une suite de formules est une déduction à partir d’un ensemble de prémisses.
  2. Construire des déductions dans le système de Łukasiewicz, avec des axiomes, des prémisses et le modus ponens, et des déductions sur les déductions avec la réflexivité, la monotonie, la coupure, le théorème de déduction et sa réciproque.
  3. Démontrer les propriétés structurelles de la déduction et le théorème de déduction par récurrence forte sur le nombre de lignes.
  4. Établir des équivalences prouvables et utiliser le fait que l’équivalence prouvable est réflexive, symétrique et transitive.
  5. Démontrer qu’une formule n’est pas déductible au moyen d’un marquage que les axiomes et le modus ponens conservent, et expliquer par lui la limite du système de Łukasiewicz dans la langue à un seul connecteur et pourquoi une seconde règle est nécessaire.

Qu’est-ce qu’un système déductif formel

L’unité précédente a construit un langage : elle a décidé quelles chaînes de cercles et de disques sont des formules, et rien de plus. Or un langage, à lui seul, n’affirme ni ne démontre rien ; pour démontrer il faut, en outre, un point de départ et une manière d’avancer. Un système déductif formel se compose donc de trois éléments : un langage formel, qui fixe les formules ; un ensemble d’axiomes, formules que l’on admet sans démonstration ; et un ensemble de règles d’inférence, qui disent quelle formule peut s’écrire à partir d’autres déjà écrites. Le point décisif est que ces trois choses sont purement syntaxiques : pour vérifier qu’une formule est un axiome, ou qu’une règle a été bien appliquée, il suffit de regarder les chaînes, sans demander ce qu’elles signifient. S’il en est ainsi, une démonstration dans un système formel peut se vérifier mécaniquement, symbole par symbole, et c’est dans cette possibilité que réside toute sa valeur.

Il convient de remarquer dès le début qu’un axiome n’est pas ici une « vérité évidente par elle-même », comme dans l’usage ancien du mot, mais une formule choisie comme point de départ. Que le choix soit judicieux (que les axiomes soient vrais en un sens que la sémantique précisera, et qu’ils suffisent à déduire tout ce qui doit se déduire) est une question sur le système, à laquelle on répond par des théorèmes à son sujet et non par l’intuition : l’unité sur la métathéorie y répond, et la dernière section de cette leçon montre que la question n’est pas oiseuse.

Schémas d’axiomes et instances

Les systèmes de la logique propositionnelle n’énoncent pas leurs axiomes un par un, car ils sont en nombre infini, mais au moyen de schémas : des expressions du métalangage écrites avec des métavariables, comme (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Un schéma n’est pas une formule ; c’est un moule. Une instance du schéma est la formule qui résulte de la substitution d’une formule à chaque métavariable, de manière uniforme : la même formule est substituée à toutes les occurrences d’une même métavariable, bien que des métavariables distinctes puissent recevoir la même formule ou des formules distinctes.

ExempleInstances d’un schéma

Avec φ:=v1\varphi := v_{1} et ψ:=¬v2\psi := \neg v_{2}, le schéma (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) donne l’instance (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})) ; avec φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) et ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}), il donne ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), car rien n’empêche deux métavariables de recevoir la même formule. En revanche, (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) n’est pas une instance de ce schéma : la première et la dernière occurrence de φ\varphi recevraient des formules distinctes, et la substitution ne serait pas uniforme. Chaque instance, une fois les abréviations dépliées, est une chaîne de cercles et de disques ; le schéma, au contraire, ne vit que dans le métalangage.