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 modifier

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  . Cela 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

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

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

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

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

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

Bibliographie modifier