Axiome logique

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 : ${\displaystyle (P\lor P)\Rightarrow P}$

• si p alors (p ou q) : ${\displaystyle P\Rightarrow (P\lor Q)}$

• si (p ou q) alors (q ou p) : ${\displaystyle (P\lor Q)\Rightarrow (Q\lor P)}$

• si (si p alors q) alors (si (p ou r) alors (q ou r)) : ${\displaystyle (P\Rightarrow Q)\Rightarrow ((P\lor R)\Rightarrow (Q\lor R))}$

• si (tout x est tel que p) alors p’ : ${\displaystyle (\forall x,p(x))\Rightarrow 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) : ${\displaystyle (\forall x,(p\lor q(x)))\Rightarrow (p\lor (\forall x,q(x)))}$

où p est une formule qui ne contient pas x comme variable libre

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)

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.

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.