Logique infinitaire

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

Une logique infinitaire est une logique qui permet des formules infiniment longues et/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[modifier | modifier le code]

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. «  » 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  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 suite infinie de quantificateurs pour chaque  où .

Les suffixes et les «  » 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[modifier | modifier le code]

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  alors  et  sont des formules. (dans chaque cas, la formule est de longueur .)
  • Étant donné un ensemble de variables et une formule  alors  et  sont des formules. (dans chaque cas, la suite de quantificateurs est de longueur .)

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  est un ensemble de formules. Une preuve dans la logique infinitaire d'une théorie T est une suite d'énoncés de longueur  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  ayant déjà existé précédemment dans la preuve, alors l'énoncé 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 : et  tel que .

  • Pour chaque ,
  • Loi de distributivité de Chang (pour chaque ): , où  ou , et 
  • Pour , , où  est un ensemble bien ordonné de 

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é[modifier | modifier le code]

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  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  est faiblement compact quand pour chaque théorie T dans  contenant au plus  formules, si tout S T de cardinalité inférieure  a un modèle, alors T a un modèle. Un cardinal  est fortement compact quand pour chaque théorie T in , sans restriction de taille, si chaque S T de cardinalité inférieure à a un modèle, alors T a un modèle.

Concepts expressibles en logique infinitaire[modifier | modifier le code]

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

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[modifier | modifier le code]

Deux logiques infinitaires se distinguent dans leur complétude. Celles-ci sont  et . 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.

est également fortement complète, compacte et fortement compacte.

 n'est pas compacte, mais est complète. En outre, elle satisfait une variante de la propriété d'interpolation de Craig.

Si  est fortement complète, alors  est fortement compacte.

Notes et références[modifier | modifier le code]

  1. Notion formelle correspondant à la notion informelle de « vérité »

Bibliographie[modifier | modifier le code]