Atomic types of finite tuples

AtomicIdx L n indexes equalities of positions and relation symbols applied to positions in an n-tuple. Nullary relations are included, even for the empty tuple. SameAtomicType expresses agreement on these tests, the initial level of back-and-forth equivalence.

For a relational language these are all atomic formulas. SameAtomicType requires a relational language so that agreement on these tests is agreement on the full atomic type.

The construction follows the atomic tests in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Scott/BackAndForth.lean.

inductive TauCeti.AtomicIdx (L : FirstOrder.Language) (n : ℕ) : Type v

An equality of tuple positions or a relation symbol applied to tuple positions. The arity of a relation may be zero.

• eq {L : FirstOrder.Language} {n : ℕ} (i j : Fin n) : AtomicIdx L n
• rel {L : FirstOrder.Language} {n k : ℕ} (r : L.Relations k) (f : Fin k → Fin n) : AtomicIdx L n

instance TauCeti.instCountableAtomicIdxOfSigmaNatRelations {L : FirstOrder.Language} {n : ℕ} [Countable ((k : ℕ) × L.Relations k)] : Countable (AtomicIdx L n)

A countable relation language has countably many atomic tests on a finite tuple.

instance TauCeti.instFiniteAtomicIdxOfSigmaNatRelations {L : FirstOrder.Language} {n : ℕ} [Finite ((k : ℕ) × L.Relations k)] : Finite (AtomicIdx L n)

A finite relation language has finitely many atomic tests on a finite tuple.

def TauCeti.AtomicIdx.Holds {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] : AtomicIdx L n → (Fin n → M) → Prop

Evaluate an atomic test at a tuple.

@[simp]

theorem TauCeti.AtomicIdx.holds_eq {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] (i j : Fin n) (a : Fin n → M) : (eq i j).Holds a ↔ a i = a j

@[simp]

theorem TauCeti.AtomicIdx.holds_rel {L : FirstOrder.Language} {n : ℕ} {M : Type w} [L.Structure M] {k : ℕ} (r : L.Relations k) (f : Fin k → Fin n) (a : Fin n → M) : (rel r f).Holds a ↔ FirstOrder.Language.Structure.RelMap r (a ∘ f)

structure TauCeti.SameAtomicType {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] (a : Fin n → M) (b : Fin n → N) : Prop

Agreement on all atomic formulas of a relational language, including nullary relations.

• holds (i : AtomicIdx L n) : i.Holds a ↔ i.Holds b

  The tuples agree on each atomic test.

theorem TauCeti.sameAtomicType_def {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] (a : Fin n → M) (b : Fin n → N) : SameAtomicType a b ↔ ∀ (i : AtomicIdx L n), i.Holds a ↔ i.Holds b

Atomic-type agreement is pointwise agreement on the atomic tests.

theorem TauCeti.sameAtomicType_iff {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] (a : Fin n → M) (b : Fin n → N) : SameAtomicType a b ↔ (∀ (i j : Fin n), a i = a j ↔ b i = b j) ∧ ∀ {k : ℕ} (r : L.Relations k) (f : Fin k → Fin n), FirstOrder.Language.Structure.RelMap r (a ∘ f) ↔ FirstOrder.Language.Structure.RelMap r (b ∘ f)

Separate the equality and relation parts of atomic-type agreement.

theorem TauCeti.SameAtomicType.eq_iff {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (i j : Fin n) : a i = a j ↔ b i = b j

Tuples with the same atomic type have the same equality pattern.

theorem TauCeti.SameAtomicType.rel_iff {L : FirstOrder.Language} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) {k : ℕ} (r : L.Relations k) (f : Fin k → Fin n) : FirstOrder.Language.Structure.RelMap r (a ∘ f) ↔ FirstOrder.Language.Structure.RelMap r (b ∘ f)

Tuples with the same atomic type agree on every relation, including nullary ones.

@[simp]

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

Every tuple agrees with itself on all atomic tests.

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

Atomic-type agreement is symmetric.

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

Atomic-type agreement is transitive across three structures.

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

Atomic-type agreement is preserved by reindexing both tuples along the same map of positions, which may repeat or omit entries.

theorem TauCeti.sameAtomicType_elim0 {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [IsEmpty (L.Relations 0)] : SameAtomicType Fin.elim0 Fin.elim0

In a relational language without nullary relation symbols, the empty tuples of any two structures have the same atomic type.