Herbrandisation - Herbrandization

L' herbrandisation d'une formule logique (du nom de Jacques Herbrand ) est une construction double à la skolémisation d'une formule. Thoralf Skolem avait considéré les skolémisations de formules sous forme de prenex comme faisant partie de sa démonstration du théorème de Löwenheim – Skolem (Skolem 1920). Herbrand a travaillé avec cette double notion d'herbrandisation, généralisée pour s'appliquer également aux formules non prenex, afin de prouver le théorème de Herbrand (Herbrand 1930).

La formule résultante n'est pas nécessairement équivalente à la formule originale. Comme pour la Skolémisation, qui ne préserve que la satisfiabilité , l'Herbrandisation étant le double de la Skolémisation, préserve la validité : la formule résultante est valide si et seulement si l'original l'est.

Définition et exemples

Soit une formule dans le langage de la logique du premier ordre . Nous pouvons supposer que ne contient aucune variable liée par deux occurrences de quantificateur différentes, et qu'aucune variable ne se produit à la fois liée et libre. (Autrement dit, pourrait être relogé pour garantir ces conditions, de telle sorte que le résultat est une formule équivalente). ${\ displaystyle F}$${\ displaystyle F}$${\ displaystyle F}$

L' herbrandisation de s'obtient alors comme suit: ${\ displaystyle F}$

• Tout d'abord, remplacez toutes les variables libres par des symboles constants. ${\ displaystyle F}$
• Deuxièmement, supprimez tous les quantificateurs sur les variables qui sont soit (1) universellement quantifiés et dans un nombre pair de signes de négation, ou (2) existentiellement quantifiés et dans un nombre impair de signes de négation.
• Enfin, remplacez chacune de ces variables par un symbole de fonction , où sont les variables qui sont encore quantifiées et dont les quantificateurs gouvernent . ${\ displaystyle v}$${\ displaystyle f_ {v} (x_ {1}, \ dots, x_ {k})}$${\ displaystyle x_ {1}, \ dots, x_ {k}}$${\ displaystyle v}$

Par exemple, considérez la formule . Il n'y a pas de variables libres à remplacer. Les variables sont du type que nous considérons pour la deuxième étape, nous supprimons donc les quantificateurs et . Enfin, nous remplaçons par une constante (puisqu'il n'y avait pas d'autres quantificateurs gouvernant ), et nous remplaçons par un symbole de fonction : ${\ displaystyle F: = \ forall y \ exists x [R (y, x) \ wedge \ neg \ exists zS (x, z)]}$${\ displaystyle y, z}$${\ displaystyle \ forall y}$${\ displaystyle \ existe z}$${\ displaystyle y}$${\ displaystyle c_ {y}}$${\ displaystyle y}$${\ displaystyle z}$${\ displaystyle f_ {z} (x)}$

${\ displaystyle F ^ {H} = \ existe x [R (c_ {y}, x) \ wedge \ neg S (x, f_ {z} (x))].}$

La skolémisation d'une formule est obtenue de la même manière, sauf que dans la deuxième étape ci-dessus, nous supprimerions les quantificateurs sur des variables qui sont soit (1) quantifiées existentiellement et dans un nombre pair de négations, soit (2) universellement quantifiées et dans un nombre impair des négations. Ainsi, considérant la même chose d'en haut, sa Skolémisation serait: ${\ displaystyle F}$

${\ displaystyle F ^ {S} = \ forall y [R (y, f_ {x} (y)) \ wedge \ neg \ exists zS (f_ {x} (y), z)].}$

Pour comprendre la signification de ces constructions, voir le théorème de Herbrand ou le théorème de Löwenheim – Skolem .

Voir également

• Logique du foncteur de prédicat

Les références

• Skolem, T. "Enquêtes logico-combinatoires dans la satisfiabilité ou la prouvabilité des propositions mathématiques: Une preuve simplifiée d'un théorème par L. Löwenheim et généralisations du théorème". (Dans van Heijenoort 1967, 252-63.)
• Herbrand, J. "Enquêtes en théorie de la preuve: les propriétés des propositions vraies". (Dans van Heijenoort 1967, 525-81.)
• van Heijenoort, J. De Frege à Gödel: Un livre source en logique mathématique, 1879-1931 . Harvard University Press, 1967.