Axiome logique
La méthode axiomatique permet de définir l'ensemble des lois logiques du premier ordre à partir d'axiomes logiques et de règles de déduction de telle façon que toutes les lois logiques soient ou bien un axiome ou bien une formule dérivée des axiomes avec un nombre fini d'applications des règles de déduction.
Cette présentation, purement syntaxique, est équivalente à la présentation sémantique de la théorie des modèles, qui permet de définir une loi logique comme une formule vraie dans tous les mondes possibles. Cette équivalence fait l'objet d'un théorème de complétude.
Les axiomes logiques des Principia Mathematica
Les lois logiques sont obtenues à l’intérieur du système de Whitehead et Russell (1910) à partir de six schémas d’axiomes et de deux règles de déduction, la règle de détachement et la règle de généralisation.
Les schémas d’axiomes
Ces schémas d’axiomes sont les suivants. p, q, et r peuvent être remplacées par des formules quelconques (avec ou sans variables libres) du calcul des prédicats au premier ordre.
- si (p ou p) alors p :
- si p alors (p ou q) :
- si (p ou q) alors (q ou p) :
- si (si p alors q) alors (si (p ou r) alors (q ou r)) :
- si (tout x est tel que p) alors p’ :
où p’ est obtenu à partir de p en substituant une variable y, non liée dans p, à toutes les occurrences libres de x dans p.
- si (tout x est tel que (p ou q)) alors (p ou tout x est tel que q) :
où p est une formule qui ne contient pas x comme variable libre
Les deux règles de déduction
La règle de détachement ou modus ponens dit que des deux prémisses p et (si p alors q) on peut déduire q.
La règle de généralisation dit que de l’unique prémisse p on peut déduire (tout x est tel que p)
Équivalence avec la déduction naturelle
On peut prouver que toutes les vérités anhypothétiques, au sens de la déduction naturelle, sont ou bien des axiomes obtenus à partir de ces schémas, ou bien des conséquences que l’on peut déduire en un nombre fini d’étapes à partir de ces axiomes avec les deux règles de déduction.
Toutes les preuves que l’on peut formaliser dans la déduction naturelle peuvent être formalisées dans le calcul logique (au premier ordre) de Whitehead et Russell et inversement.
Complétude du système
Gödel a prouvé un théorème de complétude qui affirme que ces six schémas d'axiomes et ces deux règles de déduction suffisent pour obtenir toutes les lois logiques.
Portail de la logique