Infinitary syntax, back-and-forth, and Scott analysis
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremScott's isomorphism theorem#
In a countable language, every countable structure M has
an Lω₁ω sentence that M satisfies and that holds in a countable structure, in any universe,
exactly when that structure is isomorphic to M.
Function symbols are allowed: the sentence is the back-translation of the Scott sentence of the
graph expansion of M.
TauCeti.scott_isomorphism.{u, v, w, w'} {L : FirstOrder.Language}
[Countable ((k : ℕ) × L.Functions k)] [Countable ((k : ℕ) × L.Relations k)] (M : Type w)
[L.Structure M] [Countable M] :
∃ σ,
FirstOrder.Language.SentenceInf.Realize σ M ∧
∀ (N : Type w') [inst : L.Structure N] [Countable N],
FirstOrder.Language.SentenceInf.Realize σ N ↔ Nonempty (L.Equiv M N)
Uses 5
TheoremTauCeti.realize_scottSentenceAt_iff#
At a countable internally stabilizing level, the Scott sentence of a countable structure M
holds in a countable structure exactly when that structure is isomorphic to M.
TauCeti.realize_scottSentenceAt_iff.{u, v, w, w', o} {L : FirstOrder.Language} [L.IsRelational]
[Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] {α : Ordinal.{o}}
(hα : α < Ordinal.omega 1) (hs : TauCeti.SelfStabilizesCompletely M α) (N : Type w')
[L.Structure N] [Countable N] :
FirstOrder.Language.SentenceInf.Realize (TauCeti.scottSentenceAt M α) N ↔ Nonempty (L.Equiv M N)
Uses 4
TheoremKarp's theorem at a common carrier#
Structures in a relational language that are both
coded into κ are potentially isomorphic exactly when they satisfy the same infinitary sentences
with carrier κ.
TauCeti.karp_theorem_at.{u, v, w, w', uκ} {L : FirstOrder.Language} {M : Type w} {N : Type w'}
[L.Structure M] [L.Structure N] [L.IsRelational] {κ : Type uκ} (cM : TauCeti.IndexCoding M κ)
(cN : TauCeti.IndexCoding N κ) : TauCeti.PotentialIso M N ↔ TauCeti.InfEquivAt κ M N
Uses 3 · Used by 1
TheoremKarp's theorem#
Structures in a relational language are potentially isomorphic exactly when
they satisfy the same infinitary sentences. The converse uses the carrier M ⊕ N.
TauCeti.karp_theorem.{u, v, w, w'} {L : FirstOrder.Language} {M : Type w} {N : Type w'}
[L.Structure M] [L.Structure N] [L.IsRelational] :
TauCeti.PotentialIso M N ↔ TauCeti.InfEquivW M N
Lean
Formalized in Tau Ceti as TauCeti.karp_theorem.
Other forms
Karp's theorem, converse direction. Formalized in Tau Ceti as TauCeti.InfEquivAt.potentialIso.
TauCeti.InfEquivAt.potentialIso.{u, v, w, w', uκ} {L : FirstOrder.Language} {M : Type w}
{N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {κ : Type uκ}
(cM : TauCeti.IndexCoding M κ) (cN : TauCeti.IndexCoding N κ) (h : TauCeti.InfEquivAt κ M N) :
TauCeti.PotentialIso M N
Karp's theorem, forward direction. Formalized in Tau Ceti as TauCeti.PotentialIso.infEquivAt.
TauCeti.PotentialIso.infEquivAt.{u, v, w, w', uκ} {L : FirstOrder.Language} {M : Type w}
{N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] (h : TauCeti.PotentialIso M N)
(κ : Type uκ) : TauCeti.InfEquivAt κ M N
Sources
Uses 4 · Used by 2
TheoremKarp's theorem for countable structures#
Countable structures in a relational language are
isomorphic exactly when they satisfy the same L_{ω₁ω} sentences, the infinitary sentences whose
conjunctions and disjunctions are indexed by ℕ.
TauCeti.countable_infEquivAt_nat_iff_iso.{u, v, w, w'} {L : FirstOrder.Language} {M : Type w}
{N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [Countable M] [Countable N] :
TauCeti.InfEquivAt ℕ M N ↔ Nonempty (L.Equiv M N)
Uses 3 · Used by 1
TheoremTauCeti.realize_scottFormula_iff_bfEquiv#
A tuple in any structure satisfies the canonical Scott formula exactly when it is back-and-forth equivalent to the original tuple at that countable ordinal.
TauCeti.realize_scottFormula_iff_bfEquiv.{u, v, w, w', o} {L : FirstOrder.Language}
[Countable ((k : ℕ) × L.Relations k)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ}
[L.IsRelational] {N : Type w'} [L.Structure N] (a : Fin n → M) (b : Fin n → N) {α : Ordinal.{o}}
(hα : α < Ordinal.omega 1) :
FirstOrder.Language.BoundedFormulaInf.Realize (TauCeti.scottFormula a α) Empty.elim b ↔
TauCeti.BFEquiv α n a b
Uses 2 · Used by 2
TheoremTauCeti.internalScottRank_lt_omega_one#
Every countable structure has internal Scott rank below the first uncountable ordinal. The relational language need not be countable.
TauCeti.internalScottRank_lt_omega_one.{u, v, w} {L : FirstOrder.Language} [L.IsRelational]
{M : Type w} [L.Structure M] [Countable M] : TauCeti.internalScottRank M < Ordinal.omega 1
Uses 2
TheoremTauCeti.selfStabilizationOrdinal_eq_iSup_orbitRank#
The least simultaneous stabilization level is the supremum of the orbit ranks of all finite tuples. This holds for arbitrary structures.
TauCeti.selfStabilizationOrdinal_eq_iSup_orbitRank.{u, v, w} {L : FirstOrder.Language}
[L.IsRelational] {M : Type w} [L.Structure M] :
TauCeti.selfStabilizationOrdinal M = ⨆ p, TauCeti.orbitRank p.snd
Lean
Formalized in Tau Ceti as TauCeti.selfStabilizationOrdinal_eq_iSup_orbitRank.
Sources
Uses 1
TheoremTauCeti.elementarilyEquivalent_int_sumLex_int#
ℤ and ℤ ⊕ₗ ℤ satisfy the same first-order sentences in the language of orders.
TauCeti.elementarilyEquivalent_int_sumLex_int :
FirstOrder.Language.order.ElementarilyEquivalent ℤ (ℤ ⊕ₗ ℤ)
TheoremElementary equivalence is strictly weaker than infinitary equivalence#
The countable
orders ℤ and ℤ ⊕ₗ ℤ are elementarily equivalent (elementarilyEquivalent_int_sumLex_int),
but some L_{ω₁ω} sentence distinguishes them. A fortiori they are not L_{∞ω}-equivalent, since
TauCeti.InfEquivW.infEquivAt turns L_{∞ω}-equivalence into agreement at ℕ.
TauCeti.not_infEquivAt_nat_int_sumLex_int : ¬TauCeti.InfEquivAt ℕ ℤ (ℤ ⊕ₗ ℤ)
Uses 2
TheoremTauCeti.exists_dlo_aleph_one_potentialIso_isEmpty_equiv#
Potential isomorphism, and hence L∞ω-equivalence, does not imply isomorphism for
uncountable structures of the same cardinality: in every universe there are two dense linear
orders without endpoints of cardinality ℵ₁ that are potentially isomorphic, and so
L∞ω-equivalent (TauCeti.InfEquivW), but not isomorphic. The witnesses are ω₁ ×ₗ ℚ and its
order dual.
TauCeti.exists_dlo_aleph_one_potentialIso_isEmpty_equiv.{w} :
∃ M N x x_1,
M ⊨ FirstOrder.Language.order.dlo ∧
N ⊨ FirstOrder.Language.order.dlo ∧
Cardinal.mk M = Cardinal.aleph 1 ∧
Cardinal.mk N = Cardinal.aleph 1 ∧
TauCeti.PotentialIso M N ∧
TauCeti.InfEquivW M N ∧ IsEmpty (FirstOrder.Language.order.Equiv M N)
Lean
Formalized in Tau Ceti as TauCeti.exists_dlo_aleph_one_potentialIso_isEmpty_equiv.
Sources
Uses 3
InductiveFirstOrder.Language.BoundedFormulaInf#
An infinitary bounded formula of L_{∞ω}, with infinitary conjunctions and disjunctions
branching over the fixed carrier ι, free variables indexed by α, and n additional bound
variables available.
FirstOrder.Language.BoundedFormulaInf.{u, v, u', uι} (L : FirstOrder.Language) (ι : Type uι)
(α : Type u') : ℕ → Type (max u v u' uι)
Used by 23
ℕ · Morley's dichotomy on the tier ℕ · Morley's theorem (cardinal form) · A countable theory is one sentence · FirstOrder.Language.StrongHomClass.theoryω_model_iff · FirstOrder.Language.Theoryω · FirstOrder.Language.Theoryω.conjunction · FirstOrder.Language.Theoryω.Model · Back-and-forth equivalence at level α gives agreement up to quantifier rank α · Elementary equivalence is strictly weaker than infinitary equivalence · FirstOrder.Language.BoundedFormulaInf.freeVarSupport · Karp's theorem · Karp's theorem at a common carrier · Karp's theorem for countable structures · Scott's isomorphism theorem · TauCeti.elementarilyEquivalent_int_sumLex_int · TauCeti.exists_dlo_aleph_one_potentialIso_isEmpty_equiv · TauCeti.realize_scottFormula_iff_bfEquiv · TauCeti.realize_scottSentenceAt_iff · Transport a formula along a coding of its carrier · The fragment Tarski–Vaught criterion · The model existence theorem with omitted types · The omitting types theorem for a countable formation-closed fragmentDefinitionTransport a formula along a coding of its carrier#
each ι-indexed conjunction or
disjunction becomes the corresponding coded connective at carrier κ.
FirstOrder.Language.BoundedFormulaInf.reindex.{u, v, u', uι, uκ} {L : FirstOrder.Language}
{ι : Type uι} {κ : Type uκ} {α : Type u'} (c : TauCeti.IndexCoding ι κ) {n : ℕ} :
L.BoundedFormulaInf ι α n → L.BoundedFormulaInf κ α n
Uses 1
DefinitionFirstOrder.Language.BoundedFormulaInf.freeVarSupport#
The free-variable support of an infinitary formula: the set of free variables that occur in one of its atoms. Infinitary connectives take the union over all their branches, so the support may be infinite.
FirstOrder.Language.BoundedFormulaInf.freeVarSupport.{u, v, u', uι} {L : FirstOrder.Language}
{α : Type u'} {ι : Type uι} {n : ℕ} : L.BoundedFormulaInf ι α n → Set α
Lean
Formalized in Tau Ceti as FirstOrder.Language.BoundedFormulaInf.freeVarSupport.
Sources
Uses 1
DefinitionTauCeti.BFEquiv#
Ordinal back-and-forth equivalence of tuples. At successors the previous level is retained, in addition to the forth and back requirements. The language is relational.
TauCeti.BFEquiv.{u, v, w, w', o} {L : FirstOrder.Language} [L.IsRelational] {M : Type w}
{N : Type w'} [L.Structure M] [L.Structure N] (α : Ordinal.{o}) (n : ℕ) (a : Fin n → M)
(b : Fin n → N) : Prop
Used by 10
ℕ · Back-and-forth equivalence at level α gives agreement up to quantifier rank α · Karp's theorem · Scott's isomorphism theorem · TauCeti.elementarilyEquivalent_int_sumLex_int · TauCeti.exists_complete_self_stabilization · TauCeti.internalScottRank_lt_omega_one · TauCeti.realize_scottFormula_iff_bfEquiv · TauCeti.realize_scottSentenceAt_iff · TauCeti.selfStabilizationOrdinal_eq_iSup_orbitRankDefinitionTauCeti.PotentialIso#
Two structures are potentially isomorphic if a nonempty set of finitely generated partial equivalences admits extensions containing every element on either side.
TauCeti.PotentialIso.{u, v, w, w'} {L : FirstOrder.Language} (M : Type w) (N : Type w')
[L.Structure M] [L.Structure N] : Prop
Used by 8
TheoremTauCeti.PotentialIso.trans#
Potential isomorphism is transitive.
TauCeti.PotentialIso.trans.{u, v, w, w', u_1} {L : FirstOrder.Language} {M : Type w} {N : Type w'}
[L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h₁ : TauCeti.PotentialIso M N)
(h₂ : TauCeti.PotentialIso N P) : TauCeti.PotentialIso M P
Uses 1
TheoremBack-and-forth equivalence at level α gives agreement up to quantifier rank α#
Tuples
that are back-and-forth equivalent at level α satisfy the same infinitary formulas of quantifier
rank at most α, at every carrier. The rank and the level are compared after lifting them to a
common universe.
TauCeti.BFEquiv.realize_iff_of_qrank_le.{u, v, w, w', o, uκ} {L : FirstOrder.Language} {M : Type w}
{N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {κ : Type uκ} {n : ℕ}
(φ : L.BoundedFormulaInf κ Empty n) {α : Ordinal.{o}} {a : Fin n → M} {b : Fin n → N} :
TauCeti.BFEquiv α n a b →
Ordinal.lift.{o, uκ} φ.qrank ≤ Ordinal.lift.{uκ, o} α →
∀ (v : Empty → M) (w : Empty → N), φ.Realize v a ↔ φ.Realize w b
Uses 2 · Used by 2
TheoremTauCeti.exists_complete_self_stabilization#
A countable structure stabilizes below ω₁. Only its tuples are counted; the language
may be uncountable.
TauCeti.exists_complete_self_stabilization.{u, v, w} {L : FirstOrder.Language} [L.IsRelational]
(M : Type w) [L.Structure M] [Countable M] :
∃ α < Ordinal.omega 1, TauCeti.SelfStabilizesCompletely M α
Uses 1 · Used by 3
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.