1.9. Axiomes et preuves
Enoncés
Une expression est close, si sa liste de variables libres est vide
(toutes ses variables sont liées), de sorte que sa valeur ne dépend que du système où elle
est interprétée.
En logique du premier ordre, un énoncé est une formule close. Un énoncé A aura
donc une valeur booléenne précise (vrai ou faux) dépendant uniquement du choix d'un système
M interprétant son langage. On note M⊨A la véracité de A dans
M.
La liste des axiomes d'une théorie est un ensemble d'énoncés, présentés
comme tous vrais dans certains systèmes donnés appelés modèles de la théorie. Expliquons.
Théories réalistes vs axiomatiques en mathématiques et autres sciences
Après la distinction de nature (mathématique ou non), les théories
peuvent également différer selon l'intention de leur usage, entre réalisme et formalisme :
Une théorie axiomatique est une théorie formellement donnée
T = (τ, L, X) avec une
liste X d'axiomes visant à définir la classe de ses modèles, comme celle de
tous les systèmes M interprétant le langage L où tous les axiomes (éléments
de X) sont vrais, ce qu'on notera M⊨T.
Une théorie réaliste est une théorie invoquée pour décrire soit
un système fixe soit un système variable (une classe de systèmes), vus comme
donnés par une réalité indépendante. Ses axiomes donnés
sont des énoncés qui, pour certaines raisons, sont considérés connus comme vrais sur ces
systèmes. Une telle théorie est "vraie" si tous ses axiomes y sont effectivement vrais.
Ces systèmes sont alors des modèles, qualifiés de standard par contraste avec les
autres modèles (non voulus) de cette théorie prise axiomatiquement.
Cette véracité sera habituellement assurée pour les théories réalistes des
mathématiques pures : arithmétique et théorie des ensembles (bien que la signification
réaliste de la théorie des ensembles ne soit pas toujours claire suivant les axiomes considérés).
Ces théories admettront également des modèles non standard, rendant effective la
différence entre leurs significations réaliste et axiomatique.
Hors des mathématiques pures, la véracité des théories réalistes peut être douteuse
(discutable): les énoncés non mathématiques sur des systèmes non mathématiques peuvent
être ambigus (mal définis), tandis que la vérité des théories des mathématiques appliquées
peut être approximative, ou spéculative comme les systèmes "réels" voulus peuvent être
inconnus (contingents parmi d'autres systèmes possibles). Une telle théorie est dite
falsifiable si en principe, le cas de sa fausseté
peut être découvert en comparant ses prédictions (théorèmes) avec les observations.
Par exemple, la biologie est relative à un grand nombre de choix aléatoires discrètement
accumulées par la nature sur Terre pendant des milliards d'années. Elle contient de
nombreux "axiomes", falsifiables et qui nécessitent de nombreux tests empiriques.
Les théories non-réalistes en dehors des mathématiques
(non qualifiées d'axiomatiques par manque de précision mathématique) seraient des
œuvres de fiction décrivant des systèmes imaginaires ou futurs possibles.
La géométrie euclidienne fut d'abord conçue comme théorie réaliste de mathématiques
appliquées (pour son rôle de première théorie physique), puis fut comprise comme une théorie
axiomatique de mathématiques pures parmi d'autres géométries également légitimes
mathématiquement ; tandis que l'espace physique réel est plus précisément décrit par la
géométrie non-euclidienne de la Relativité Générale.
Démontrabilité
Une preuve ou démonstration d'un énoncé A dans une théorie T,
est un modèle fini d'une théorie de la démonstration (réduite à la description d'une
unique preuve), présentant A en "conclusion" et utilisant une liste finie d'axiomes
parmi ceux de T.
Des formalisations complètes appropriées du concept de preuve pour la logique du premier ordre
ont pu être établies par les spécialistes. Elles peuvent prendre la forme de théories de la
démonstration formalisées (comme théories axiomatiques), ou d'algorithmes de vérification
de preuves (n'utilisant qu'une quantité de ressources de calcul liée à la taille d'une preuve donnée).
Mais la plupart des travaux mathématiques ne sont que partiellement formalisés:
on utilise des preuves semi-formelles, juste assez rigoureuses pour donner l’impression qu’une
formalisation complète est possible sans l'avoir en fait rédigée;
une vision intuitive d'un problème peut sembler plus claire qu'un raisonnement formel.
De même, ce travail présentera des preuves naturellement sans formalisation complète explicite :
utilisant parfois des articulations en langage courant, elles seront principalement écrites sous
forme d’une succession d’énoncés, chacun visiblement vrai en vertu des précédents, de
prémisses, d'axiomes, de théorèmes connus, et de règles de preuve, notamment celles des quantificateurs (1.10). Les fins de preuves sont marquées
par "∎".
Mais sans détailler
une théorie de la démonstration, voyons-en quelques propriétés générales.
On dit que A est démontrable (ou ) dans T, ou un théorème de T, et
on note T ⊢ A s'il existe une preuve de A
dans T.
En pratique, seuls sont qualifiés de théorèmes les énoncés connus comme tels, à savoir
dont on connait une preuve. Mais des synonymes de "théorème" sont traditionnellement utilisés
pour les qualifier suivant leur importance: un théorème
est plus important qu'une proposition. L'un ou l'autre peuvent se déduire d'un lemme
autrement moins important, et implique facilement un corolaire aussi moins important.
Toute bonne théorie de la démonstration doit bien entendu être correcte, à savoir
qu'elle ne peut "prouver" que des énoncés toujours vrais: la démontrabilité implique la
vérité dans chaque modèle (où tous les axiomes sont vrais).
Validité logique
Pour un langage donné L, un énoncé A est dit logiquement valide, s'il est
démontrable avec L sans utiliser d'axiome. On pourrait noter cela
⊢ A mais par
mesure d'exactitude il faut l'écrire L ⊢ A (signifiant que A est théorème de
la théorie faite de L
sans axiome, donc de toute autre théorie contenant L), Alors, A est vrai dans
tous les systèmes interprétant L en vertu du caractère correct du cadre logique.
Les plus simples énoncés logiquement valides sont les tautologies (dont les
variables Booléennes sont remplacées par des énoncés); d'autres seront donnés en 1.10.
Une preuve de A utilisant certains axiomes peut se voir comme une preuve de
(conjonction de ces axiomes ⇒ A) sans axiome, rendant cette implication logiquement valide.
Réfutabilité et cohérence
Une réfutation de A dans T, est une preuve de ¬A. S'il en existe
(T ⊢ ¬A), l'énoncé A est dit réfutable (dans T).
Un énoncé est dit décidable (dans T) s'il est démontrable ou réfutable.
Une contradiction d'une théorie T est une preuve de 0 dans T.
S'il en existe (T ⊢ 0), la théorie T est dite contradictoire ou inconsistante.
Sinon est est dite cohérente.
Une réfutation de A dans T
peut se voir comme une contradiction
de la théorie T∧A obtenue en ajoutant A aux axiomes de T.
Si un énoncé est à la fois démontrable et réfutable dans T alors tous le
sont, car cela signifie que la théorie est contradictoire, indépendamment de
l'énoncé choisi :
⊢ (A ∧ ¬A) ⇔ 0
((T ⊢ A) ∧
(T ⊢ B)) ⇔ (T ⊢ A∧B)
((T ⊢ A) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).
Ainsi une contradiction peut être présentée comme une preuve de A avec une
réfutation de A. Dans une théorie contradictoire, tout énoncé est démontrable.
Son cadre étant correct, une telle théorie n'a aucun modèle.
Au-delà de la qualité indispensable de correction de la partie théorie de la
démonstration d'un cadre logique, plus remarquable est sa qualité réciproque
de complétude: pour toute théorie axiomatique qu'il décrit, tout énoncé vrai
dans tous les modèles est démontrable. Autrement dit, tout énoncé non démontable
est faux quelque part et tout énoncé irréfutable est vrai quelque part. Ainsi, toute théorie
cohérente a des modèles existants, mais souvent une diversité de ceux-ci, car tout énoncé
indécidable est vrai dans certains et faux dans d'autres. Ajouter des énoncés indécidables
aux axiomes conduit à différentes théories cohérentes pouvant être «en désaccord»
sans conflit, descriptions correctes de systèmes différents qui existent également.
Cela résout le gros des divergences a priori entre Platonisme et
formalisme, tout en donnant un sens clair
et naturel aux concepts a priori intuitifs de «démonstration», «théorème» et «cohérence».
Other languages:
EN : 1. First foundations of
mathematics : 1.9. Axioms and proofs