Logique infinitaire

Une logique infinitaire est une logique qui permet des formules infiniment longues ou des démonstrations infiniment longues. Certaines logiques infinitaires peuvent avoir des propriétés différentes de celles de la logique de premier ordre standard. En particulier, les logiques infinitaires peuvent ne pas être compactes ou complètes. Les notions de compacité et de complétude qui sont équivalentes en logique finitaire ne le sont pas forcément dans les logiques infinitaires. Par conséquent, pour les logiques infinitaires, des notions de forte compacité et complétude sont définies. Cet article aborde les logiques infinitaires présentées dans les systèmes à la Hilbert, car elles ont été largement étudiées et constituent les extensions les plus simples de la logique finitaire. Ce ne sont cependant pas les seules logiques infinitaires qui ont été formulées ou étudiées.

Notation et axiome de choix

Comme nous présentons un langage avec des formules infiniment longues, il n'est pas possible d'écrire explicitement ces formules. Pour contourner ce problème, un certain nombre de commodités de notation, qui, à proprement parler, ne font pas partie du langage formel, sont utilisées. « ${\displaystyle \cdots }$ » est utilisé pour souligner une expression infiniment longue. Dans le cas où cette notation n'est pas claire, la longueur de la séquence est notée plus tard. Lorsque cette notation devient ambiguë ou confuse, des suffixes tels que ${\displaystyle \lor _{\gamma <\delta }{A_{\gamma }}}$ sont utilisés pour indiquer une disjonction infinie sur un ensemble de formules de cardinalité ${\displaystyle \delta }$. La même notation peut être appliquée aux quantificateurs, par exemple ${\displaystyle \forall _{\gamma <\delta }{V_{\gamma }:}}$. Cela est censé représenter une suite infinie de quantificateurs pour chaque ${\displaystyle V_{\gamma }}$ où ${\displaystyle \gamma <\delta }$.

Les suffixes et les « ${\displaystyle \cdots }$ » ne font pas partie de l'alphabet formel des langages infinitaires.

L'axiome du choix est supposé vrai, de façon à avoir des lois de distributivité adéquates.^[Quoi ?]

Définition des logiques infinitaires de type Hilbert

Une logique infinitaire de premier-ordre L_α,β, α régulier, β = 0 ou ω ≤ β ≤ α, a le même ensemble de symboles qu'une logique finitaire et peut utiliser toutes les règles pour la formation de formules d'une logique finitaire ainsi que les suivantes :

• Étant donné un ensemble de formules ${\displaystyle A=\{A_{\gamma }|\gamma <\delta <\alpha \}}$ alors ${\displaystyle (A_{0}\lor A_{1}\lor \cdots )}$ et ${\displaystyle (A_{0}\land A_{1}\land \cdots )}$ sont des formules. (dans chaque cas, la formule est de longueur ${\displaystyle \delta }$.)
• Étant donné un ensemble de variables ${\displaystyle V=\{V_{\gamma }|\gamma <\delta <\beta \}}$ et une formule ${\displaystyle A_{0}}$ alors ${\displaystyle \forall V_{0}:\forall V_{1}\cdots (A_{0})}$ et ${\displaystyle \exists V_{0}:\exists V_{1}\cdots (A_{0})}$ sont des formules. (dans chaque cas, la suite de quantificateurs est de longueur ${\displaystyle \delta }$.)

Les concepts de variables libres et liées s'appliquent de la même manière à des formules infinitaires. Tout comme dans la logique finitaire, une formule dont toutes les variables sont liées est appelée un énoncé.

Une théorie T en logique infinitaire ${\displaystyle L_{\alpha ,\beta }}$ est un ensemble de formules. Une preuve dans la logique infinitaire d'une théorie T est une suite d'énoncés de longueur ${\displaystyle \gamma }$ qui obéit aux conditions suivantes : chaque déclaration est soit un axiome logique, un élément de T, soit déduit des déclarations précédentes en utilisant une règle d'inférence. Comme précédemment, toutes les règles d'inférence dans la logique finitaire peuvent être utilisées, avec :

• Étant donné un ensemble de formules ${\displaystyle A=\{A_{\gamma }|\gamma <\delta <\alpha \}}$ ayant déjà existé précédemment dans la preuve, alors l'énoncé ${\displaystyle \land _{\gamma <\delta }{A_{\gamma }}}$ peut en être déduit.

Les schémas d'axiomes logiques spécifiques à la logique infinitaire sont présentés ci-dessous. Variables de schémas globaux : ${\displaystyle \delta }$ et ${\displaystyle \gamma }$ tel que ${\displaystyle 0<\delta <\alpha }$.

• ${\displaystyle ((\land _{\epsilon <\delta }{(A_{\delta }\implies A_{\epsilon })})\implies (A_{\delta }\implies \land _{\epsilon <\delta }{A_{\epsilon }}))}$
• Pour chaque ${\displaystyle \gamma <\delta }$, ${\displaystyle ((\land _{\epsilon <\delta }{A_{\epsilon }})\implies A_{\gamma })}$
• Loi de distributivité de Chang (pour chaque ${\displaystyle \gamma }$): ${\displaystyle (\lor _{\mu <\gamma }{(\land _{\delta <\gamma }{A_{\mu ,\delta }})})}$, où ${\displaystyle \forall \mu \forall \delta \exists \epsilon <\gamma :A_{\mu ,\delta }=A_{\epsilon }}$ ou ${\displaystyle A_{\mu ,\delta }=\neg A_{\epsilon }}$, et ${\displaystyle \forall g\in \gamma ^{\gamma }\exists \epsilon <\gamma :\{A_{\epsilon },\neg A_{\epsilon }\}\subseteq \{A_{\mu ,g(\mu )}:\mu <\gamma \}}$
• Pour ${\displaystyle \gamma <\alpha }$, ${\displaystyle ((\land _{\mu <\gamma }{(\lor _{\delta <\gamma }{A_{\mu ,\delta }})})\implies (\lor _{\epsilon <\gamma ^{\gamma }}{(\land _{\mu <\gamma }{A_{\mu ,\gamma _{\epsilon }(\mu )})}}))}$, où ${\displaystyle \{\gamma _{\epsilon }:\epsilon <\gamma ^{\gamma }\}}$ est un ensemble bien ordonné de ${\displaystyle \gamma ^{\gamma }}$

Les deux derniers schémas d'axiomes nécessitent l'axiome de choix car certains ensembles doivent être bien ordonnés. Le dernier schéma d'axiome est à proprement parler inutile car les lois de distribution de Chang l'impliquent.

Complétude, compacité et forte compacité

Une théorie est un ensemble de formules. Conformément à la théorie des modèles, la validité^[1] des formules dans les modèles est définie par récurrence et est conforme à la définition donnée de la validité en logique finitaire. On dit qu'une formule est valide dans une théorie T si elle est valide dans tous les modèles de T.

Une logique ${\displaystyle L_{\alpha ,\beta }}$ est complète si pour chaque formule S valable dans chaque modèle, il existe une preuve de S. Elle est fortement complète si, pour toute théorie T pour chaque formule S valide en T, il existe une preuve de S de T. Une logique infinitaire peut être complète sans être fortement complète.

Un cardinal ${\displaystyle \kappa \neq \omega }$ est faiblement compact quand pour chaque théorie T dans ${\displaystyle L_{\kappa ,\kappa }}$ contenant au plus ${\displaystyle \kappa }$ formules, si tout S ${\displaystyle \subseteq }$ T de cardinalité inférieure ${\displaystyle \kappa }$ a un modèle, alors T a un modèle. Un cardinal ${\displaystyle \kappa \neq \omega }$ est fortement compact quand pour chaque théorie T in ${\displaystyle L_{\kappa ,\kappa }}$, sans restriction de taille, si chaque S ${\displaystyle \subseteq }$ T de cardinalité inférieure à ${\displaystyle \kappa }$ a un modèle, alors T a un modèle.

Concepts expressibles en logique infinitaire

Dans le langage de la théorie des ensembles, l'expression suivante correspond à l'axiome de fondation :

${\displaystyle \forall _{\gamma <\omega }{V_{\gamma }:}\neg \land _{\gamma <\omega }{V_{\gamma +}\in V_{\gamma }}.\,}$

Contrairement à l'axiome de fondation, cette expression n'admet aucun modèle non standard. Le concept de bonne fondation ne peut s'exprimer que dans une logique qui permet un nombre infini de quantificateurs dans une unique formule. En conséquence, de nombreuses théories, y compris l'arithmétique de Peano, qui ne peuvent être finiment axiomatisées, car uniquement axiomatisées par un schéma infini de formules en logique finitaire, peuvent l'être dans une logique infinitaire.

Logiques infinitaires complètes

Deux logiques infinitaires se distinguent dans leur complétude. Celles-ci sont ${\displaystyle L_{\omega ,\omega }}$ et ${\displaystyle L_{\omega _{1},\omega }}$. La première est une logique de premier ordre finitaire standard et la seconde est une logique infinitaire qui ne permet que des déclarations de taille dénombrable.

${\displaystyle L_{\omega ,\omega }}$ est également fortement complète, compacte et fortement compacte.

${\displaystyle L_{\omega _{1},\omega }}$ n'est pas compacte, mais est complète. En outre, elle satisfait une variante de la propriété d'interpolation de Craig.

Si ${\displaystyle L_{\alpha ,\alpha }}$ est fortement complète, alors ${\displaystyle \alpha }$ est fortement compacte.

Notes et références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Infinitary logic » (voir la liste des auteurs).

Bibliographie

• Carol R. Karp, Languages with expressions of infinite length, Amsterdam, North-Holland Publishing Co., 1964 (MR 0176910)
• Kenneth Jon Barwise, Infinitary logic and admissible sets, vol. 34, J. Symbolic Logic, 1969, 226–252 p. (DOI 10.2307/2271099, JSTOR 2271099, MR 0406760), chap. 2

• Portail de la logique