Logique infinitaire - Infinitary logic

Une logique infinitaire est une logique qui permet des déclarations infiniment longues et / ou des preuves infiniment longues . Certaines logiques infinitaires peuvent avoir des propriétés différentes de celles de la logique standard du premier ordre . En particulier, les logiques infinitaires peuvent ne pas être compactes ou complètes . Les notions de compacité et d'exhaustivité qui sont équivalentes en logique finitaire ne le sont parfois pas en logique infinitaire. Par conséquent, pour les logiques infinitaires, les notions de forte compacité et de forte complétude sont définies. Cet article aborde les logiques infinitaires de type 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.

Considérer si une certaine logique infinitaire nommée Ω-logique est complète promet d'éclairer l' hypothèse du continuum .

Un mot sur la notation et l'axiome du choix

Lorsqu'un langage avec des formules infiniment longues est présenté, il n'est pas possible d'écrire de telles formules explicitement. 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. est utilisé pour désigner une expression infiniment longue. Là où cela n'est pas clair, la longueur de la séquence est notée par la suite. Lorsque cette notation devient ambiguë ou déroutante, des suffixes tels que sont utilisés pour indiquer une disjonction infinie sur un ensemble de formules de cardinalité . La même notation peut être appliquée aux quantificateurs, par exemple . Ceci est censé représenter une séquence infinie de quantificateurs: un quantificateur pour chaque où . ${\ displaystyle \ cdots}$${\ displaystyle \ bigvee _ {\ gamma <\ delta} {A _ {\ gamma}}}$ ${\ displaystyle \ delta}$${\ displaystyle \ forall _ {\ gamma <\ delta} {V _ {\ gamma}:}}$${\ displaystyle V _ {\ gamma}}$${\ displaystyle \ gamma <\ delta}$

Tous les usages de suffixes et ne font pas partie des langages infinitaires formels. ${\ displaystyle \ cdots}$

L'axiome du choix est supposé (comme cela se fait souvent lors de la discussion de la logique infinitaire) car il est nécessaire d'avoir des lois de distributivité sensibles.

Définition des logiques infinitaires de type Hilbert

Une logique infinitaire du premier ordre L _{α , β} , α régulière , β = 0 ou ω ≤ β ≤ α , a le même ensemble de symboles qu'une logique finitaire et peut utiliser toutes les règles de formation des formules d'une logique finitaire avec quelques autres:

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

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

Une théorie T en logique infinitaire est un ensemble de phrases en logique. Une preuve en logique infinitaire à partir d'une théorie T est une suite d'énoncés de longueur qui obéit aux conditions suivantes: Chaque énoncé est soit un axiome logique, un élément de T , soit est déduit d'énoncés précédents à l'aide d'une règle d'inférence. Comme précédemment, toutes les règles d'inférence en logique finitaire peuvent être utilisées, ainsi qu'une autre: ${\ displaystyle L _ {\ alpha, \ beta}}$${\ displaystyle \ gamma}$

• Étant donné un ensemble d'énoncés qui se sont produits précédemment dans la preuve, l'énoncé peut être déduit. ${\ displaystyle A = \ {A _ {\ gamma} | \ gamma <\ delta <\ alpha \}}$${\ displaystyle \ land _ {\ gamma <\ delta} {A _ {\ gamma}}}$

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

• ${\ displaystyle ((\ land _ {\ epsilon <\ delta} {(A _ {\ delta} \ implique A _ {\ epsilon})}) \ implique (A _ {\ delta} \ implique \ land _ {\ epsilon <\ delta} {A _ {\ epsilon}}))}$
• Pour chacun , ${\ displaystyle \ gamma <\ delta}$${\ displaystyle ((\ land _ {\ epsilon <\ delta} {A _ {\ epsilon}}) \ implique A _ {\ gamma})}$
• Lois de distributivité de Chang (pour chacun ):, où ou , et ${\ displaystyle \ gamma}$${\ displaystyle (\ lor _ {\ mu <\ gamma} {(\ land _ {\ delta <\ gamma} {A _ {\ mu, \ delta}})})}$${\ displaystyle \ forall \ mu \ forall \ delta \ exists \ epsilon <\ gamma: A _ {\ mu, \ delta} = A _ {\ epsilon}}$${\ displaystyle A _ {\ mu, \ delta} = \ neg A _ {\ epsilon}}$${\ displaystyle \ forall g \ in \ gamma ^ {\ gamma} \ exists \ epsilon <\ gamma: \ {A _ {\ epsilon}, \ neg A _ {\ epsilon} \} \ subseteq \ {A _ {\ mu, g (\ mu)}: \ mu <\ gamma \}}$
• Car ,, où est une bonne commande de ${\ displaystyle \ gamma <\ alpha}$${\ displaystyle ((\ land _ {\ mu <\ gamma} {(\ lor _ {\ delta <\ gamma} {A _ {\ mu, \ delta}})}) \ implique (\ lor _ {\ epsilon < \ gamma ^ {\ gamma}} {(\ land _ {\ mu <\ gamma} {A _ {\ mu, \ gamma _ {\ epsilon} (\ mu)})}}))}$${\ displaystyle \ {\ gamma _ {\ epsilon}: \ epsilon <\ gamma ^ {\ gamma} \}}$${\ displaystyle \ gamma ^ {\ gamma}}$

Les deux derniers schémas d'axiomes nécessitent l'axiome de choix car certains ensembles doivent être bien ordonnables . Le dernier schéma d'axiome est à proprement parler inutile comme l'impliquent les lois de distributivité de Chang, mais il est inclus comme un moyen naturel de permettre des affaiblissements naturels de la logique.

Exhaustivité, compacité et forte complétude

Une théorie est un ensemble d'énoncés. La vérité des déclarations dans les modèles est définie par récursivité et sera en accord avec la définition de la logique finitaire où les deux sont définis. Compte tenu d' une théorie T une déclaration est dite valide pour la théorie T s'il est vrai dans tous les modèles de T .

Une logique est complète si , pour chaque phrase S valide dans tous les modèles , il existe une preuve de S . Il est fortement complet si pour toute théorie T pour chaque phrase S valide dans T il y a une preuve de S de T . Une logique infinitaire peut être complète sans être fortement complète. ${\ displaystyle L _ {\ alpha, \ beta}}$

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

Concepts exprimables en logique infinitaire

Dans le langage de la théorie des ensembles, l'énoncé suivant exprime le fondement :

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

Contrairement à l'axiome de la fondation, cette affirmation n'admet aucune interprétation non standard. Le concept de bien-fondé ne peut être exprimé que dans une logique qui autorise une infinité de quantificateurs dans un énoncé individuel. En conséquence, de nombreuses théories, y compris l'arithmétique Peano , qui ne peuvent pas être correctement axiomatisées en logique finitaire, peuvent être dans une logique infinitaire appropriée. D'autres exemples incluent les théories des champs non archimédiens et des groupes sans torsion . Ces trois théories peuvent être définies sans l'utilisation d'une quantification infinie; seules des jonctions infinies sont nécessaires.

Logiques infinitaires complètes

Deux logiques infinitaires se distinguent par leur exhaustivité. Ce sont et . La première est une logique finitaire standard du premier ordre et la seconde est une logique infinitaire qui n'autorise que des déclarations de taille dénombrable. ${\ displaystyle L _ {\ omega, \ omega}}$${\ displaystyle L _ {\ omega _ {1}, \ omega}}$

${\ displaystyle L _ {\ omega, \ omega}}$ est également très complet, compact et fortement compact.

${\ displaystyle L _ {\ omega _ {1}, \ omega}}$ échoue à être compact, mais il est complet (sous les axiomes donnés ci-dessus). De plus, il satisfait une variante de la propriété d' interpolation de Craig .

Si est fortement complet (sous les axiomes donnés ci-dessus) alors est fortement compact (parce que les preuves dans ces logiques ne peuvent pas utiliser ou plus des axiomes donnés). ${\ displaystyle L _ {\ alpha, \ alpha}}$${\ displaystyle \ alpha}$${\ displaystyle \ alpha}$

Les références

• Karp, Carol R. (1964), Languages ​​with expressions of infinite length , Amsterdam: North-Holland Publishing Co., MR   0176910
• Barwise, Kenneth Jon (1969), "Logique infinitaire et ensembles admissibles", Journal of Symbolic Logic , 34 (2): 226–252, doi : 10.2307 / 2271099 , JSTOR   2271099 , MR   0406760