Documentation

InfinitaryLogic.ModelTheory.HanfSpectrum.Countable

The countable-spectrum witness #

The first bounded-spectrum sentence of the sharpness chain: over constantsOn ℕ, the constants are pairwise distinct and every element is a constant. The spectrum is EXACTLY {ℵ₀} (mk_eq_aleph0_of_models_countableSpectrumSentence — the constant interpretation is a bijection ℕ ≃ M), so through the generic bounded-spectrum endpoint lt_Lomega1omegaHanfNumber_of_maximal_model:

Reference: Marker, Lectures on Infinitary Model Theory, Ch. 1. The powerset witness (ladder stage α = 0) and the Marker Exercise 5.3 ℶ_{α+1} ladder complete the chain in sibling files (endpoint: Lomega1omegaHanfNumber_eq_beth_omega1, HanfSpectrum/BethLadder.lean). Implementation helpers live in the CountableSpectrum namespace; only the sentence and the headline spectrum theorems are top-level.

source
def FirstOrder.Language.CountableSpectrum.const (n : ℕ) {α : Type} :
(constantsOn ℕ).Term α

The n-th constant of constantsOn ℕ, as a term over any variable type.

Equations
Instances For
    source
    theorem FirstOrder.Language.CountableSpectrum.const_realize {M : Type u_1} [(constantsOn ℕ).Structure M] {α : Type} (v : α → M) (n : ℕ) :
    Term.realize v (const n) = Structure.funMap (have this := n; this) Fin.elim0

    A constant realizes valuation-independently, to the interpretation of its symbol.

    source
    theorem FirstOrder.Language.CountableSpectrum.const_realize_structure {M : Type u_1} (σ : ℕ → M) {α : Type} (v : α → M) (n : ℕ) :
    Term.realize v (const n) = σ n

    Under a constantsOn.structure σ interpretation, a constant realizes to its σ-value.

    source
    noncomputable def FirstOrder.Language.CountableSpectrum.distinctAt (n : ℕ) :
    (constantsOn ℕ).Sentenceω

    The n-th distinctness conjunct: for n coding the pair (i, j) with i ≠ j, the disequality cᵢ ≠ cⱼ; a tautology on the diagonal.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def FirstOrder.Language.CountableSpectrum.surj :
      (constantsOn ℕ).Sentenceω

      Surjectivity onto the constants: every element equals some cₙ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def FirstOrder.Language.countableSpectrumSentence :
        (constantsOn ℕ).Sentenceω

        The countable-spectrum sentence: constants pairwise distinct, every element a constant. Its models are exactly the sets enumerated bijectively by ℕ — spectrum {ℵ₀}.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem FirstOrder.Language.CountableSpectrum.nat_models :
          countableSpectrumSentence.Realize ℕ

          ℕ itself (constants interpreted by id) models the countable-spectrum sentence.

          source
          theorem FirstOrder.Language.CountableSpectrum.constInterp_surjective {M : Type} [(constantsOn ℕ).Structure M] (hM : countableSpectrumSentence.Realize M) :
          Function.Surjective fun (n : ℕ) => Structure.funMap (have this := n; this) Fin.elim0

          The constant interpretation of a model is surjective (the surjectivity clause).

          source
          theorem FirstOrder.Language.CountableSpectrum.constInterp_injective {M : Type} [(constantsOn ℕ).Structure M] (hM : countableSpectrumSentence.Realize M) :
          Function.Injective fun (n : ℕ) => Structure.funMap (have this := n; this) Fin.elim0

          The constant interpretation of a model is injective (the distinctness clauses, keyed by Nat.pair).

          source
          theorem FirstOrder.Language.mk_eq_aleph0_of_models_countableSpectrumSentence {M : Type} [(constantsOn ℕ).Structure M] (hM : countableSpectrumSentence.Realize M) :
          Cardinal.mk M = Cardinal.aleph0

          The exact countable spectrum: every model of the countable-spectrum sentence has size exactly ℵ₀ — the constant interpretation is a bijection ℕ ≃ M.

          source
          theorem FirstOrder.Language.not_hasArbLargeModels_countableSpectrumSentence :
          ¬HasArbLargeModels countableSpectrumSentence

          The countable-spectrum sentence has no uncountable models — it does NOT have arbitrarily large models.

          source
          theorem FirstOrder.Language.aleph0_lt_Lomega1omegaHanfNumber :
          Cardinal.aleph0 < Lomega1omegaHanfNumber

          The first sharpness step: ℵ₀ < Lomega1omegaHanfNumber — the countable-spectrum sentence through the generic bounded-spectrum endpoint.

          source
          theorem FirstOrder.Language.not_isLomega1omegaHanfBound_of_le_aleph0 {κ : Cardinal.{0}} (hκ : κ ≤ Cardinal.aleph0) :
          ¬IsLomega1omegaHanfBound κ

          No κ ≤ ℵ₀ is a global L_{ω₁ω} Hanf bound.