Documentation

InfinitaryLogic.Scott.AtomicDiagram

Atomic Diagrams for Relational Languages #

This file defines atomic types and atomic diagrams for relational first-order languages. These are the building blocks for Scott formulas.

Main Definitions #

Implementation Notes #

We restrict to relational languages (L.IsRelational) so that the atomic diagram of a finite tuple is determined by equality and relation holding information.

source
inductive FirstOrder.Language.AtomicIdx (L : Language) (n : ℕ) :
Type (max u v)

Index type for atomic formulas in a relational language with n free variables. Either an equality between two variables, or a relation applied to variables.

Instances For
    source
    instance FirstOrder.Language.AtomicIdx.instCountableOfSigmaNatRelations {L : Language} {n : ℕ} [Countable ((l : ℕ) × L.Relations l)] :
    Countable (L.AtomicIdx n)

    Countable instance for AtomicIdx.

    source
    def FirstOrder.Language.AtomicIdx.holds {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (idx : L.AtomicIdx n) (a : Fin n → M) :
    Prop

    Evaluates whether an atomic formula indexed by idx holds for a tuple a.

    Equations
    Instances For
      source
      def FirstOrder.Language.AtomicIdx.pushforward {L : Language} {n m : ℕ} (idx : L.AtomicIdx m) (σ : Fin m → Fin n) :
      L.AtomicIdx n

      Pushforward an atomic index through a function σ : Fin m → Fin n. This transforms an atomic index over m variables to one over n variables by composing indices.

      Equations
      Instances For
        source
        theorem FirstOrder.Language.AtomicIdx.holds_comp_eq_holds_pushforward {L : Language} {M : Type w} [L.Structure M] {n m : ℕ} (idx : L.AtomicIdx m) (a : Fin n → M) (σ : Fin m → Fin n) :
        idx.holds (a ∘ σ) = (idx.pushforward σ).holds a

        The key lemma: holds on composed tuple equals holds of pushforward on original tuple.

        source
        def FirstOrder.Language.atomicFormula {L : Language} {n : ℕ} (idx : L.AtomicIdx n) :
        L.BoundedFormula (Fin n) 0

        Builds an atomic formula from an index. The formula uses free variables for the tuple.

        Equations
        Instances For
          source
          def FirstOrder.Language.atomicFormulaω {L : Language} {n : ℕ} (idx : L.AtomicIdx n) :
          L.BoundedFormulaω (Fin n) 0

          The atomic formula as an Lω₁ω formula.

          Equations
          Instances For
            source
            @[simp]
            theorem FirstOrder.Language.realize_atomicFormula {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (idx : L.AtomicIdx n) (a : Fin n → M) :
            (atomicFormula idx).Realize a Fin.elim0 ↔ idx.holds a
            source
            @[simp]
            theorem FirstOrder.Language.realize_atomicFormulaω {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (idx : L.AtomicIdx n) (a : Fin n → M) :
            (atomicFormulaω idx).Realize a Fin.elim0 ↔ idx.holds a
            source
            noncomputable def FirstOrder.Language.atomicDiagram {L : Language} {M : Type w} [L.Structure M] {n : ℕ} [Countable ((l : ℕ) × L.Relations l)] (a : Fin n → M) :
            L.Formulaω (Fin n)

            The atomic diagram of a tuple: the conjunction over all atomic indices of either the atomic formula or its negation, depending on whether it holds.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def FirstOrder.Language.SameAtomicType {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {N : Type w'} [L.Structure N] (a : Fin n → M) (b : Fin n → N) :
              Prop

              Two tuples have the same atomic type if they satisfy exactly the same atomic formulas.

              Note on IsRelational: While this definition is well-formed without [L.IsRelational], the notion of "same atomic type" only captures the full atomic equivalence for relational languages. With function symbols, AtomicIdx doesn't cover terms built from functions, so this would be a weaker notion than the standard "same atomic type" in model theory. For Scott analysis, we restrict to relational languages where this captures the full notion.

              Equations
              Instances For
                source
                theorem FirstOrder.Language.sameAtomicType_iff_realize_atomicDiagram {L : Language} {M : Type w} [L.Structure M] {n : ℕ} [Countable ((l : ℕ) × L.Relations l)] {N : Type w'} [L.Structure N] (a : Fin n → M) (b : Fin n → N) :
                SameAtomicType a b ↔ (atomicDiagram a).Realize b

                The correspondence between atomic diagrams and same atomic type.

                source
                theorem FirstOrder.Language.SameAtomicType.refl {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) :
                SameAtomicType a a

                Same atomic type is reflexive.

                source
                theorem FirstOrder.Language.SameAtomicType.symm {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {N : Type w'} [L.Structure N] {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) :
                SameAtomicType b a

                Same atomic type is symmetric.

                source
                theorem FirstOrder.Language.SameAtomicType.trans {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {N : Type u_1} {P : Type u_2} [L.Structure N] [L.Structure P] {a : Fin n → M} {b : Fin n → N} {c : Fin n → P} (hab : SameAtomicType a b) (hbc : SameAtomicType b c) :
                SameAtomicType a c

                Same atomic type is transitive.

                source
                theorem FirstOrder.Language.SameAtomicType.relabel {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n m : ℕ} {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (σ : Fin m → Fin n) :
                SameAtomicType (a ∘ σ) (b ∘ σ)

                Same atomic type is preserved under relabeling. If SameAtomicType a b and σ : Fin m → Fin n, then SameAtomicType (a ∘ σ) (b ∘ σ).