Logique Infinitaire

Table des matières:

Logique Infinitaire
Logique Infinitaire

Vidéo: Logique Infinitaire

Vidéo: Logique Infinitaire
Vidéo: 1ère bac : la logique -- partie 1-- 2024, Mars
Anonim

Navigation d'entrée

  • Contenu de l'entrée
  • Bibliographie
  • Outils académiques
  • Aperçu du PDF des amis
  • Informations sur l'auteur et la citation
  • Retour au sommet

Logique infinitaire

Publié pour la première fois le 23 janvier 2000; révision de fond ven 26 févr.2016

Traditionnellement, les expressions dans les systèmes formels ont été considérées comme signifiant des inscriptions finies qui sont - au moins en principe - susceptibles d'être effectivement écrites en notation primitive. Cependant, le fait que les formules (du premier ordre) puissent être identifiées avec des nombres naturels (via la «numérotation de Gödel») et donc avec des ensembles finis rend plus nécessaire de considérer les formules comme des inscriptions, et suggère la possibilité de façonner des «langages» certains dont les formules seraient naturellement identifiées comme des ensembles infinis. Un «langage» de ce genre est appelé un langage infinitaire: dans cet article je discute ces langages infinitaires qui peuvent être obtenus de manière directe à partir des langages du premier ordre en permettant aux conjonctions, disjonctions et, éventuellement, séquences quantifiantes, d'être infinies. longueur. Au cours de la discussion, on verra que, si le pouvoir expressif de telles langues dépasse de loin celui de leurs homologues finitaires (de premier ordre), très peu d'entre eux possèdent les caractéristiques «attractives» (par exemple, la compacité et l'exhaustivité) de le dernier. En conséquence, les langues infinitaires qui possèdent en fait ces caractéristiques méritent une attention particulière.

Au §1, la syntaxe et la sémantique de base des langages infinitaires sont énoncées; leur pouvoir expressif est alors affiché au moyen d'exemples. Le §2 est consacré à ces langages infinitaires qui ne permettent que des séquences de quantification finies: ces langages s'avèrent relativement bien élevés. Le §3 est consacré à une discussion du problème de la compacité pour les langages infinitaires et de sa connexion avec des questions purement théoriques des ensembles concernant les «grands» nombres cardinaux. Au §4, un argument est esquissé qui montre que la plupart des langages «quantificateurs infinis» ont une nature de second ordre et sont ipso facto très incomplets. Le § 5 donne un bref compte rendu d'une certaine classe spéciale de sous-langues de langues infinitaires pour lesquelles une généralisation satisfaisante du théorème de compacité peut être démontrée. Cette section comprend une sous-section sur la définition des ensembles admissibles. Des remarques historiques et bibliographiques sont fournies au §6.

  • 1. Définition et propriétés de base des langages infinitaires
  • 2. Langages à quantificateur fini
  • 3. La propriété Compactness
  • 4. Incomplétude des langages quantificateurs infinis
  • 5. Sous-langages de L (ω 1, ω) et du théorème de la compacité à barres

    5.1 Définition du concept d'ensemble admissible

  • 6. Remarques historiques et bibliographiques
  • Bibliographie
  • Outils académiques
  • Autres ressources Internet
  • Entrées connexes

1. Définition et propriétés de base des langages infinitaires

Étant donné un couple κ, λ de cardinaux infinis tels que λ ≤ κ, on définit une classe de langages infinitaires dans chacun desquels on peut former des conjonctions et des disjonctions d'ensembles de formules de cardinalité <κ, et des quantifications sur des suites de variables de longueur < λ.

Soit L - le langage de base (finitaire) - un langage arbitraire mais fixe du premier ordre avec n'importe quel nombre de symboles extralogiques. Le langage infinitaire L (κ, λ) a les symboles de base suivants:

  • Tous les symboles de L
  • Un ensemble Var de variables individuelles, où la cardinalité de Var (écrite: | Var |) est κ
  • Un opérateur logique ∧ (conjonction infinitaire)

La classe des préformules de L (κ, λ) est définie récursivement comme suit:

  • Chaque formule de L est une préformule;
  • si φ et ψ sont des préformules, il en est de même pour φ∧ψ et ¬φ;
  • si Φ est un ensemble de préformules telles que | Φ | <κ, alors ∧Φ est une préformule;
  • si φ est une préformule et X ⊆ Var est tel que | X | <λ, alors ∃ X φ est une préformule;
  • toutes les préformules sont définies par les clauses ci-dessus.

Si Φ est un ensemble de préformules indexées par un ensemble I, disons Φ = {φ i: i ∈ I}, alors nous acceptons d'écrire ∧Φ pour:

i ∈ I  φ

ou, si I est l'ensemble des nombres naturels, on écrit ∧Φ pour:

φ 0 ∧ φ 1 ∧…

Si X est un ensemble de variables individuelles indexées par un ordinal α, disons X = {x ξ: ξ <α}, nous acceptons d'écrire (∃ x ξ) ξ <α φ pour ∃ X φ.

Les opérateurs logiques ∨, →, ↔ sont définis de la manière habituelle. Nous introduisons également les opérateurs ∨ (disjonction infinitaire) et ∀ (quantification universelle) par

∨Φ = df ¬∧ {¬φ: φ ∈ Φ}

∀Xφ = df ¬∃X¬φ,

et utilisent des conventions similaires à celles de ∧, ∃.

Ainsi L (κ, λ) est le langage infinitaire obtenu à partir de L en permettant des conjonctions et disjonctions de longueur <κ et des quantifications [1] de longueur <λ. Les langages L (κ, ω) sont appelés langages à quantificateur fini, les autres langages à quantificateur infini. Observez que L (ω, ω) est juste L lui-même.

Notez l'anomalie suivante qui peut survenir dans un langage infinitaire mais pas dans un langage finitaire. Dans le langage L (ω 1, ω), qui permet des conjonctions infinies dénombrables mais seulement des quantifications finies, il existe des préformules avec tellement de variables libres qu'elles ne peuvent pas être «fermées» en phrases de L (ω 1, ω) en préfixant des quantificateurs. Tel est le cas, par exemple, pour la L (ω 1, ω) -préformule

x 0 <x 1 ∧ x 1 <x 2 ∧… ∧ x n <x n +1 …,

où L contient le symbole de relation binaire <. Pour cette raison, nous faisons ce qui suit

Définition. Une formule de L (κ, λ) est une préformule qui contient <λ variables libres. L'ensemble de toutes les formules de L (κ, λ) sera noté Form (L (κ, λ)) ou simplement Form (κ, λ) et l'ensemble de toutes les phrases par Sent (L (κ, λ)) ou simplement envoyé (κ, λ).

A ce propos, notons qu'en général, on ne gagnerait rien à considérer des «langages» L (κ, λ) avec λ> κ. Par exemple, dans le «langage» L (ω, ω 1), les formules n'auront qu'un nombre fini de variables libres, alors qu'il y aura une foule de quantificateurs «inutiles» capables de lier une infinité de variables libres. [2]

Après avoir défini la syntaxe de L (κ, λ), nous en esquissons ensuite la sémantique. Puisque les symboles extralogiques de L (κ, λ) ne sont que ceux de L, et que ce sont ces symboles qui déterminent la forme des structures dans lesquelles un langage donné du premier ordre doit être interprété, il est naturel de définir un L (κ, λ) -structure pour être simplement une L-structure. La notion d'une formule de L (κ, λ) étant satisfaite dans une L-structure A (par une suite d'éléments du domaine de A) est définie de la même manière inductive que pour les formules de L sauf qu'il faut ajouter deux les clauses supplémentaires correspondant aux clauses pour ∧Φ et ∃Xφ dans la définition des préformules. Dans ces deux cas, on définit naturellement:

∧Φ est satisfaite dans A (par une suite donnée) ⇔ pour tout φ ∈ Φ, φ est satisfaite dans A (par la suite);

∃ X φ est satisfaite dans un ⇔ il existe une séquence d'éléments du domaine de A en correspondance bijective avec X qui satisfait à & phiv A.

Ces définitions informelles doivent être resserrées dans un développement rigoureux, mais leur signification doit être claire pour le lecteur. Maintenant, les notions habituelles de vérité, de validité, de satisfiabilité et de modèle pour les formules et les phrases de L (κ, λ) deviennent disponibles. En particulier, si A est une L-structure et σ ∈ Sent (κ, λ), on écrira A ⊨ σ car A est un modèle de σ, et ⊨ σ pour σ est valide, c'est-à-dire pour tout A, A ⊨ σ. Si Δ ⊆ Sent (κ, λ), on écrira Δ ⊨ σ car σ est une conséquence logique de Δ, c'est-à-dire que chaque modèle de Δ est un modèle de σ.

Nous donnons maintenant quelques exemples destinés à afficher la puissance expressive des langages infinitaires L (κ, λ) avec κ ≥ ω 1. Dans chaque cas, il est bien connu que la notion en question ne peut être exprimée dans aucune langue de premier ordre.

Caractérisation du modèle standard de l'arithmétique en L (ω 1, ω). Ici, le modèle standard de l'arithmétique est la structure N = ⟨N, +, ·, s, 0⟩, où N est l'ensemble des nombres naturels, +, · et 0 ont leurs significations habituelles, et s est l'opération successeur. Soit L le premier ordre approprié de langue pour N. Alors la classe des L-structures isomorphes à N coïncide avec la classe des modèles de la conjonction des phrases L (ω 1, ω) suivantes (où 0 est un nom de 0):

m ∈ωn ∈ω s m 0 + s n 0 = s m + n 0

m ∈ωn ∈ω s m 0 · s n 0 = s m · n 0

m ∈ωn ∈ω− {m} s m 0 ≠ s n 0

∀ x ∨ m ∈ω x = s m 0

Les termes s n x sont définis récursivement par

s 0 x = X
s n +1 x = s (s n x)

Caractérisation de la classe de tous les ensembles finis dans L (ω 1, ω). Ici, la langue de base n'a pas de symboles extralogiques. La classe de tous les ensembles finis coïncide alors avec la classe des modèles de la L (ω 1, ω) -sentence

n ∈ω ∃ v 0 … ∃ v n ∀ x (x = v 0 ∨… ∨ x = v n).

Définition de la vérité en L (ω 1, ω) pour un langage de base dénombrable L. Soit L un langage dénombrable du premier ordre (par exemple, le langage de l'arithmétique ou de la théorie des ensembles) qui contient un nom n pour chaque nombre naturel n, et soit σ 0, σ 1,… une énumération de ses phrases. Alors la formule L (ω 1, ω)

Tr (x) = dfn ∈ω (x = n ∧ σ n)

est un prédicat de vérité pour L dans la mesure où la phrase

Tr (n) ↔ σ n

est valable pour chaque n.

Caractérisation des ordres de puits dans L (ω 1, ω 1). Le langage de base L comprend ici un symbole de prédicat binaire ≤. Soit σ 1 les phrases L habituelles caractérisant les ordres linéaires. Alors la classe des L-structures dans lesquelles l'interprétation de ≤ est un bon ordre coïncide avec la classe des modèles de la phrase L (ω 1, ω 1) σ = σ 1 ∧ σ 2, où

σ 2 = df (∀ v n) n ∈ω ∃ x [∨ n ∈ω (x = v n) ∧ ∧ n ∈ω (x ≤ v n)].

Remarquez que la phrase σ 2 contient un quantificateur infini: elle exprime l'assertion essentiellement du second ordre selon laquelle chaque sous-ensemble dénombrable a un plus petit membre. On peut en effet montrer que la présence de ce quantificateur infini est essentielle: la classe des structures bien ordonnées ne peut être caractérisée dans aucun langage quantificateur fini. Cet exemple indique que les langages à quantification infinie tels que L (ω 1, ω 1) se comportent plutôt comme des langages du second ordre; nous verrons qu'ils partagent les défauts de ces derniers (incomplétude) ainsi que certains de leurs avantages (fort pouvoir expressif).

De nombreuses extensions de langues de premier ordre peuvent être traduites dans des langues infinies. Par exemple, considérons le langage de quantificateur généralisé L (Q 0) obtenu à partir de L en ajoutant un nouveau symbole de quantificateur Q 0 et en interprétant Q 0 x φ (x) car il existe une infinité de x tels que φ (x). On voit facilement que la phrase Q 0 x φ (x) a les mêmes modèles que la L (ω 1, ω) -sentence

¬∨ n ∈ω ∃ v 0 … ∃ v n ∀ x [φ (x) → (x = v 0 ∨… ∨ x = v n)].

Ainsi L (Q 0) est, au sens naturel, traduisible en L (ω 1, ω). Un autre langage traduisible en L (ω 1, ω) dans ce sens est le langage faible du second ordre obtenu en ajoutant un ensemble dénombrable de variables de prédicat monadique à L qui sont alors interprétées comme s'étendant sur tous les ensembles finis d'individus.

Des langages avec des conjonctions, disjonctions et (éventuellement) quantifications arbitrairement longues peuvent également être introduits. Pour un cardinal infini fixe λ, le langage L (∞, λ) est défini en spécifiant sa classe de formules, Forme (∞, λ), pour être l'union, sur tout κ ≥ λ, des ensembles Forme (κ, λ)). Ainsi L (∞, λ) autorise des conjonctions et disjonctions arbitrairement longues, en ce sens que si Φ est un sous-ensemble arbitraire de la forme (∞, λ), alors ∧Φ et ∨Φ sont tous deux membres de la forme (∞, λ). Mais L (∞, λ) n'admet que des quantifications de longueur <λ: toutes ses formules ont <λ variables libres. Le langage L (∞, ∞) est défini à son tour en spécifiant sa classe de formules, Forme (∞, ∞), pour être l'union, sur tous les cardinaux infinis λ, des classes Forme (∞, λ). Donc L (∞, ∞) permet des quantifications arbitrairement longues en plus de conjonctions et disjonctions arbitrairement longues. Notez que la forme (∞, λ) et la forme (∞, ∞) sont des classes propres au sens de la théorie des ensembles de Gödel-Bernays. La satisfaction des formules de L (∞, λ) et L (∞, ∞) dans une structure peut être définie par une extension évidente de la notion correspondante pour L (κ, λ).

2. Langages à quantificateur fini

Nous avons remarqué que les langages quantificateurs infinis tels que L (ω 1, ω 1) ressemblent aux langages du second ordre dans la mesure où ils permettent une quantification sur des ensembles infinis d'individus. Le fait que cela ne soit pas autorisé dans les langages à quantificateurs finis suggère que ceux-ci peuvent être à certains égards plus proches de leurs homologues du premier ordre que ce qui pourrait être évident à première vue. Nous verrons que c'est bien le cas, notamment dans le cas de L (ω 1, ω).

La langue L (ω 1, ω) occupe une place particulière parmi les langues infinitaires car, comme les langues du premier ordre, elle admet un appareil déductif efficace. En fait, ajoutons aux axiomes et règles d'inférence habituels du premier ordre le nouveau schéma d'axiomes

∧Φ → φ

pour tout ensemble dénombrable Φ ⊆ Forme1, ω) et tout φ ∈ Φ, avec la nouvelle règle d'inférence

φ 0, φ 1,…, φ n,…
n ∈ω φ n

et permettre aux déductions d'être de longueur dénombrable. En écrivant ⊢ * pour la déductibilité en ce sens, on a alors le

L (ω 1, ω) - Théorème de complétude. Pour tout σ ∈ Envoyé1, ω), ⊨ σ ⇔ ⊢ * σ

Comme corollaire immédiat, nous en déduisons que cet appareil déductif est adéquat pour les déductions d'ensembles dénombrables de prémisses dans L (ω 1, ω). Autrement dit, avec l'extension évidente de la notation, nous avons, pour tout ensemble dénombrable Δ ⊆ Sent1, ω)

(2,1) Δ ⊨ σ ⇔ Δ⊢ * σ

Ce théorème d'exhaustivité peut être prouvé en modifiant la preuve d'exhaustivité habituelle de Henkin pour la logique du premier ordre, ou en employant des méthodes booléennes algébriques. Des arguments similaires, appliqués à d'autres augmentations appropriées des axiomes et des règles d'inférence, donnent des théorèmes d'exhaustivité analogues pour de nombreux autres langages à quantificateurs finis.

Si de simples déductions de longueur dénombrable sont admises, alors aucun appareil déductif pour L (ω 1, ω) ne peut être mis en place qui soit adéquat pour les déductions d'ensembles arbitraires de prémisses, c'est-à-dire pour lesquels (2.1) serait valable pour tout ensemble Δ ⊆ Envoyé1, ω), quelle que soit la cardinalité. Cela découle de la simple observation qu'il existe un langage L du premier ordre et un ensemble indénombrable Γ de L (ω 1, ω) -sentences tels que Γ n'a pas de modèle mais que chaque sous-ensemble dénombrable de Γ en a. Pour voir cela, soit L le langage de l'arithmétique augmenté de ω 1 nouveaux symboles constants { c ξ: ξ <ω 1 } et soit Γ l'ensemble des L (ω 1, ω) -sentences {σ} ∪ { cξc η: ξ ≠ η}, où σ est la L (ω 1, ω) -sentence caractérisant le modèle standard de l'arithmétique. Cet exemple montre également que le théorème de compacité échoue pour L (ω 1, ω) et donc aussi pour tout L (κ, λ) avec κ ≥ ω 1.

Un autre résultat qui tient dans le cas du premier ordre mais échoue pour L (κ, ω) avec κ ≥ ω 1 (et aussi pour L (ω 1, ω 1), bien que cela soit plus difficile à prouver) est la forme normale du prénex théorème. Une phrase est prenex si tous ses quantificateurs apparaissent au début; nous donnons un exemple d'une L (ω 1, ω) -sentence qui n'est pas équivalente à une conjonction de phrases prénex. Soit L le langage du premier ordre sans symboles extralogiques et soit σ la L (ω 1, ω) -sentence qui caractérise la classe des ensembles finis. Supposons que σ équivaut à une conjonction

i ∈ je σ i

de prénex L (ω 1, ω) -sentences σ i. Alors chaque σ i est de la forme

Q 1 x 1 … Q n x n φ i (x 1,…, x n),

où chaque Q k est ∀ ou ∃ et φ i est une conjonction ou disjonction (éventuellement infinitaire) de formules de la forme x k = x l ou x k ≠ x l. Puisque chaque σ i est une phrase, il n'y a qu'une infinité de variables dans chaque φ i, et il est facile de voir que chaque φ i est alors équivalent à une formule du premier ordre. En conséquence, chaque σ i peut être considéré comme une phrase du premier ordre. Puisque σ est supposé équivalent à la conjonction de σ i, il s'ensuit que σ et l'ensemble Δ = {σ i: i ∈ I} ont les mêmes modèles. Mais évidemment σ, et donc aussi Δ, ont des modèles de toutes les cardinalités finies; le théorème de compacité pour les ensembles de phrases du premier ordre implique maintenant que Δ, et donc aussi σ, a un modèle infini, contredisant la définition de σ.

En nous tournant vers le théorème de Löwenheim-Skolem, nous trouvons que la version descendante a des généralisations adéquates à L (ω 1, ω) (et, en fait, à toutes les langues infinitaires). En fait, on peut montrer à peu près de la même manière que pour les ensembles de phrases du premier ordre que si Δ ⊆ Sent1, ω) a un modèle infini de cardinalité ≥ | Δ |, il a un modèle de cardinalité le plus grand de ℵ 0, | Δ |. En particulier, toute L (ω 1, ω) -sentence avec un modèle infini a un modèle dénombrable.

D'autre part, le théorème ascendant de Löwenheim-Skolem dans sa forme habituelle échoue pour toutes les langues infinitaires. Par exemple, la L (ω 1, ω) -sentence caractérisant le modèle standard de l'arithmétique a un modèle de cardinalité ℵ 0 mais aucun modèle d'une autre cardinalité. Cependant, tout n'est pas perdu ici, comme nous le verrons.

On définit le nombre de Hanf h (L) d'un langage L comme étant le plus petit cardinal κ tel que, si une L -sentence a un modèle de cardinalité κ, elle a des modèles de cardinalité arbitrairement grande. L'existence de h (L) est facilement établie. Pour chaque L -sentence σ ne possédant pas de modèles de cardinalité arbitrairement grande soit κ (σ) le plus petit cardinal κ tel que σ n'ait pas de modèle de cardinalité κ. Si λ est le supremum de tous les κ (σ), alors, si une phrase de L a un modèle de cardinalité λ, elle a des modèles de cardinalité arbitrairement grande.

Définir les cardinaux μ (α) récursivement par

μ (0) = 0
μ (α + 1) = 2 μ (α)
μ (λ) = α <λ μ (α), pour la limite λ.

Ensuite, on peut montrer que

h (L (ω 1, ω)) = μ (ω 1),

des résultats similaires pour d’autres langages de quantificateurs finis. Les valeurs des nombres Hanf des langages quantificateurs infinis tels que L (ω 1, ω 1) sont sensibles à la présence ou non de grands cardinaux, mais doivent en tout cas largement dépasser celle de L (ω 1, ω).

Un résultat pour L qui se généralise à L (ω 1, ω) mais à aucun autre langage infinitaire est le

Théorème d'interpolation de Craig: Si σ, τ ∈ Sent1, ω) sont tels que ⊨ σ → τ, alors il y a θ ∈ Sent1, ω) tel que ⊨ σ → θ et ⊨ θ → τ, et chacun le symbole extralogique apparaissant dans θ apparaît à la fois dans σ et τ.

La preuve est une extension raisonnablement simple du cas du premier ordre.

Enfin, nous mentionnons un autre résultat qui se généralise bien à L (ω 1, ω) mais à aucun autre langage infinitaire. Il est bien connu que, si A est une L-structure finie avec seulement un nombre fini de relations, il existe une L-phrase σ caractérisant A jusqu'à l'isomorphisme. Pour L (ω 1, ω), nous avons la généralisation suivante connue sous le nom de

Théorème de l'isomorphisme de Scott. Si A est une dénombrable L structure avec seulement comptablement beaucoup de relations, alors il y a un L (ω 1, ω) -sentence dont la classe de modèles dénombrables coïncide avec la classe des structures L-isomorphes A.

La restriction aux structures dénombrables est essentielle car la dénombrabilité ne peut en général être exprimée par une L (ω 1, ω) -sentence.

Le langage L (∞, ω) peut également être compté comme un langage à quantificateur fini. Le concept d'équivalence des structures par rapport à ce langage a une signification particulière: on appelle deux structures (similaires) A et B (∞, ω) - équivalentes, écrites A∞ω B, si les mêmes phrases de L (∞, ω) en prise à la fois A et B. Cette relation peut tout d'abord être caractérisée par la notion d'isomorphisme partiel. Un isomorphisme partiel entre A et B est une famille P non vide de cartes telle que:

  • Pour chaque p ∈ P, dom (p) est une sous-structure de A, ran (p) est une sous-structure de B, et p est un isomorphisme de son domaine sur son domaine; et
  • Si p ∈ P, a ∈ A, b ∈ B, alors il existe r, s ∈ P étendant tous les deux p tels que a ∈ dom (r), b ∈ run (s) (propriété «va-et-vient»).

Si un isomorphisme partiel existe entre A et B, nous disons que A et B sont partiellement isomorphes et écriture Ap B. Nous avons alors

Théorème de l'isomorphisme partiel de Karp.

Pour toutes les structures semblables A, B, A∞ω BA de p B.

Il existe également une version du théorème d'isomorphisme de Scott pour L (∞, ω), à savoir,

(2.2) Étant donné toute structure A, il existe une L (∞, ω) -sentence σ telle que, pour toutes les structures B, Ap BB ⊨ σ.

L'isomorphisme partiel et l'équivalence (∞, ω) sont liés à la notion d'isomorphisme booléen. Pour définir cela, nous devons introduire l'idée d'un modèle de théorie des ensembles à valeurs booléennes. Étant donné une algèbre booléenne B complète, l'univers V (B) des ensembles à valeurs B, également appelé extension B de l'univers V des ensembles, est obtenu en définissant d'abord, récursivement sur α,

V α (B) = {x: x est une fonction ∧ range (x) ⊆ B ∧ ∃ξ <α [domain (x) ⊆ V ξ (B)]}

puis définissant

V (B) = {x: ∃α (x ∈ V α (B))}.

Les membres de V (B) sont appelés ensembles à valeur B. On voit maintenant facilement qu'un ensemble de valeurs B est précisément une fonction de valeurs B avec un domaine un ensemble d'ensembles de valeurs B. Soit maintenant L le langage du premier ordre de la théorie des ensembles et soit L (B) le langage obtenu en ajoutant à L un nom pour chaque élément de V (B) (nous utiliserons le même symbole pour l'élément et son nom). On peut maintenant construire une application [·] (B) des (phrases du) langage L (B) en B: pour chaque phrase σ de L (B), l'élément [σ] (B) de B est le " Valeur de vérité booléenne »de σ dans V (B). Cette application [·] (B) est définie de manière à envoyer tous les théorèmes de la théorie des ensembles de Zermelo-Fraenkel à l'élément supérieur 1 de B, c'est-à-dire à la «vérité»; en conséquence, V (B) peut être considéré comme un modèle de théorie des ensembles à valeurs booléennes. En général, si [σ] (B) = 1, on dit que σ est valide dans V (B), et on écrit V (B) ⊨ σ.

Maintenant, chaque x ∈ V a un représentant canonique x dans V (B), satisfaisant

x = y ssi V (B) ⊨ x = y

x ∈ y ssi V (B) ⊨ x ∈ y

On dit que deux structures similaires A, B sont booléennes isomorphes, écrites Ab B, si, pour une algèbre booléenne B complète, on a V (B)AB, c'est-à-dire s'il y a une extension booléenne du univers d'ensembles dans lequel les représentants canoniques de A et B sont isomorphes de valeur booléenne 1. On peut alors montrer que:

(2,3) A∞ω BAb B.

Ce résultat peut être renforcé par la formulation de la théorie des catégories. Pour cela, nous avons besoin du concept de topos (n) (élémentaire). Pour introduire ce concept, nous commençons par la catégorie familière des ensembles d'ensembles et de mappages. L'ensemble a les propriétés clés suivantes:

  1. Il existe un objet «terminal» 1 tel que, pour tout objet X, il y ait une application unique X → 1 (pour 1 on peut prendre tout ensemble à un élément, en particulier, {0}).
  2. Toute paire d'objets X, Y a un produit cartésien X × Y.
  3. pour n'importe quelle paire d'objets on peut former l'objet «exponentiel» Y X de toutes les cartes de X → Y.
  4. Il existe un objet «valeur de vérité» Ω tel que pour chaque objet X il existe une correspondance naturelle entre les sous-objets (sous-ensembles) de X et les applications X → Ω. (Pour Ω on peut prendre l'ensemble 2 = {0,1}; les applications X → Ω sont alors des fonctions caractéristiques sur X.)

Ces quatre conditions peuvent être formulées dans un langage théorique des catégories - une catégorie qui les satisfait est appelée un topos. La catégorie Set est un topos; il en est de même (i) de la catégorie Ensemble (B) des ensembles et des mappages à valeur booléenne dans toute extension booléenne V (B) de l'univers des ensembles; (ii) la catégorie des faisceaux d'ensembles sur un espace topologique; (iii) la catégorie de tous les diagrammes de cartes d'ensembles

X 0 → X 1 → X 2 →…

Les objets de chacune de ces catégories peuvent être considérés comme des ensembles qui varient d'une certaine manière: dans le cas (i) sur une algèbre booléenne; dans le cas (ii) sur un espace topologique; dans le cas (iii) sur un temps (discret). Un topos peut donc être conçu comme un univers d'ensembles «variables». La catégorie familière Set est le cas particulier limite d'un topos dans lequel la «variation» des objets a été réduite à zéro.

Tout comme dans la théorie des ensembles, des «opérateurs logiques» peuvent être définis sur l'objet de valeur de vérité dans n'importe quel topos. Ce sont des cartes ¬: Ω → Ω; ∧, ∨, ⇒: Ω × Ω → Ω correspondant aux opérations logiques de négation, conjonction, disjonction et implication. Avec ces opérations, Ω devient une algèbre de Heyting, incarnant ainsi en général les lois non pas de la logique classique mais de la logique intutionniste. En ce sens, la logique intuitionniste est «internalisée» dans un topos: la logique intuitionniste est la logique des ensembles de variables. (Bien sûr, la logique classique est internalisée dans certains objets, par exemple Set et Set (B) pour toute algèbre booléenne complète B.)

Tout topos peut être conçu comme un possible «univers du discours» dans lequel des assertions mathématiques peuvent être interprétées et des constructions mathématiques peuvent être exécutées. Les assertions mathématiques sont rendues interprétables dans un topos E par une expression dans le langage interne de E - une version théorique des types du langage habituel de la théorie des ensembles. De manière analogue à la validité à valeur booléenne, on peut introduire une notion appropriée de validité en E d'une phrase σ de son langage interne. Encore une fois, nous écrivons E ⊨ σ pour «σ est valide dans E».

Un topos E est dit plein si, pour tout ensemble I, le copower I-plié [3]I 1 de son objet terminal existe dans E. ∐ I 1 peut être considéré comme le représentant canonique en E de l'ensemble JE; en conséquence, nous l'écrivons simplement comme je. (En V (B) cela coïncide avec I tel que défini précédemment.) Tous les objets mentionnés ci-dessus sont pleins.

Soit maintenant E un topos complet. Si A = (A, R,…) est une structure, écrivez A pour (A, R,…). Deux structures A et B sont dites topos isomorphes, notées At B, si, pour un topos E défini sur la catégorie des ensembles, on a E ⊨ A ≅ B. En d'autres termes, deux structures sont topos isomorphes si leurs représentants canoniques sont isomorphes dans le langage interne de certains topos. On peut alors montrer que

(2,4) A∞ω BAt B.

Par conséquent, l'équivalence (∞, ω) peut être considérée comme un isomorphisme dans le contexte extrêmement général des univers d'ensembles «variables». A cet égard, l'équivalence (∞, ω) est une notion «invariante» d'isomorphisme.

3. La propriété Compactness

Comme nous l'avons vu, le théorème de compacité dans sa forme habituelle échoue pour tous les langages infinitaires. Néanmoins, il est d'un certain intérêt de déterminer si les langages infinitaires satisfont à une version convenablement modifiée du théorème. Ce soi-disant problème de compacité s'avère avoir un lien naturel avec des questions purement théoriques des ensembles impliquant des nombres cardinaux «grands».

Nous construisons la définition suivante. Soit κ un cardinal infini. Un langage L est dit κ- compact (resp. Faiblement κ-compact) si chaque fois que Δ est un ensemble de L -sentences (resp. Un ensemble de L -sentences de cardinalité ≤ κ) et chaque sous-ensemble de Δ de cardinalité < κ a un modèle, ainsi que Δ. Notez que le théorème de compacité habituel pour L est précisément l'affirmation que L est ω-compact. Une raison pour accorder une signification à la propriété κ-compacité est la suivante. Appelons L κ- complet (resp. Faiblement κ- complet) s'il existe un système déductif P pour L avec des déductions de longueur <κ telles que, si Δ est un ensemble P- cohérent [4] de L -sentences (resp. Telles que | Δ | ≤ κ), alors Δ a un modèle. Observez qu'un tel P sera adéquat pour les déductions d'ensembles arbitraires de prémisses (de cardinalité ≤ κ) au sens du §2. On voit facilement que si L est κ-complet ou faiblement κ-complet, alors L est κ-compact ou faiblement κ-compact. Ainsi, si nous pouvons montrer qu'une langue donnée n'est pas (faiblement) κ-compacte, alors il ne peut y avoir de système déductif pour elle avec des déductions de longueur <κ adéquates pour les déductions d'ensembles arbitraires de prémisses (de cardinalité ≤ κ).

Il s'avère, en fait, que la plupart des langages L (κ, λ) ne sont pas même faiblement κ-compacts, et, pour ceux qui le sont, κ doit être un cardinal extrêmement grand. Nous aurons besoin de quelques définitions.

Un cardinal infini κ est dit faiblement inaccessible si

(a) λ <κ → λ + <κ, (où λ + désigne le successeur cardinal de λ), et

(b) | I | <κ et λ i <κ (pour tout i ∈ I) ⇒ ∑ i ∈ I λ i <κ.

Si en plus

(c) λ <κ ⇒ 2 λ <κ,

alors κ est dit (fortement) inaccessible. Puisque ℵ 0 est inaccessible, il est normal de limiter l'attention sur les cardinaux inaccessibles ou faiblement inaccessibles qui dépassent ℵ 0. En conséquence, les cardinaux inaccessibles ou faiblement inaccessibles seront toujours considérés comme indénombrables. Il est clair que ces cardinaux - s'ils existent - doivent être extrêmement grands; et en effet le théorème d'incomplétude de Gödel implique que l'existence de cardinaux même faiblement inaccessibles ne peut être prouvée à partir des axiomes habituels de la théorie des ensembles.

Appelons un cardinal κ compact (resp. Faiblement compact) si le langage L (κ, κ) est κ-compact (resp. Faiblement κ-compact). Ensuite, nous avons les résultats suivants:

(3.1) ℵ 0 est compact. C'est, bien sûr, juste une manière succincte d'exprimer le théorème de compacité pour les langages du premier ordre.

(3.2) κ est faiblement compact ⇒ L (κ, ω) est faiblement κ- compact ⇒ κ est faiblement inaccessible. En conséquence, il est cohérent (avec les axiomes usuels de la théorie des ensembles) de supposer qu'aucun langage L (κ, ω) avec κ ≥ ω 1 n'est faiblement κ-compact, ou, a fortiori, faiblement κ-complet.

(3.3) Supposons que κ soit inaccessible. Alors κ est faiblement compact ⇔ L (κ, ω) est faiblement κ- compact. Aussi, aussi κ est faiblement compact ⇒ il y a un ensemble de κ inaccessibles avant κ. Ainsi, un cardinal inaccessible faiblement compact est extrêmement grand; en particulier, il ne peut pas être le premier, le deuxième,…, le nième,… inaccessible.

(3.4) κ est compact ⇒ κ est inaccessible. (Mais, par le résultat immédiatement ci-dessus, l'inverse échoue.)

Soit Constr pour l'axiome de constructibilité de Gödel; rappelons que Constr est cohérent avec les axiomes habituels de la théorie des ensembles.

(3.5) Si Constr tient, alors il n'y a pas de cardinaux compacts.

(3.6) Supposons Constr et soit κ inaccessible. Alors κ est faiblement compact ⇔ L (ω 1, ω) est faiblement κ- compact pour tout L.

(3.7) Si Constr tient, alors il n'y a pas de cardinaux κ pour lesquels L (ω 1, ω) est compact. En conséquence, il est cohérent avec les axiomes habituels de la théorie des ensembles de supposer qu'il n'y a pas de cardinal κ tel que tous les langages L (ω 1, ω) soient κ-complets. Ce résultat doit être mis en contraste avec le fait que tous les langages du premier ordre sont ω-complets.

L'intérêt de ces résultats est que le théorème de compacité échoue très mal pour la plupart des langages L (κ, λ) avec κ ≥ ω 1.

Quelques remarques historiques s'imposent ici. Dans les années 1930, les mathématiciens ont étudié diverses versions du soi-disant problème de mesure pour les ensembles, problème qui s'est posé à propos de la théorie de la mesure de Lebesgue sur le continuum. En particulier, la notion très simple de mesure suivante a été formulée. Si X est un ensemble, une mesure (non triviale à deux valeurs additive dénombrable) sur X est une application μ sur l'ensemble de puissances P X à l'ensemble {0, 1} satisfaisant:

(a) μ (X) = 1, (b) μ ({x}) = μ (∅) = 0 pour tout x ∈ X, et

(c) si A est une famille dénombrable de sous-ensembles mutuellement disjoints de X, alors μ (∪ A) = ∑ {μ (Y): Y ∈ A }.

Évidemment, le fait qu'un ensemble donné supporte une telle mesure ne dépend que de sa cardinalité, il est donc naturel de définir un cardinal κ pour être mesurable si tous les ensembles de cardinalité κ supportent une mesure de ce type. On s'est vite rendu compte qu'un cardinal mesurable devait être inaccessible, mais la fausseté de l'inverse n'a été établie que dans les années 1960 lorsque Tarski a montré que les cardinaux mesurables sont faiblement compacts et que son élève Hanf a montré que les premier, deuxième, etc. inaccessibles ne sont pas faiblement inaccessibles. compact (cf. (3.3)). Si la conclusion selon laquelle les cardinaux mesurables doivent être monstrueusement grands est maintenant normalement prouvée sans faire le détour par une faible compacité et des langages infinitaires, il n'en reste pas moins que ces idées ont été utilisées pour établir le résultat en premier lieu.

4. Incomplétude des langages quantificateurs infinis

Le résultat le plus important concernant les langages du premier ordre est probablement le théorème de complétude de Gödel qui dit bien sûr que l'ensemble de toutes les formules valides de tout langage L du premier ordre peut être généré à partir d'un simple ensemble d'axiomes au moyen de quelques règles simples de inférence. Une conséquence majeure de ce théorème est que, si les formules de L sont codées comme des nombres naturels d'une manière constructive, alors l'ensemble des (codes de) phrases valides est récursivement énumérable. Ainsi, l'exhaustivité d'un langage de premier ordre implique que l'ensemble de ses phrases valides est définissable d'une manière particulièrement simple. Il semblerait donc raisonnable, étant donné un langage arbitraire L, de renverser cette implication et de suggérer que, si l'ensemble des L valides-sentences n'est pas définissable d'une manière simple, alors aucun résultat d'exhaustivité significatif ne peut être établi pour L, ou, comme nous le dirons, que L est incomplet. Dans cette section, nous allons utiliser cette suggestion pour esquisser une preuve que «la plupart» des langages quantificateurs infinis sont incomplets en ce sens.

Introduisons d'abord la notion formelle de définissabilité comme suit. Si L est un langage, A une L -structure, et X un sous-ensemble du domaine A de A, on dit que X est définissable dans A par une formule φ (x, y 1,…, y n) de L s'il y a est une séquence de 1, …, a n d'éléments de a telle que X est le sous - ensemble de tous les éléments x ∈ a pour lequel φ (x, a 1, …, a n) tient dans a.

Maintenant, écrivez Val (L) pour l'ensemble de toutes les L -sentences valides, c'est-à-dire celles qui sont valables dans chaque L -structure. Afin d'attribuer une signification à l'énoncé «Val (L) est définissable», nous devons spécifier

  1. une structure C (L) - la structure de codage pour L;
  2. une carte un-un particulière - la carte de codage - de l'ensemble des formules de L dans le domaine de C (L).

Ensuite, si nous identifions Val (L) avec son image en C (L) sous la carte de codage, nous interpréterons l'énoncé «Val (L) est définissable» comme l'énoncé «Val (L), considéré comme un sous-ensemble du domaine de C (L), est définissable dans C (L) par une formule de L. »

Par exemple, lorsque L est le langage L du premier ordre de l'arithmétique, Gödel utilisait à l'origine comme structure de codage le modèle standard de l'arithmétique ℕ et comme carte de codage la fonction bien connue obtenue à partir du théorème de factorisation premier pour les nombres naturels. L'énumérabilité récursive de Val (L) signifie alors simplement que l'ensemble des codes («nombres de Gödel») des membres de Val (L) est définissable dans ℕ par une L-formule de la forme ∃ y φ (x, y), où φ (x, y) est une formule récursive.

Une autre structure de codage équivalente pour le langage du premier ordre de l'arithmétique est la structure [5] ⟨H (ω), ∈ ⨡ H (ω)⟩ des ensembles héréditairement finis, où un ensemble x est héréditaire si x, ses membres, ses membres de membres, etc., sont tous finis. Cette structure de codage tient compte du fait que les formules du premier ordre sont naturellement considérées comme des ensembles finis.

Passant maintenant au cas dans lequel L est un langage infinitaire L (κ, λ), quelle serait une structure de codage appropriée dans ce cas? Nous avons remarqué au début que les langages infinitaires étaient suggérés par la possibilité de penser les formules comme des objets théoriques des ensembles, alors essayons d'obtenir notre structure de codage en pensant à quel genre d'objets théoriques des ensembles nous devrions prendre des formules infinitaires. Étant donné que, pour chaque forme φ∈ (κ, λ), φ et ses sous-formules, sous-sous-formules, etc., sont toutes de longueur <κ, [6]la réflexion d'un moment révèle que les formules de L (κ, λ) «correspondent» à des ensembles x héréditairement de cardinalité <κ au sens où x, ses membres, ses membres de membres, etc., sont tous de cardinalité <κ. L'ensemble de tous ces ensembles s'écrit H (κ). H (ω) est la collection d'ensembles héréditairement finis introduite ci-dessus, et H (ω 1) celle de tous les ensembles héréditairement dénombrables.

Pour simplifier, supposons que le seul symbole extralogique du langage de base L soit le symbole de prédicat binaire ∈ (la discussion est facilement étendue au cas où L contient des symboles extralogiques supplémentaires). Guidé par les remarques ci-dessus, comme structure de codage pour L (κ, λ) nous prenons la structure,

H (κ) = df ⟨H (κ), ∈ ⨡ H (κ)⟩.

Nous pouvons maintenant définir la carte de codage de la forme (κ, λ) en H (κ). Tout d'abord, à chaque symbole de base s de L (κ, λ), nous affectons un objet code s ∈ H (κ) comme suit. Soit {v ξ: ξ <κ} une énumération des variables individuelles de L (κ, λ).

symbole Objet de code Notation
¬ 1 ¬
2
3
4
5
= 6 =
v ξ ⟨0, ξ⟩ v ξ

Ensuite, pour chaque φ ∈ forme (κ, λ) nous assignons l'objet de code & phiv suit récursive comme:

v ξ = v r | = df v ξ , = , v r | ⟩, v Ç ∈ v r | = df v Ç , , v r | ⟩;

pour φ, ψ ∈ Forme (κ, λ),

& phiv ∧ ψ = df & phiv , , ψ

¬φ = df ¬ , & phiv

∃ X & phiv = df, { x : x ∈ X}, & phiv ⟩;

et enfin si Φ ⊆ Forme (κ, λ) avec | Φ | <κ,

∧Φ = df, { & phiv : φ ∈ Φ}⟩.

La carte φ ↦ φ de la forme (κ, λ) dans H (κ) est facilement considérée comme un-un et est la carte de codage requise. En conséquence, nous convenons d'identifier Val (L (κ, λ)) avec son image en H (κ) sous cette carte de codage.

Quand Val (L (κ, λ)) est-il un sous-ensemble définissable de H (κ)? Afin de répondre à cette question, nous avons besoin des définitions suivantes.

Une L-formule est appelée formule Δ 0 - si elle équivaut à une formule dans laquelle tous les quantificateurs sont de la forme ∀ x ∈ y ou ∃ x ∈ y (c'est-à-dire ∀ x (x ∈ y →…) ou ∃ x (x ∈ y ∧…)). Une L-formule est une formule Σ 1 - si elle équivaut à une formule qui peut être construite à partir de formules atomiques et de leurs négations en utilisant uniquement les opérateurs logiques ∧, ∨, ∀ x ∈ y, ∃ x. Un sous-ensemble X d'un ensemble A est dit Δ 0 (resp. Σ 1) sur A s'il est définissable dans la structure ⟨A, ∈ ⨡ A⟩ par une formule Δ 0 - (resp. Σ 1 -) de L.

Par exemple, si nous identifions l'ensemble des nombres naturels avec l'ensemble H (ω) des ensembles héréditairement finis de la manière habituelle, alors pour chaque X ⊆ H (ω) nous avons:

X est Δ 0 sur H (ω) ⇔ X est récursif

X est Σ 1 sur H (ω) ⇔ X est récursivement énumérable.

Ainsi les notions d'ensemble Δ 0 et Σ 1 peuvent être considérées comme des généralisations des notions d'ensemble récursif et récursivement énumérable, respectivement.

Le théorème de complétude pour L implique que Val (L) - considéré comme un sous-ensemble de H (ω) - est récursivement énumérable, et donc Σ 1 sur H (ω). De même, le théorème de complétude pour L (ω 1, ω) (voir §2) implique que Val (L (ω 1, ω)) - considéré comme un sous-ensemble de H (ω 1) - est Σ 1 sur H (ω 1). Cependant, cet état de fait agréable s'effondre complètement dès que L (ω 1, ω 1) est atteint. Car on peut prouver

Théorème d'indéfinissabilité de Scott pour L (ω 1, ω 1). Val (L (ω 1, ω 1)) n'est pas définissable dans H (ω 1) même par une formule L (ω 1, ω 1) -; donc a fortiori Val (L (ω 1, ω 1)) n'est pas Σ 1 sur H (ω 1).

Ce théorème est prouvé à peu près de la même manière que le résultat bien connu que l'ensemble des (codes de) phrases valides du langage du second ordre de l'arithémétique L 2 n'est pas définissable du second ordre dans sa structure de codage ℕ. Pour obtenir ce dernier résultat, on observe d'abord que ℕ est caractérisé par une seule phrase L 2, puis on montre que, si le résultat était faux, alors «vérité en ℕ» pour les phrases L 2 serait définissable par un L 2 -formule, violant ainsi le théorème de Tarski sur l'indéfinissabilité de la vérité.

En conséquence, pour prouver le théorème d'indéfinissabilité de Scott dans le sens ci-dessus, il faut établir:

(4.1) Caractérisabilité de la structure codante H (ω 1) dans L (ω 1, ω 1): il existe une L (ω 1, ω 1) -sentence τ 0 telle que, pour toutes les L-structures A, A ⊨ τ 0A ≅ H (ω 1).

(4.2) Indéfinissabilité de la vérité pour L (ω 1, ω 1) - phrases dans la structure codante: il n'y a pas de L (ω 1, ω 1) -formule φ (v 0) telle que, pour tout L (ω 1, ω 1) -sentences σ, H (ω 1) ⊨ σ↔φ ( σ ).

(4.3) Il existe un terme t (v 0, v 1) de L (ω 1, ω 1) tel que, pour chaque couple de phrases σ, τ de L (ω 1, ω 1), H (ω 1) ⊨ [t ( σ , τ ) = σ → τ ].

(4.1) est prouvé en analysant la définition théorique des ensembles de H (ω 1) et en montrant qu'elle peut être formulée «en interne» dans L (ω 1, ω 1). (4.2) est établi à peu près de la même manière que le théorème de Tarski sur l'indéfinissabilité de la vérité pour les langages du premier ou du second ordre. (4.3) est obtenue en formalisant la définition de la carte de codage σ ↦ σ dans L (ω 1, ω 1).

Forts de ces faits, nous pouvons obtenir le théorème d'indéfinissabilité de Scott de la manière suivante. Supposons que ce soit faux; alors il y aurait une L (ω 1, ω 1) -formule θ (v 0) telle que, pour toutes les L (ω 1, ω 1) -sentences σ,

(4.4) H (ω 1) ⊨ θ ( σ ) ssi σ ∈ Val (L (ω 1, ω 1)).

Soit τ 0 la phrase donnée en (4.1). Alors on a, pour toutes les L (ω 1, ω 1) -sentences σ,

H (ω 1) ⊨ σ ssi (τ 0 → σ) ∈ Val (L (ω 1, ω 1)),

de sorte que, par (4.4),

H (ω 1) ⊨ σ ssi H (ω 1) ⊨ θ ( τ 0 → σ ).

Si t est le terme donné en (4.3), il s'ensuivrait que

H (ω 1) ⊨ σ↔θ (t ( τ 0 , σ )).

Maintenant, écrivez φ (v 0) pour la L (ω 1, ω 1) -formule θ (t ( τ 0 , σ )). ensuite

H (ω 1) ⊨ σ↔φ ( σ ),

contredisant (4.2), et complétant la preuve.

Ainsi Val (L (ω 1, ω 1)) n'est pas définissable même par une formule L (ω 1, ω 1) -, donc a fortiori L (ω 1, ω 1) est incomplète. Des arguments similaires montrent que le théorème d'indéfinissabilité de Scott continue de tenir lorsque ω 1 est remplacé par tout cardinal successeur κ +; en conséquence les langages L (κ +, κ +) sont tous incomplets. [7]

5. Sous-langages de L (ω 1, ω) et du théorème de la compacité à barres

Compte tenu de ce que nous savons maintenant sur les langages infinitaires, il semblerait que L (ω 1, ω) soit le seul à se comporter raisonnablement bien. D'autre part, l'échec du théorème de compacité à se généraliser à L (ω 1, ω) de manière utile est un inconvénient majeur en ce qui concerne les applications. Essayons d'analyser cet échec plus en détail.

Rappelons du §4 que nous pouvons coder les formules d'un langage L du premier ordre comme des ensembles héréditairement finis, c'est-à-dire comme membres de H (ω). Dans ce cas, chaque ensemble fini de (codes de) phrases L est également un membre de H (ω), et il s'ensuit que le théorème de compacité pour L peut être énoncé sous la forme:

(5.1) Si Δ ⊆ Sent (L) est tel que chaque sous-ensemble Δ 0 ⊆ Δ, Δ 0 ∈ H (ω) a un modèle, il en va de même pour Δ.

Or, il est bien connu que (5.1) est une conséquence immédiate du théorème de complétude généralisé pour L, qui, énoncé sous une forme similaire à celle de (5.1), devient l'assertion:

(5.2) Si Δ ⊆ Sent (L) et σ ∈ Sent (L) satisfont Δ ⊨ σ, alors il y a une déduction D de σ de Δ telle que D ∈ H (ω). [8]

Au §2 nous avons remarqué que le théorème de compacité pour L (ω 1, ω) échoue très fortement; en fait, nous avons construit un ensemble Γ ⊆ Sent1, ω) tel que

(5.3) Chaque sous-ensemble dénombrable de Γ a un modèle mais pas Γ.

Rappelons aussi que nous avons introduit la notion de déduction dans L (ω 1, ω); comme ces déductions sont de longueur dénombrable, il résulte rapidement de (5.3) que

(5.4) Il existe une phrase [9] σ ∈ Envoyée1, ω) telle que Γ ⊨ σ, mais il n'y a pas de déduction de σ dans L (ω 1, from) de.

Maintenant, les formules de L (ω 1, can) peuvent être codées comme membres de H (ω 1), et il est clair que H (ω 1) est fermé sous la formation de sous-ensembles et de séquences dénombrables. En conséquence (5.3) et (5.4) peuvent s'écrire:

(5.3 bis) Chaque Γ 0 ⊆ Γ tel que Γ 0 ∈ H (ω 1) a un modèle, mais pas not;

(5.4 bis) Il existe une phrase σ ∈ Sent1, ω) telle que Γ ⊨ σ, mais il n'y a pas de déduction D ∈ H (ω 1) de σ à partir de Γ.

Il s'ensuit que (5.1) et (5.2) échouent lorsque «L» est remplacé par «L (ω 1, ω)» et «H (ω)» par «H (ω 1)». De plus, on peut montrer que l'ensemble Γ ⊆ Envoyé1, in) dans (5.3 bis) et (5.4 bis) peut être pris égal à Σ 1 sur H (ω 1). Ainsi, les théorèmes de compacité et de complétude généralisée échouent même pour les Σ 1- ensembles de L (ω 1, ω) -sentences.

On voit d'après (5.4 bis) que la raison pour laquelle le théorème de complétude généralisé échoue pour Σ 1- ensembles dans L (ω 1, ω) est que, grosso modo, H (ω 1) n'est pas «fermé» sous la formation des déductions à partir de Σ 1- ensembles de phrases dans H (ω 1). Donc, pour y remédier, il semblerait naturel de remplacer H (ω 1) par des ensembles A qui sont, en un certain sens, fermés sous la formation de telles déductions, puis de ne considérer que les formules dont les codes sont dans A.

Nous donnons maintenant un aperçu de la façon dont cela peut être fait.

Tout d'abord, nous identifions les symboles et formules de L (ω 1, ω) avec leurs codes dans H (ω 1), comme au §4. Pour chaque ensemble transitif dénombrable [10] A, soit

L A = Forme (L (ω 1, ω)) ∩ A.

On dit que L A est un sous-langage de L (ω 1, ω) si les conditions suivantes sont remplies:

  1. L ⊆ L A
  2. si φ, ψ ∈ L A, alors φ ∧ ψ ∈ L A et ¬φ ∈ L A
  3. si φ ∈ L A et x ∈ A, alors ∃ x φ ∈ L A
  4. si φ (x) ∈ L A et y ∈ A, alors φ (y) ∈ L A
  5. si φ ∈ L A, toute sous-formule de φ est dans L A
  6. si Φ ⊆ L A et Φ ∈ A, ∧Φ ∈ L A.

La notion de déduction dans L A est définie de manière usuelle; si Δ est un ensemble de phrases de L A et ɸ ∈ L A, puis la déduction de φ à partir de Δ en L A est une déduction de φ à partir de Δ en L (ω 1, ω) chaque formule est dans L A. On dit que φ est déductible de Δ dans L A s'il y a une déduction D de φ de Δ dans L A; dans ces conditions on écrit Δ ⊢ A φ. En général, D ne sera pas membre de A; afin de garantir qu'une telle déduction puisse être trouvée en A, il sera nécessaire d'imposer des conditions supplémentaires à A.

Soit A un ensemble transitif dénombrable tel que L A est un sous - langage de L (ω 1, ω) et soit Δ un ensemble de phrases de L A. On dit que A (ou, par abus de terminologie, L A) est Δ- fermé si, pour toute formule φ de L A telle que Δ ⊢ A φ, on déduit D de φ de Δ telle que D ∈ A. On peut montrer que le seul langage dénombrable qui est Δ-fermé pour Δ arbitraire est le langage du premier ordre L, c'est-à-dire lorsque A = H (ω). Cependant J. Barwise a découvert qu'il existe des ensembles dénombrables A ⊆ H (ω 1) dont les langages correspondants L A diffèrent de L et sont pourtant Δ-fermés pour tout Σ 1- ensembles de phrases Δ. De tels ensembles A sont appelés ensembles admissibles; en gros, ce sont des extensions des ensembles héréditairement finis dans lesquels la théorie de la récursivité - et donc la théorie de la preuve - sont encore possibles (pour la définition complète, voir la section 5.1 ci-dessous).

Du résultat de Barwise, on obtient immédiatement le

Théorème de la compacité à barres. Soit A un ensemble admissible dénombrable et soit Δ un ensemble de phrases de L A qui est Σ 1 sur A. Si chaque Δ '⊆ Δ tel que Δ' ∈ A a un modèle, alors Δ en a un.

La présence de «Σ 1 » indique ici que ce théorème est une généralisation du théorème de compacité pour des ensembles de phrases récursivement énumérables.

Une autre version du théorème de compacité de Barwise, utile pour construire des modèles de théorie des ensembles, est la suivante. Soit ZFC l'ensemble habituel d'axiomes pour la théorie des ensembles de Zermelo-Fraenkel, y compris l'axiome de choix. Ensuite nous avons:

5.5 Théorème. Soit A un ensemble transitif dénombrable tel que A = ⟨A, ∈ ⨡ A⟩ est un modèle de ZFC. Si Δ est un ensemble de phrases de L A définissable dans A par une formule du langage de la théorie des ensembles et si chaque Δ '⊆ Δ tel que Δ' ∈ A a un modèle, il en va de même pour Δ.

Pour conclure, nous donnons une application simple de ce théorème. Soit A = ⟨A, ∈ ⨡ A⟩ un modèle de ZFC. Un modèle B = ⟨B, E⟩ de ZFC est dit une extension d'extrémité propre de A si (i) AB, (ii) AB, (iii) a ∈ A, b ∈ B, bEa ⇒ b ∈ A. Ainsi, une extension de fin propre d'un modèle de ZFC est une extension propre dans laquelle aucun élément «nouveau» ne vient «avant» un élément «ancien». Comme notre application de 5.5, nous prouvons

5.6 Théorème. Chaque modèle transitif dénombrable de ZFC a une extension d'extrémité appropriée.

Preuve. Soit A = ⟨A, ∈ ⨡ A⟩ un modèle transitif de ZFC et soit L le langage du premier ordre de la théorie des ensembles augmenté d'un nom a pour chaque a ∈ A, et d'une constante supplémentaire c. Soit Δ l'ensemble des L A -sences comprenant:

  • tous les axiomes de ZFC;
  • ca, pour chaque a ∈ A;
  • ∀ x (x ∈ a → ∨ b ∈ a x = b), pour chaque a ∈ A;
  • ab, pour chaque a ∈ b ∈ A.

On montre facilement que Δ est un sous-ensemble de A qui est définissable dans A par une formule du langage de la théorie des ensembles. Aussi, chaque sous-ensemble Δ '⊆ Δ tel que Δ' ∈ A a un modèle. Pour l'ensemble C de tout a ∈ A pour lequel a apparaît dans Δ 'appartient à A - puisque Δ' le fait - et donc, si nous interprétons c comme n'importe quel membre de l'ensemble (nécessairement non vide) A - C, alors A est un modèle de Δ '. En conséquence, (5.5) implique que Δ a un modèle ⟨B, E⟩. Si nous interprétons chaque constante un comme l'élément a ∈ A, ⟨B, E⟩ est une bonne fin de l' extension A. La preuve est complète.

Le lecteur verra rapidement que le théorème de compacité du premier ordre ne donnera pas ce résultat.

5.1 Définition du concept d'ensemble admissible

Un ensemble transitif non vide A est dit admissible lorsque les conditions suivantes sont satisfaites:

  1. si a, b ∈ A, alors {a, b} ∈ A et ∪ A ∈ A;
  2. si a ∈ A et X ⊆ A est Δ 0 sur A, alors X ∩ a ∈ A;
  3. si a ∈ A, X ⊆ A est Δ 0 sur A, et ∀ x ∈ a ∃ y (<x, y> ∈ X), alors, pour certains b ∈ A, ∀ x ∈ a ∃ y ∈ b (<x, y> ∈ X).

La condition (ii) - le Δ 0 - schéma de séparation - est une version restreinte de l'axiome de séparation de Zermelo. La condition (iii) - une version également affaiblie de l'axiome de remplacement - peut être appelée le schéma de remplacement Δ 0.

Il est assez facile de voir que si A est un ensemble transitif tel que <A, ∈ | A> est un modèle de ZFC, alors A est admissible. Plus généralement, le résultat continue de tenir lorsque l'axiome de l'ensemble de puissance est omis de ZFC, de sorte que H (ω) et H (ω 1) sont tous deux admissibles. Cependant, puisque ce dernier est indénombrable, le théorème de compacité de Barwise ne s'applique pas à lui.

6. Remarques historiques et bibliographiques

§§ 1 et 2. Les langages propositionnels et prédicats infinitaires semblent avoir fait leur première apparition explicite dans la presse écrite avec les articles de Scott et Tarski [1958] et Tarski [1958]. Le théorème de complétude pour L (ω 1, ω), ainsi que pour d'autres langages infinitaires, a été prouvé par Karp [1964]. Les calculs des nombres de Hanf pour L (ω 1, ω) ont d'abord été effectués par Morley [1965]. Le caractère indéfinissable des ordres de puits dans les langages quantificateurs finis a été prouvé par Karp [1965] et Lopez-Escobar [1966]. Le théorème d'interpolation pour L (ω 1, ω) a été prouvé par Lopez-Escobar [1965] et le théorème d'isomorphisme de Scott pour L (ω 1, ω) par Scott [1965].

Le théorème d'isomorphisme partiel de Karp a été prouvé pour la première fois dans Karp [1965]; voir également Barwise [1973]. Le résultat (2.2) apparaît dans Chang [1968], le résultat (2.3) dans Ellentuck [1976] et le résultat (2.4) dans Bell [1981].

§ 3. Les résultats (3.2) et (3.3) sont dus à Hanf [1964], avec quelques raffinements par Lopez-Escobar [1966] et Dickmann [1975], tandis que (3.4) a été prouvé par Tarski. Le résultat (3.5) est dû à Scott [1961], (3.6) à Bell [1970] et [1972]; et (3.7) à Bell [1974]. Les cardinaux mesurables ont d'abord été considérés par Ulam [1930] et Tarski [1939]. Le fait que les cardinaux mesurables soient faiblement compacts a été noté dans Tarski [1962].

§ 4. Concernant le théorème d'indéfinissabilité pour L (ω 1, ω 1). Carol Karp remarque (1964, 166), «Au Congrès international de logique, méthodologie et philosophie des sciences de l'Université de Stanford en 1960, Dana Scott a fait circuler un aperçu d'une preuve de l'impossibilité d'un système formel définissable complet pour (γ +, γ +) avec un seul symbole de prédicat à deux places en plus du symbole d'égalité. » Scott n'a jamais publié son résultat et une preuve entièrement détaillée est apparue pour la première fois dans Karp [1964]. L'approche du théorème adoptée ici est basée sur le récit donné dans Dickmann [1975].

§ 5. La motivation initiale des résultats présentés dans cette section est venue de Kreisel; dans son [1965], il a souligné qu'il n'y avait aucune raison impérieuse de choisir des formules infinitaires uniquement sur la base de la «longueur», et a proposé à la place que des critères de définissabilité ou de «clôture» soient employés. La suggestion de Kreisel a été reprise avec grand succès par Barwise [1967], où son théorème de compacité a été prouvé. La notion d'ensemble admissible est due à Platek [1966]. Le théorème (5.6) est tiré de Keisler [1974].

Pour plus de détails sur le sujet des langues infinitaires, voir Aczel [1973], Dickmann [1975], Karp [1964], Keisler [1974] et Makkai [1977]. Un compte rendu utile du lien entre les langages infinitaires et les grands cardinaux peut être trouvé dans le chapitre 10 de Drake [1974].

Bibliographie

  • Aczel, P., 1973, «Infinitary Logic and the Barwise Compactness Theorem», Actes de la Bertrand Russell Memorial Logic Conference de 1971 (Uldum, Danemark), J. Bell, J. Cole, G. Priest et A. Slomson (éd..), Leeds: Bertrand Russell Memorial Logic Conference, 234-277.
  • Barwise, J., 1967, Infinitary Logic and Admissible Sets. doctorat Thèse, Université de Stanford.
  • –––, 1973, «En arrière et en avant à travers la logique infinitaire. Studies in Model Theory », dans Studies in Mathematics (Volume 8), Buffalo: Mathematical Association of American, pp. 5–34.
  • –––, 1975, Ensembles et structures admissibles, Berlin: Springer-Verlag.
  • Barwise, J. et S. Feferman (éds.), 1985, Handbook of Model-Theoretic Logics, New York: Springer-Verlag.
  • Baumgartner, J., 1974, «Le nombre de Hanf pour des phrases L ω 1, ω complètes (sans GCH)», Journal of Symbolic Logic, 39: 575–578.
  • Bell, JL, 1970, «Faible compacité dans les langues restreintes du second ordre», Bulletin de l'Académie polonaise des sciences, 18: 111–114.
  • –––, 1972, «Sur la relation entre la faible compacité en L ω 1, ω, L ω 1, ω 1, et les langues restreintes du second ordre», Archive for Mathematical Logic, 15: 74–78.
  • –––, 1974, «On Compact Cardinals», Zeitschrift für Mathematical Logik und Grundlagen der Mathematik, 20: 389–393.
  • –––, 1981, «Isomorphisme des structures en S-topos», Journal of Symbolic Logic, 43 (3): 449–459.
  • Chang, CC, 1968, «Quelques remarques sur la théorie des modèles des langages infinitaires». dans The Syntax and Semantics of Infinitary Languages (Lecture Notes in Mathematics: Volume 72), J. Barwise (ed.), Springer-Verlag, Berlin, 36-63.
  • Dickmann, MA, 1975, Large Infinitary Languages, Amsterdam: Hollande du Nord.
  • Drake, FR, 1974, Théorie des ensembles: une introduction aux grands cardinaux, Amsterdam: North-Holland Publishing Company.
  • Ellentuck, E., 1976, «Categoricity Regained», Journal of Symbolic Logic, 41 (3): 639–643.
  • Hanf, WP, 1964, Incompactness in Languages with Infinually Long Expressions, Amsterdam: Hollande du Nord.
  • Karp, C., 1964, Langues avec des expressions de longueur infinie, Amsterdam: Hollande du Nord.
  • –––, 1965, «Équivalence à quantificateur fini» dans la théorie des modèles, J. Addison, L. Henkin et A. Tarski (éd.), Amsterdam: North-Holland, 407–412.
  • Keisler, HJ, 1974, Model Theory for Infinitary Logic, Amsterdam: Hollande du Nord.
  • Keisler, HJ et Julia F. Knight, 2004, «Barwise: Infinitary Logic And Admissible Sets», Journal of Symbolic Logic, 10 (1): 4–36
  • Kolaitis, P. et M. Vardi, 1992, «Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory», Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS '92), IEEE, pp. 46-57; disponible en ligne, doi: 10.1109 / LICS.1992.185518
  • Kreisel, G., 1965, «Model-Theoretic Invariants, Applications to Recursive and Hyperarithmetic Operations», dans The Theory of Models, J. Addison, L. Henkin et A. Tarski (eds.), Amsterdam: North-Holland, 190-205.
  • Kueker, D., 1975, «Arguments de va-et-vient dans les langues infinitaires», in Infinitary Logic: In Memoriam Carol Karp (Notes de cours en mathématiques: volume 492), D. Kueker (éd.), Berlin: Springer-Verlag.
  • Lopez-Escobar, EGK, 1965, «Un théorème d'interpolation pour des phrases infiniment longues», Fundamenta Mathematicae, 57: 253-272.
  • –––, 1966, «On Defining Well-Orderings», Fundamenta Mathematicae, 59: 13–21.
  • Makkai, M., 1977, «Admissible Sets and Infinitary Logic», Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, 233-282.
  • Morley, M., 1965, «Omitting Classes of Elements», The Theory of Models, J. Addison, L. Henkin et A. Tarski (eds.), Amsterdam: North-Holland, 265-273.
  • Nadel, M. 1985, «L ω 1, ω and Admissible Fragments», dans J. Barwise et S. Feferman (eds.) 1985, 271-287.
  • Platek, R., 1966, Fondements de la théorie de la récursivité, Ph. D. Thèse, Université de Stanford.
  • Scott, D., 1961, «Cardinaux mesurables et ensembles constructibles», Bulletin de l'Académie des sciences polonaises, 9: 521-524.
  • –––, 1965, «Logic with Denumerably Long Formulas and Finite Strings of Quantifiers», The Theory of Models, J. Addison, L. Henkin et A. Tarski (eds.), Amsterdam: North-Holland, 329-341.
  • Scott, D. et A. Tarski, 1958, «Le calcul sententiel avec des expressions infiniment longues», Colloquium Mathematicum, 16: 166-170.
  • Shelah, Saharon, 2012, «Nice infinitary logics», Journal of the American Mathematical Society, 25: 395-427, disponible en ligne, doi: 10.1090 / S0894-0347-2011-00712-1
  • Tarski, A., 1939, «Ideale in völlständingen Mengenkörpern I», Fundamenta Mathematicae, 32: 140-150.
  • –––, 1958, «Remarques sur la logique des prédicats avec des expressions infiniment longues», Colloquium Mathematicum, 16: 171–176.
  • –––, 1962, «Quelques problèmes et résultats concernant les fondements de la théorie des ensembles», in E, Nagel, P. Suppes et A. Tarski (éd.), Logic, Methodology and Philosophy of Science, Stanford: Stanford University Press, 123-135.
  • Ulam, S., 1930, «Zur Masstheorie in der algemeinen Mengenlehre», Fundamenta Mathematicae, 16: 140-150.

Outils académiques

icône de l'homme Sep
icône de l'homme Sep
Comment citer cette entrée.
icône de l'homme Sep
icône de l'homme Sep
Prévisualisez la version PDF de cette entrée à la Friends of the SEP Society.
icône inpho
icône inpho
Recherchez cette rubrique d'entrée sur le projet d'ontologie de philosophie Internet (InPhO).
icône de papiers phil
icône de papiers phil
Bibliographie améliorée pour cette entrée chez PhilPapers, avec des liens vers sa base de données.

Autres ressources Internet

Recommandé: