Nullary tags

Expanding a language by countably many nullary relation symbols P_n, interpreted by a set X ⊆ ℕ (P_n holds iff n ∈ X), the same way in every structure considered. The signature L.withTags is fixed independently of X; only the interpretation varies.

• tagLang: the language with nullary symbols indexed by ℕ and nothing else.
• L.withTags := L.sum tagLang.
• Tagged X M: the structure M expanded by the tags X (a type synonym carrying the expanded structure).

Semantic invariance, for expansions with matching tags:

• bfEquiv_tagged_iff: back-and-forth equivalence is preserved and reflected at every level.
• Equiv.toTagged, Equiv.ofTagged, taggedEquivEquiv: isomorphisms (hence automorphisms) are the same before and after tagging.
• orbitRank_tagged, internalScottRank_tagged: the orbit rank of every tuple and the internal Scott rank are unchanged. (Tagged X M carries M's own L-structure, so the right-hand sides are the untagged ranks; the type synonym keeps both sides syntactically well-typed at every transparency.)

With differing tags the expansions are already inequivalent at level 0 (not_bfEquiv_tagged_of_ne): a nullary atom distinguishes them, on any carrier, including the empty one.

Nothing here is effective: the diagram reductions D(M̂) ≡_T X and A ≅ M̂ → X ≤_T D(A) are downstream statements about presentations, not about these semantic invariances.

The tag language

def FirstOrder.Language.TagSym : ℕ → Type

Tag symbols: countably many at arity 0, none elsewhere.

Equations

• FirstOrder.Language.TagSym 0 = ℕ
• FirstOrder.Language.TagSym n.succ = Empty

def FirstOrder.Language.tagLang : Language

The language of nullary tags.

Equations

• FirstOrder.Language.tagLang = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.TagSym }

instance FirstOrder.Language.instIsRelationalTagLang : tagLang.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.withTags (L : Language) : Language

A language with nullary tags.

Equations

• L.withTags = L.sum FirstOrder.Language.tagLang

instance FirstOrder.Language.instIsRelationalWithTags (L : Language) [L.IsRelational] : L.withTags.IsRelational

Tagged structures

def FirstOrder.Language.Tagged (_X : Set ℕ) (M : Type w) : Type w

The structure M expanded by the tags X.

Equations

• FirstOrder.Language.Tagged _X M = M

@[instance_reducible]

instance FirstOrder.Language.instTaggedBase {L : Language} {M : Type w} [L.Structure M] (X : Set ℕ) : L.Structure (Tagged X M)

Equations

• FirstOrder.Language.instTaggedBase X = FirstOrder.Language.instTaggedBase._aux_1 X

@[instance_reducible]

instance FirstOrder.Language.instTaggedTags {M : Type w} (X : Set ℕ) : tagLang.Structure (Tagged X M)

The tags: P_n holds iff n ∈ X; the tuple is ignored.

Equations

• One or more equations did not get rendered due to their size.

Atoms

theorem FirstOrder.Language.sameAtomicType_tagged_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) {n : ℕ} (a : Fin n → Tagged X M) (b : Fin n → Tagged X N) : SameAtomicType a b ↔ SameAtomicType a b

Tagged atomic agreement is atomic agreement, for matching tags.

Back-and-forth equivalence

theorem FirstOrder.Language.bfEquiv_tagged_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) (α : Ordinal.{u_1}) {n : ℕ} (a : Fin n → Tagged X M) (b : Fin n → Tagged X N) : BFEquiv α n a b ↔ BFEquiv α n a b

Back-and-forth equivalence is preserved and reflected by tagging with matching tags, at every level.

theorem FirstOrder.Language.not_bfEquiv_tagged_of_ne {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {X Y : Set ℕ} {k : ℕ} (hk : (k ∈ X) ≠ (k ∈ Y)) {n : ℕ} (a : Fin n → Tagged X M) (b : Fin n → Tagged Y N) : ¬BFEquiv 0 n a b

With differing tags, the expansions are inequivalent already at level 0, on any carrier.

Isomorphisms

def FirstOrder.Language.Equiv.toTagged {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) (f : L.Equiv M N) : L.withTags.Equiv (Tagged X M) (Tagged X N)

An isomorphism is one of the tagged expansions with matching tags.

Equations

• FirstOrder.Language.Equiv.toTagged X f = { toEquiv := f.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

def FirstOrder.Language.Equiv.ofTagged {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) (g : L.withTags.Equiv (Tagged X M) (Tagged X N)) : L.Equiv M N

An isomorphism of tagged expansions is an isomorphism of the underlying structures.

Equations

• FirstOrder.Language.Equiv.ofTagged X g = { toEquiv := g.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

def FirstOrder.Language.taggedEquivEquiv {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) : L.withTags.Equiv (Tagged X M) (Tagged X N) ≃ L.Equiv M N

Isomorphisms are unchanged by tagging: the two notions correspond bijectively.

Equations

• FirstOrder.Language.taggedEquivEquiv X = { toFun := FirstOrder.Language.Equiv.ofTagged X, invFun := FirstOrder.Language.Equiv.toTagged X, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FirstOrder.Language.Equiv.toTagged_apply {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) (f : L.Equiv M N) (x : M) : (toTagged X f) x = f x

@[simp]

theorem FirstOrder.Language.Equiv.ofTagged_apply {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (X : Set ℕ) (g : L.withTags.Equiv (Tagged X M) (Tagged X N)) (x : M) : (ofTagged X g) x = g x

Ranks

theorem FirstOrder.Language.orbitRank_tagged {L : Language} {M : Type w} [L.Structure M] (X : Set ℕ) {n : ℕ} (a : Fin n → Tagged X M) : orbitRank a = orbitRank a

Orbit ranks are unchanged by tagging.

theorem FirstOrder.Language.internalScottRank_tagged {L : Language} {M : Type w} [L.Structure M] (X : Set ℕ) : internalScottRank (Tagged X M) = internalScottRank (Tagged X M)

Internal Scott ranks are unchanged by tagging.