Atomic diagrams of finite tuples

atomicDiagram a is the countable conjunction of the atomic tests true of a and the negations of the tests false of a. For a relational language, a tuple in any other structure realizes this formula exactly when it has the same atomic type. The tuple occupies bound-variable slots, with no free variables. Nullary relations are retained even when the tuple is empty.

This is the initial approximation in the construction of characteristic formulas for tuples. For a finite relation language, firstOrderAtomicDiagram a is the same conjunction as a first-order formula. The construction follows the atomic-diagram construction in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Scott/AtomicDiagram.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4; here tuples occupy bound positions rather than free variables. See also Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers (1965).

def TauCeti.AtomicIdx.toFormula {L : FirstOrder.Language} {n : ℕ} : AtomicIdx L n → L.BoundedFormula Empty n

The finitary atomic formula testing equality or a relation on bound-variable positions.

@[simp]

theorem TauCeti.AtomicIdx.toFormula_eq {L : FirstOrder.Language} {n : ℕ} (i j : Fin n) : (eq i j).toFormula = FirstOrder.Language.BoundedFormula.equal (FirstOrder.Language.var (Sum.inr i)) (FirstOrder.Language.var (Sum.inr j))

@[simp]

theorem TauCeti.AtomicIdx.toFormula_rel {L : FirstOrder.Language} {n k : ℕ} (r : L.Relations k) (f : Fin k → Fin n) : (rel r f).toFormula = FirstOrder.Language.BoundedFormula.rel r fun (i : Fin k) => FirstOrder.Language.var (Sum.inr (f i))

@[simp]

theorem TauCeti.AtomicIdx.realize_toFormula {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] (i : AtomicIdx L n) (a : Fin n → M) : i.toFormula.Realize Empty.elim a ↔ i.Holds a

The formula for an atomic test realizes precisely that test.

noncomputable def TauCeti.firstOrderAtomicDiagram {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] [Finite ((k : ℕ) × L.Relations k)] (a : Fin n → M) : L.BoundedFormula Empty n

For a finite relation language, the finite conjunction of the atomic tests true of a tuple and the negations of the tests false of it. Unlike atomicDiagram, this is a first-order formula.

theorem TauCeti.firstOrderAtomicDiagram_def {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] [Finite ((k : ℕ) × L.Relations k)] (a : Fin n → M) : firstOrderAtomicDiagram a = FirstOrder.Language.BoundedFormula.iInf fun (i : AtomicIdx L n) => if i.Holds a then i.toFormula else i.toFormula.not

The first-order atomic diagram is the finite conjunction of signed atomic formulas.

@[simp]

theorem TauCeti.realize_firstOrderAtomicDiagram_iff_sameAtomicType {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Finite ((k : ℕ) × L.Relations k)] [L.IsRelational] (a : Fin n → M) (v : Empty → N) (b : Fin n → N) : (firstOrderAtomicDiagram a).Realize v b ↔ SameAtomicType a b

Over a finite relational language, the first-order atomic diagram characterizes atomic-type agreement in every structure.

noncomputable def TauCeti.atomicDiagram {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] [Countable ((k : ℕ) × L.Relations k)] (a : Fin n → M) : L.BoundedFormulaω Empty n

The signed conjunction of all equality and relation tests on a tuple's positions. For a relational language this is its complete atomic diagram.

theorem TauCeti.atomicDiagram_def {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] [Countable ((k : ℕ) × L.Relations k)] (a : Fin n → M) : atomicDiagram a = FirstOrder.Language.BoundedFormulaInf.iInfAlong (IndexCoding.ofEncodableWith (Encodable.ofCountable (AtomicIdx L n))) fun (i : AtomicIdx L n) => if i.Holds a then i.toFormula.toOmega else FirstOrder.Language.BoundedFormulaInf.not i.toFormula.toOmega

The atomic diagram is a coded conjunction of signed atomic formulas.

@[simp]

theorem TauCeti.realize_atomicDiagram_iff_sameAtomicType {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable ((k : ℕ) × L.Relations k)] [L.IsRelational] (a : Fin n → M) (b : Fin n → N) : FirstOrder.Language.BoundedFormulaInf.Realize (atomicDiagram a) Empty.elim b ↔ SameAtomicType a b

Over a relational language, the atomic diagram characterizes atomic-type agreement in every structure, without a countability assumption on the realizing structure.