Finite extension and the block back-and-forth hierarchy

Two conventions for symmetric back-and-forth with full atomic agreement at level 0:

• BFEquiv (Scott/BackAndForth.lean): one element is added at each successor step.
• BlockBFEquiv (this module): for each β < α, a finite block of any length, zero included, is added at level β (Harrison-Trainor–Igusa–Knight, Some new computable structures of high rank, Definitions 1.1–1.2).

BFEquiv is unchanged. Contents, in dependency order:

1. Finite extension: forth or back by a k-tuple costs k levels (BFEquiv.forth_block, BFEquiv.back_block).
2. BlockBFEquiv, with its public equation blockBFEquiv_iff, monotonicity, and the two comparison bounds BlockBFEquiv.toBFEquiv (block level α gives single-element level α) and BFEquiv.toBlock (single-element level ω·α gives block level α).
3. Before any rank: equivalence at every level is the same in both conventions (bfEquiv_all_iff_blockBFEquiv_all), so block stabilization reuses the orbit-rank machinery.
4. Block orbit rank and block Scott rank with the inequalities r_B ≤ r ≤ ω·r_B and R_B ≤ R ≤ ω·R_B, which need no closure hypothesis, and the transfer of strict bounds below α. The closure hypothesis ∀ β < α, ω·β < α is required explicitly for the upward strict-bound transfer; it is not a standing assumption, and it is not implied by α being a countable limit.

The K₂ ⊔ K₃ regression in scripts/check_block_backandforth_regressions.lean shows the two hierarchies differ at the same level; it does not establish optimality of the ω factor.

Convention note: in the usual nonempty relational setting BFEquiv coincides with the Scott-rank survey's symmetric hierarchy (arXiv:2011.03923, Definition 2.5). On an empty carrier with differing nullary facts they differ: BFEquiv retains the atomic condition explicitly at every level, while the survey's positive clause consists solely of single-element moves. The survey's asymmetric Definition 2.1 tests only finitely many quantifier-free formulas at level 0; that finite-tested condition does not imply full atomic agreement (the other implication holds), and no comparison with it is made here.

Finite extension

theorem FirstOrder.Language.BFEquiv.forth_block {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{u_1}} {n : ℕ} (k : ℕ) {a : Fin n → M} {b : Fin n → N} : BFEquiv (α + ↑k) n a b → ∀ (c : Fin k → M), ∃ (d : Fin k → N), BFEquiv α (n + k) (Fin.append a c) (Fin.append b d)

Forth by a block: a k-tuple can be matched at the cost of k levels.

theorem FirstOrder.Language.BFEquiv.back_block {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{u_1}} {n : ℕ} (k : ℕ) {a : Fin n → M} {b : Fin n → N} (h : BFEquiv (α + ↑k) n a b) (d : Fin k → N) : ∃ (c : Fin k → M), BFEquiv α (n + k) (Fin.append a c) (Fin.append b d)

Back by a block: symmetric to forth_block.

The block hierarchy

noncomputable def FirstOrder.Language.BlockBFEquiv {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] : Ordinal.{u_1} → (n : ℕ) → (Fin n → M) → (Fin n → N) → Prop

The block back-and-forth relation (Harrison-Trainor–Igusa–Knight Definition 1.2): atomic agreement, and for each β < α a forth and a back move by a finite block of any length at level β. Defined by well-founded recursion on α; use blockBFEquiv_iff.

Equations

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

theorem FirstOrder.Language.blockBFEquiv_iff {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (α : Ordinal.{u_1}) {n : ℕ} (a : Fin n → M) (b : Fin n → N) : BlockBFEquiv α n a b ↔ SameAtomicType a b ∧ ∀ β < α, (∀ (k : ℕ) (c : Fin k → M), ∃ (d : Fin k → N), BlockBFEquiv β (n + k) (Fin.append a c) (Fin.append b d)) ∧ ∀ (k : ℕ) (d : Fin k → N), ∃ (c : Fin k → M), BlockBFEquiv β (n + k) (Fin.append a c) (Fin.append b d)

The public equation of BlockBFEquiv.

theorem FirstOrder.Language.BlockBFEquiv.sameAtomicType {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{u_1}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BlockBFEquiv α n a b) : SameAtomicType a b

theorem FirstOrder.Language.BlockBFEquiv.forth {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α β : Ordinal.{u_1}} (hβ : β < α) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BlockBFEquiv α n a b) (k : ℕ) (c : Fin k → M) : ∃ (d : Fin k → N), BlockBFEquiv β (n + k) (Fin.append a c) (Fin.append b d)

theorem FirstOrder.Language.BlockBFEquiv.back {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α β : Ordinal.{u_1}} (hβ : β < α) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BlockBFEquiv α n a b) (k : ℕ) (d : Fin k → N) : ∃ (c : Fin k → M), BlockBFEquiv β (n + k) (Fin.append a c) (Fin.append b d)

theorem FirstOrder.Language.blockBFEquiv_zero {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) : BlockBFEquiv 0 n a b ↔ SameAtomicType a b

Level 0 is atomic agreement.

theorem FirstOrder.Language.BlockBFEquiv.monotone {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α β : Ordinal.{u_1}} (hβα : β ≤ α) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BlockBFEquiv α n a b) : BlockBFEquiv β n a b

theorem FirstOrder.Language.BlockBFEquiv.toBFEquiv {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{u_1}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BlockBFEquiv α n a b) : BFEquiv α n a b

Block level α gives single-element level α: a block of length one is a single move.

theorem FirstOrder.Language.BFEquiv.toBlock {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{u_1}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv (Ordinal.omega0 * α) n a b) : BlockBFEquiv α n a b

Single-element level ω·α gives block level α: a k-block at β < α is matched by forth_block at level ω·β + k ≤ ω·α.

theorem FirstOrder.Language.bfEquiv_all_iff_blockBFEquiv_all {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} : (∀ (α : Ordinal.{uι}), BFEquiv α n a b) ↔ ∀ (α : Ordinal.{uι}), BlockBFEquiv α n a b

Equivalence at every level is convention-independent.

Block orbit rank and block Scott rank

def FirstOrder.Language.blockOrbitStable {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : Set Ordinal.{w}

The block stabilization set, all-levels form (Harrison-Trainor–Igusa–Knight Definition 1.3(1)).

Equations

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

theorem FirstOrder.Language.orbitRank_mem_blockOrbitStable {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a ∈ blockOrbitStable a

The single-element orbit rank is a block stabilization level.

theorem FirstOrder.Language.blockOrbitStable_nonempty {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : (blockOrbitStable a).Nonempty

noncomputable def FirstOrder.Language.blockOrbitRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : Ordinal.{w}

Block orbit rank.

Equations

• FirstOrder.Language.blockOrbitRank a = sInf (FirstOrder.Language.blockOrbitStable a)

theorem FirstOrder.Language.blockOrbitRank_mem {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : blockOrbitRank a ∈ blockOrbitStable a

theorem FirstOrder.Language.blockOrbitRank_le_of_mem {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {a : Fin n → M} {α : Ordinal.{w}} (h : α ∈ blockOrbitStable a) : blockOrbitRank a ≤ α

theorem FirstOrder.Language.blockOrbitRank_le_orbitRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : blockOrbitRank a ≤ orbitRank a

r_B ≤ r.

theorem FirstOrder.Language.orbitRank_le_omega_mul_blockOrbitRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a ≤ Ordinal.omega0 * blockOrbitRank a

r ≤ ω·r_B.

noncomputable def FirstOrder.Language.blockScottRank {L : Language} (M : Type w) [L.Structure M] : Ordinal.{w}

Block Scott rank R_B = ⨆ (r_B(a) + 1).

Equations

• FirstOrder.Language.blockScottRank M = ⨆ (x : (n : ℕ) × (Fin n → M)), FirstOrder.Language.blockOrbitRank x.snd + 1

theorem FirstOrder.Language.blockOrbitRank_add_one_le_blockScottRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : blockOrbitRank a + 1 ≤ blockScottRank M

theorem FirstOrder.Language.blockScottRank_le {L : Language} {M : Type w} [L.Structure M] {β : Ordinal.{w}} (h : ∀ (n : ℕ) (a : Fin n → M), blockOrbitRank a + 1 ≤ β) : blockScottRank M ≤ β

theorem FirstOrder.Language.blockScottRank_le_internalScottRank {L : Language} {M : Type w} [L.Structure M] : blockScottRank M ≤ internalScottRank M

R_B ≤ R.

theorem FirstOrder.Language.internalScottRank_le_omega_mul_blockScottRank {L : Language} {M : Type w} [L.Structure M] : internalScottRank M ≤ Ordinal.omega0 * blockScottRank M

R ≤ ω·R_B, via r(a) + 1 ≤ ω·r_B(a) + 1 ≤ ω·(r_B(a) + 1) ≤ ω·R_B.

theorem FirstOrder.Language.blockScottRank_lt_of_internalScottRank_lt {L : Language} {M : Type w} [L.Structure M] {α : Ordinal.{w}} (h : internalScottRank M < α) : blockScottRank M < α

Strict bounds transfer downward for free.

theorem FirstOrder.Language.internalScottRank_lt_of_blockScottRank_lt {L : Language} {M : Type w} [L.Structure M] {α : Ordinal.{w}} (hcl : ∀ β < α, Ordinal.omega0 * β < α) (h : blockScottRank M < α) : internalScottRank M < α

Strict bounds transfer upward under the closure hypothesis ∀ β < α, ω·β < α, required explicitly here and not a standing assumption of the module. It is not implied by α being a countable limit (ω·2).

Infinite pure sets

@[instance_reducible]

def FirstOrder.Language.instStructureEmpty_infinitaryLogic_1 {X : Type w} : Language.empty.Structure X

Equations

• FirstOrder.Language.instStructureEmpty_infinitaryLogic_1 = FirstOrder.Language.emptyStructure

theorem FirstOrder.Language.blockOrbitRank_pureSet {X : Type w} [Infinite X] {n : ℕ} (a : Fin n → X) : blockOrbitRank a = 0

Every tuple of an infinite pure set has block orbit rank 0.

theorem FirstOrder.Language.blockScottRank_pureSet {X : Type w} [Infinite X] : blockScottRank X = 1

An infinite pure set has block Scott rank 1.