Small universes are transparent: how to drop a size condition

Every packing argument of Immerman's mutual definability needs the universe to be above a concrete size – there is no room to lay a certificate out in a universe of three elements – and a statement gated by n ≥ N is a statement that has to carry n ≥ N for ever after. This file is what discharges such a hypothesis, and it is stated once for both logics:

A numeric relation – one that depends only on the size of the universe and on the ranks of its arguments – is definable on universes of at most k elements, whatever it is (DescriptiveComplexity.arithDef_of_card_le, DescriptiveComplexity.bitDef_of_card_le). So a numeric relation definable on the large universes is definable outright (DescriptiveComplexity.ArithDef.of_large, DescriptiveComplexity.BitDef.of_large).

The reason is that an order names its elements: orank x = j is first-order for each numeral j (DescriptiveComplexity.arithDef_orankEq, by j successors), and Nat.card A = n is first-order for each numeral n (DescriptiveComplexity.arithDef_cardEq). Below a fixed size there are finitely many (size, tuple of ranks) cases, so the relation is an explicit finite disjunction, one disjunct per case, each disjunct a conjunction of namings and a truth value decided outside the structure.

What it is for

A construction that lays out a certificate says what it needs of n and proves its statement for those n only; this turns that into the statement with no side condition. It is the shared prerequisite of two developments – the Bit Sum Lemma (LogTime/BitSum/, whose packing levels each need n above a bound) and the tuple arithmetic of AC⁰ class-hood (whose half-width splitting needs n ≥ 3) – and it is deliberately built before either.

The finiteness hypothesis is on the variables, not on anything else: a disjunction over the rank assignments of infinitely many variables is not a formula. Every consumer has finitely many, and states them as a Fin m.

Naming an element by its rank

theorem DescriptiveComplexity.arithDef_orankEq {L : FirstOrder.Language} (j : ℕ) {α : Type} (x : α) : ArithDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (v : α → x_1) => orank (v x) = j

orank x = j is first-order, for each numeral j: j steps of “add one”, each step one existential. The formula depends on j, and that is the point – it is a formula of the machine, not of the instance.

theorem DescriptiveComplexity.bitDef_orankEq {L : FirstOrder.Language} (j : ℕ) {α : Type} (x : α) : BitDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (v : α → x_1) => orank (v x) = j

The same, in the bit logic.

Naming the size of the universe

theorem DescriptiveComplexity.arithDef_cardGt {L : FirstOrder.Language} {α : Type} (k : ℕ) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (x_4 : α → A) => k < Nat.card A

The universe has more than k elements exactly when a rank k is attained, which is first-order by the naming above.

theorem DescriptiveComplexity.bitDef_cardGt {L : FirstOrder.Language} {α : Type} (k : ℕ) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (x_4 : α → A) => k < Nat.card A

The same, in the bit logic.

theorem DescriptiveComplexity.arithDef_cardEq {L : FirstOrder.Language} {α : Type} (n : ℕ) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (x_4 : α → A) => Nat.card A = n

The universe has exactly n elements: a rank n - 1 is attained and a rank n is not.

theorem DescriptiveComplexity.bitDef_cardEq {L : FirstOrder.Language} {α : Type} (n : ℕ) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (x_4 : α → A) => Nat.card A = n

The same, in the bit logic.

Numeric relations

def DescriptiveComplexity.IsNumeric {L : FirstOrder.Language} {α : Type} (R : ArithRel L α) : Prop

A family of relations is numeric when it is a function of the size of the universe and of the ranks of its arguments – which is what every statement of arithmetic is, and what an input relation is not.

Equations

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

theorem DescriptiveComplexity.isNumeric_of_ranks {L : FirstOrder.Language} {α : Type} {f : ℕ → (α → ℕ) → Prop} : IsNumeric fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => f (Nat.card A) fun (a : α) => orank (v a)

The relations a construction actually meets are numeric by inspection; this is the one that says so for an arithmetic statement of three variables.

Transparency

theorem DescriptiveComplexity.arithDef_of_card_le {L : FirstOrder.Language} {α : Type} [Finite α] {R : ArithRel L α} (k : ℕ) (h : IsNumeric R) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => Nat.card A ≤ k ∧ R A v

Below a fixed size, everything numeric is first-order: one disjunct per (size, tuple of ranks), each naming the size and every argument, and each carrying its truth value as a constant. Note what the disjunct does not do – it never looks at the instance, which is why the relation has to be numeric.

theorem DescriptiveComplexity.bitDef_of_card_le {L : FirstOrder.Language} {α : Type} [Finite α] {R : ArithRel L α} (k : ℕ) (h : IsNumeric R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => Nat.card A ≤ k ∧ R A v

The same, in the bit logic.

theorem DescriptiveComplexity.ArithDef.of_large {L : FirstOrder.Language} {α : Type} [Finite α] {R : ArithRel L α} (k : ℕ) (hnum : IsNumeric R) (h : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => k < Nat.card A ∧ R A v) : ArithDef R

The large case suffices: a numeric relation that is definable once the universe is big enough is definable, full stop. This is the lemma a packing argument quotes so that its size condition never reaches its statement.

theorem DescriptiveComplexity.BitDef.of_large {L : FirstOrder.Language} {α : Type} [Finite α] {R : ArithRel L α} (k : ℕ) (hnum : IsNumeric R) (h : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => k < Nat.card A ∧ R A v) : BitDef R

The same, in the bit logic.