Logique (mathématiques)/Autres formulations des principes de la logique du premier ordre
Cette section expose d’autres façons de formuler les principes de la logique du premier ordre.
Le calcul des séquents[modifier | modifier le wikicode]
Ce calcul a été inventé par Gentzen. Les règles de la déduction naturelle ont été formulées d’abord à son sujet. La méthode de Fitch, qui repose sur le décalage vers la droite des hypothèses provisoires, a été inventée ensuite.
Moyens d’expression[modifier | modifier le wikicode]
Aux moyens d’expression de la logique du premier ordre, le calcul des séquences ajoute deux opérateurs binaires fondamentaux, « Implique »(symbole ) et « , » (virgule), et un objet de base, « Silence ». Une séquence a la forme suivante :
- ou p1…, pn Implique c
p1…, pn sont les n prémisses, où n est un entier strictement positif, c est la conclusion. Les prémisses et la conclusion sont ou bien des formules du calcul des prédicats (sans « Implique » et « , » ) ou bien « silence ».
Formules initiales[modifier | modifier le wikicode]
Les formules initiales du calcul des séquences sont toutes les séquences de la forme suivante :
où désigne n’importe quelle formule du calcul des prédicats.
Il s’agit d’un schéma d’axiomes. C’est une vérité logique au même sens où la règle de répétition est une règle correcte de déduction. Toutes les séquences ainsi obtenues sont dites prouvables.
L’usage des hypothèses[modifier | modifier le wikicode]
La règle suivante permet d’introduire des prémisses. Elle correspond à la possibilité d’introduire librement des hypothèses provisoires.
Si est une séquence prouvable alors est une séquence prouvable.
désigne n’importe quelle combinaison de formules du calcul des prédicats avec l’opérateur « , ». On les appelle des suites (finies) de formules.
Pour calculer commodément sur les prémisses, il faut pouvoir les mettre dans n’importe quel ordre. On peut pour cela définir l’égalité entre les suites de prémisses de telle façon qu’elle respecte l’associativité et la commutativité de « , » :
L’associativité permet ainsi de supprimer toutes les parenthèses qui séparent des virgules. On se donne alors la règle suivante :
- Si et est une séquence prouvable alors est une séquence prouvable.
Les règles de déduction[modifier | modifier le wikicode]
Toutes les règles de la déduction naturelle par la méthode de Fitch peuvent être traduites en règles du calcul des séquences. Elles sont les suivantes.
Si (H Implique (si p alors q)) et (H Implique p) sont des séquences prouvables alors (H Implique q) est une séquence prouvable
Si (H, p Implique q) est une séquence prouvable alors (H Implique (si p alors q)) est une séquence prouvable
Si (H Implique p) et (H Implique q) sont des séquences prouvables alors (H Implique (p et q)) est une séquence prouvable
Si (H Implique (p et q)) est une séquence prouvable alors (H Implique p) et (H implique q) sont des séquences prouvables.
Si (H Implique p) est une séquence prouvable alors (H Implique (p ou q)) et (H Implique (q ou p)) sont des séquences prouvables.
Si (H, p Implique c) et (H, q Implique c) sont des séquences prouvables alors (H, (p ou q) Implique c) est une séquence prouvable
Si (H, p Implique (c et non c)) est une séquence prouvable alors (H Implique non p) est une séquence prouvable
Si (H Implique non non c) est une séquence prouvable alors (H Implique c) est une séquence prouvable
Si (H Implique tout x est tel que p) est une séquence prouvable et t est un terme dont les variables ne sont pas liées dans p et q est obtenu par la substitution de t à toutes les occurrences libres de x dans p alors (H Implique q) est une séquence prouvable
Si (H Implique p) est une séquence prouvable et x est une variable qui n’a pas d’occurrences libres dans les formules de H alors (H Implique tout x est tel que p) est une séquence prouvable
Si (H Implique p) est une séquence prouvable et p est obtenu à partir de q en y substituant un terme t à toutes les occurrences libres d’une variable x alors (H Implique il existe un x tel que q) est une séquence prouvable
Si (H Implique il existe un x tel que c) est une séquence prouvable et d est obtenu à partir de c en substituant à toutes les occurrences libres de x une nouvelle variable z qui n’a pas d’occurrences dans H et dans c et (H, d Implique f) est une séquence prouvable et z n’a pas d’occurrences dans f alors (H Implique f) est une séquence prouvable
L’ensemble des séquences prouvables et les vérités anhypothétiques[modifier | modifier le wikicode]
Pour définir les vérités anhypothétiques, on ajoute la règle suivante.
Si (P Implique c) est une séquence prouvable alors (P, silence Implique c) est une séquence prouvable
Les séquences prouvables sont toutes celles qui sont obtenues à partir des séquences initiales en appliquant un nombre fini de fois les règles précédentes.
Les vérités anhypothétiques sont les formules p telles que (silence Implique p) est une séquence prouvable.
Cette définition est équivalente à celle donnée par la méthode de Fitch parce que les deux méthodes sont deux façons différentes de présenter les mêmes calculs.
Les axiomes logiques des Principia Mathematica[modifier | modifier le wikicode]
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. Dans toutes les preuves les conclusions sont obtenues à partir des prémisses avec seulement ces deux règles. Cela marche parce que tous les axiomes obtenus à partir des schémas d’axiomes logiques sont automatiquement incorporés dans les prémisses.
Les schémas d’axiomes[modifier | modifier le wikicode]
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[modifier | modifier le wikicode]
La règle de détachement 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[modifier | modifier le wikicode]
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 donc être formalisées dans le calcul logique (au premier ordre) de Whitehead et Russell et inversement.
Les règles d’un dialogue[modifier | modifier le wikicode]
On va définir les règles d’un dialogue entre un défendeur et un critique. Le défendeur doit montrer que la thèse qu’il soutient est cohérente. Le critique doit prouver que la thèse est contradictoire. Les rôles ne sont pas symétriques. Le défendeur doit toujours répondre aux questions qu’on lui pose. Le critique est libre de poser des questions sur la base de tout ce que le défendeur a déjà dit.
- Si le défendeur a dit (p ou q), le critique peut lui demander de choisir entre p et q.
- Si le défendeur a dit (p et q), le critique peut lui demander de dire p, et de dire q.
- Si le défendeur a dit (si p alors q), le critique peut lui demander de choisir entre (non p) et q.
- Si le défendeur a dit (pour tout x, p) et o est un objet du discours et q est obtenu à partir de p en substituant o à toutes les occurrences libres de x dans p alors le critique peut demander au défendeur de dire q.
Les objets du discours sont des constantes construites avec les objets et les opérateurs mentionnés dans la thèse soutenue ou introduites ultérieurement.
- Si le défendeur a dit (il existe un x tel que p) alors le critique peut lui demander, comment s’appelle-t-il ? Le défendeur doit alors répondre par une constante c, et énoncer q, qui est obtenu par la substitution de c à toutes les occurrences libres de x dans p.
On suppose en outre que le défendeur et le contradicteur se sont mis d'accord sur la signification de la négation des formules complexes :
- non non p veut dire p
- non(p ou q) veut dire ((non p) et non q)
- non(p et q) veut dire ((non p) ou non q)
- non(si p alors q) veut dire (p et non q)
- non(pour tout x, p) veut dire (il existe un x tel que non p)
- non(il existe un x tel que p) veut dire (pour tout x, non p)
Un défendeur se contredit lorsqu’il a dit à la fois p et (non p), pour une formule p.
Si le défendeur est malhabile il peut être amené à se contredire alors que la thèse qu’il soutient n’est pas contradictoire. Une thèse est vraiment contradictoire lorsqu’un critique habile peut amener tous les défendeurs, habiles ou non, à se contredire.
Les règles précédentes de dialogue permettent donc de définir l’ensemble des thèses contradictoires. Définissons maintenant une loi logique comme une thèse dont la négation est contradictoire. On peut prouver que l’ensemble des lois logiques ainsi définies est identique à l’ensemble des vérités anhypothétiques définies par les règles de la déduction naturelle. Ces règles de dialogue sont donc une autre formulation des principes de la logique du premier ordre.
