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

• AtomicIdx: An index type for atomic formulas over a relational language.
• atomicFormula: Builds an atomic formula from an index.
• atomicDiagram: The conjunction of all true/false atomic facts about a tuple.
• SameAtomicType: Two tuples have the same atomic type iff they satisfy the same atomics.

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.

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.

• eq {L : Language} {n : ℕ} (i j : Fin n) : L.AtomicIdx n

  Equality between variable i and variable j.

• rel {L : Language} {n l : ℕ} (R : L.Relations l) (f : Fin l → Fin n) : L.AtomicIdx n

  Relation R applied to variables given by f.

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

Countable instance for AtomicIdx.

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

• (FirstOrder.Language.AtomicIdx.eq i j).holds a = (a i = a j)
• (FirstOrder.Language.AtomicIdx.rel R f).holds a = FirstOrder.Language.Structure.RelMap R (a ∘ f)

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

• FirstOrder.Language.atomicFormula (FirstOrder.Language.AtomicIdx.eq i j) = (FirstOrder.Language.var i).equal (FirstOrder.Language.var j)
• FirstOrder.Language.atomicFormula (FirstOrder.Language.AtomicIdx.rel R f) = R.formula fun (k : Fin l) => FirstOrder.Language.var (f k)

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

The atomic formula as an Lω₁ω formula.

Equations

• FirstOrder.Language.atomicFormulaω idx = (FirstOrder.Language.atomicFormula idx).toLω

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.

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

• FirstOrder.Language.SameAtomicType a b = ∀ (idx : L.AtomicIdx n), idx.holds a ↔ idx.holds b

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.

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.

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.

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.

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 ∘ σ).