The numeric predicates: the arithmetic expansion of a vocabulary

The vocabulary of the bottom class of the ordered world. A finite linearly ordered universe is an initial segment of ℕ, by the rank of an element (DescriptiveComplexity.orank, the number of its strict predecessors), and this file makes the arithmetic of that segment available to formulas: the language FirstOrder.Language.arith has a binary ≤ and two ternary symbols plus and times, interpreted on a finite linear order by

• plus x y z – orank x + orank y = orank z,
• times x y z – orank x * orank y = orank z.

Relations, not functions, and therefore truncated: a sum or product that does not fit in the universe simply has no witness, and “x + y overflows” is the first-order ¬∃z, plus x y z (DescriptiveComplexity.no_plus_iff_card_le).

Why relations of the order, and not a new sort of data

The numeric predicates are not extra input relations that an instance happens to carry: they are functions of the linear order, computed by orank. Three consequences, all of them design constraints rather than remarks.

• The canonical structure needs [LinearOrder A] [Finite A], where Mathlib's FirstOrder.Language.orderStructure needs only [LE A]. It is still an instance; it simply does not fire on an infinite type, which is correct – the arithmetic of an infinite universe is not what this vocabulary means.
• There is no order-free reading of this vocabulary at all. Every logic built on it is intrinsically a logic of ordered structures, and the class DescriptiveComplexity.AC0Definable accordingly has no …Free variant, unlike ∃SO, SO(LFP) or SO(PFP).
• Because the interpretation is canonical, an interpretation of one vocabulary in another does not get the numeric predicates for free: it must define the arithmetic of the interpreted universe, which is why the arithmetic analogue of DescriptiveComplexity.FOInterpretation.ordExtend is real work and not plumbing.

The transport from the ordered expansion

DescriptiveComplexity.sumOrderToArith is the language map L.sum Language.order →ᴸ L.sum Language.arith sending ≤ to ≤, with its FirstOrder.Language.LHom.IsExpansionOn instance, so that every FO(≤) sentence and every FO(≤) gadget formula of this library can be read as an arithmetic one (DescriptiveComplexity.FODefinable.ac0Definable is the consumer).

It is stated at the level of the sum rather than as a map Language.order →ᴸ Language.arith lifted by LHom.sumMap, deliberately: Language.order.Structure is not an instance in Mathlib (it would fire on every LE), so the generic sumMap instance would have to be fed a letI-supplied structure at every use site, whereas the sum-level map has both structures available by instance search.

What is here, and what needs it

Besides the vocabulary and its semantics: the formula builders (aLeF, aLtF, aPlusF, aTimesF, aMaxF, aMinF) with their realization lemmas, the overflow characterization, and one worked sentence – DescriptiveComplexity.evenCardSentence, which says that the universe has an even number of elements, by reading the parity of the rank of its greatest element. That sentence is what separates FO(≤) from AC⁰ (DescriptiveComplexity.Problems.Even), and it is the smallest example of the one thing the numeric predicates buy over a bare order: access to the size of the universe, one bit at a time.

inductive FirstOrder.Language.arithRel : ℕ → Type

Relation symbols of the arithmetic vocabulary.

• le : arithRel 2

  le x y: the rank of x is at most the rank of y, i.e., x ≤ y.

• plus : arithRel 3

  plus x y z: the ranks satisfy orank x + orank y = orank z.

• times : arithRel 3

  times x y z: the ranks satisfy orank x * orank y = orank z.

def FirstOrder.Language.instDecidableEqArithRel.decEq {a✝ : ℕ} (x✝ x✝¹ : arithRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqArithRel.decEq FirstOrder.Language.arithRel.le FirstOrder.Language.arithRel.le = isTrue FirstOrder.Language.instDecidableEqArithRel.decEq._proof_1
• FirstOrder.Language.instDecidableEqArithRel.decEq FirstOrder.Language.arithRel.plus FirstOrder.Language.arithRel.plus = isTrue FirstOrder.Language.instDecidableEqArithRel.decEq._proof_2
• FirstOrder.Language.instDecidableEqArithRel.decEq FirstOrder.Language.arithRel.plus FirstOrder.Language.arithRel.times = isFalse FirstOrder.Language.instDecidableEqArithRel.decEq._proof_3
• FirstOrder.Language.instDecidableEqArithRel.decEq FirstOrder.Language.arithRel.times FirstOrder.Language.arithRel.plus = isFalse FirstOrder.Language.instDecidableEqArithRel.decEq._proof_4
• FirstOrder.Language.instDecidableEqArithRel.decEq FirstOrder.Language.arithRel.times FirstOrder.Language.arithRel.times = isTrue FirstOrder.Language.instDecidableEqArithRel.decEq._proof_5

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqArithRel {a✝ : ℕ} : DecidableEq (arithRel a✝)

Equations

• FirstOrder.Language.instDecidableEqArithRel = FirstOrder.Language.instDecidableEqArithRel.decEq

def FirstOrder.Language.arith : Language

The relational vocabulary of the numeric predicates: a linear order and the graphs of addition and multiplication of ranks. Interpreted canonically on every finite linear order by DescriptiveComplexity.arithStructure.

Equations

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

instance FirstOrder.Language.instIsRelationalArith : Language.arith.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.arithLe : Language.arith.Relations 2

The order symbol of the arithmetic vocabulary.

Equations

• FirstOrder.Language.arithLe = FirstOrder.Language.arithRel.le

@[reducible, inline]

abbrev FirstOrder.Language.arithPlus : Language.arith.Relations 3

The addition symbol of the arithmetic vocabulary.

Equations

• FirstOrder.Language.arithPlus = FirstOrder.Language.arithRel.plus

@[reducible, inline]

abbrev FirstOrder.Language.arithTimes : Language.arith.Relations 3

The multiplication symbol of the arithmetic vocabulary.

Equations

• FirstOrder.Language.arithTimes = FirstOrder.Language.arithRel.times

The canonical interpretation on a finite linear order

@[instance_reducible]

instance DescriptiveComplexity.arithStructure (A : Type) [LinearOrder A] : FirstOrder.Language.arith.Structure A

The numeric predicates of a finite linear order: ≤ is the order, and plus/times are the graphs of addition and multiplication of ranks. Both are truncated: a value that is not the rank of an element of A is not related to anything.

Equations

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

@[simp]

theorem DescriptiveComplexity.relMap_arithLe {A : Type} [LinearOrder A] (x : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.arithLe x ↔ x 0 ≤ x 1

@[simp]

theorem DescriptiveComplexity.relMap_arithPlus {A : Type} [LinearOrder A] (x : Fin 3 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.arithPlus x ↔ orank (x 0) + orank (x 1) = orank (x 2)

@[simp]

theorem DescriptiveComplexity.relMap_arithTimes {A : Type} [LinearOrder A] (x : Fin 3 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.arithTimes x ↔ orank (x 0) * orank (x 1) = orank (x 2)

The symbols of the arithmetic expansion of a vocabulary

@[reducible, inline]

abbrev DescriptiveComplexity.aLeSym (L : FirstOrder.Language) : (L.sum FirstOrder.Language.arith).Relations 2

The order symbol, in the arithmetic expansion of L.

Equations

• DescriptiveComplexity.aLeSym L = Sum.inr FirstOrder.Language.arithLe

@[reducible, inline]

abbrev DescriptiveComplexity.aPlusSym (L : FirstOrder.Language) : (L.sum FirstOrder.Language.arith).Relations 3

The addition symbol, in the arithmetic expansion of L.

Equations

• DescriptiveComplexity.aPlusSym L = Sum.inr FirstOrder.Language.arithPlus

@[reducible, inline]

abbrev DescriptiveComplexity.aTimesSym (L : FirstOrder.Language) : (L.sum FirstOrder.Language.arith).Relations 3

The multiplication symbol, in the arithmetic expansion of L.

Equations

• DescriptiveComplexity.aTimesSym L = Sum.inr FirstOrder.Language.arithTimes

The numeric predicates of the arithmetic expansion

@[simp]

theorem DescriptiveComplexity.relMap_aLeSym {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (x : Fin 2 → A) : FirstOrder.Language.Structure.RelMap (aLeSym L) x ↔ x 0 ≤ x 1

@[simp]

theorem DescriptiveComplexity.relMap_aPlusSym {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (x : Fin 3 → A) : FirstOrder.Language.Structure.RelMap (aPlusSym L) x ↔ orank (x 0) + orank (x 1) = orank (x 2)

@[simp]

theorem DescriptiveComplexity.relMap_aTimesSym {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (x : Fin 3 → A) : FirstOrder.Language.Structure.RelMap (aTimesSym L) x ↔ orank (x 0) * orank (x 1) = orank (x 2)

The transport of an ordered formula into the arithmetic expansion

def DescriptiveComplexity.sumOrderToArith (L : FirstOrder.Language) [L.IsRelational] : L.sum FirstOrder.Language.order →ᴸ L.sum FirstOrder.Language.arith

The arithmetic expansion extends the ordered one: the language map sending the order symbol of Language.order to the order symbol of Language.arith, and every input symbol to itself.

Equations

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

instance DescriptiveComplexity.sumOrderToArith_isExpansionOn {L : FirstOrder.Language} [L.IsRelational] (A : Type) [L.Structure A] [LinearOrder A] : (sumOrderToArith L).IsExpansionOn A

The transport is an expansion: both vocabularies read ≤ as the order and the input symbols as themselves.

Formula builders

noncomputable def DescriptiveComplexity.aLeF {L : FirstOrder.Language} {α : Type} (x y : α) : (L.sum FirstOrder.Language.arith).Formula α

x ≤ y, as a formula over the arithmetic expansion.

Equations

• DescriptiveComplexity.aLeF x y = (DescriptiveComplexity.aLeSym L).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.aLtF {L : FirstOrder.Language} {α : Type} (x y : α) : (L.sum FirstOrder.Language.arith).Formula α

x < y, as a formula over the arithmetic expansion.

Equations

• DescriptiveComplexity.aLtF x y = DescriptiveComplexity.aLeF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.aLeF y x)

noncomputable def DescriptiveComplexity.aPlusF {L : FirstOrder.Language} {α : Type} (x y z : α) : (L.sum FirstOrder.Language.arith).Formula α

x + y = z, as a formula over the arithmetic expansion.

Equations

• DescriptiveComplexity.aPlusF x y z = (DescriptiveComplexity.aPlusSym L).formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.aTimesF {L : FirstOrder.Language} {α : Type} (x y z : α) : (L.sum FirstOrder.Language.arith).Formula α

x * y = z, as a formula over the arithmetic expansion.

Equations

• DescriptiveComplexity.aTimesF x y z = (DescriptiveComplexity.aTimesSym L).formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.aMinF {L : FirstOrder.Language} {α : Type} (x : α) : (L.sum FirstOrder.Language.arith).Formula α

The variable x holds a minimum.

Equations

• DescriptiveComplexity.aMinF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.aLeF (Sum.inl x) (Sum.inr 0))

noncomputable def DescriptiveComplexity.aMaxF {L : FirstOrder.Language} {α : Type} (x : α) : (L.sum FirstOrder.Language.arith).Formula α

The variable x holds a maximum.

Equations

• DescriptiveComplexity.aMaxF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.aLeF (Sum.inr 0) (Sum.inl x))

@[simp]

theorem DescriptiveComplexity.realize_aLeF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x y : α) : (aLeF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.realize_aLtF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x y : α) : (aLtF x y).Realize v ↔ v x < v y

@[simp]

theorem DescriptiveComplexity.realize_aPlusF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x y z : α) : (aPlusF x y z).Realize v ↔ orank (v x) + orank (v y) = orank (v z)

@[simp]

theorem DescriptiveComplexity.realize_aTimesF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x y z : α) : (aTimesF x y z).Realize v ↔ orank (v x) * orank (v y) = orank (v z)

@[simp]

theorem DescriptiveComplexity.realize_aMinF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x : α) : (aMinF x).Realize v ↔ ∀ (a : A), v x ≤ a

@[simp]

theorem DescriptiveComplexity.realize_aMaxF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x : α) : (aMaxF x).Realize v ↔ ∀ (a : A), a ≤ v x

Ranks, minima and covers

The order facts every walk over the ranks needs, stated once here because both routes to a complexity bound use them: the induction of DescriptiveComplexity.ArithmeticFixedPoint and the head programs of DescriptiveComplexity.HeadArith.

theorem DescriptiveComplexity.isMin_of_orank_eq_zero {A : Type} [LinearOrder A] [Finite A] {z : A} (h : orank z = 0) (a : A) : z ≤ a

An element of rank 0 is least.

theorem DescriptiveComplexity.orank_eq_succ_of_pred {A : Type} [LinearOrder A] [Finite A] {y' y : A} (h1 : y' < y) (h2 : ∀ (a : A), ¬(y' < a ∧ a < y)) : orank y = orank y' + 1

The rank of an element with an immediate predecessor is one more.

theorem DescriptiveComplexity.covBy_of_orank_succ {A : Type} [LinearOrder A] [Finite A] {w z : A} (h : orank z = orank w + 1) : w ⋖ z

A rank one higher is a cover: the converse of DescriptiveComplexity.orank_covBy, which is what lets a walk step a head by choosing the element of the next rank.

theorem DescriptiveComplexity.exists_pred_of_orank_succ {A : Type} [LinearOrder A] [Finite A] {z : A} {k : ℕ} (h : orank z = k + 1) : ∃ (z' : A), orank z' = k ∧ z' < z ∧ ∀ (a : A), ¬(z' < a ∧ a < z)

An element of positive rank has an immediate predecessor, of the rank below.

Truncation, and the size of the universe

theorem DescriptiveComplexity.no_plus_iff_card_le {A : Type} [LinearOrder A] [Finite A] (x y : A) : (¬∃ (z : A), orank x + orank y = orank z) ↔ Nat.card A ≤ orank x + orank y

Addition is truncated at the size of the universe: a sum has a witness exactly when it is small enough to be a rank. This is what makes “x + y overflows” a first-order statement.

theorem DescriptiveComplexity.even_card_iff_forall_isTop {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : Even (Nat.card A) ↔ ∀ (z : A), (∀ (a : A), a ≤ z) → ¬∃ (h : A), orank h + orank h = orank z

The parity of the universe is a numeric predicate. The greatest element has rank Nat.card A - 1, so the universe has an even number of elements exactly when no element doubles to the greatest one. The order alone cannot say this (DescriptiveComplexity.even_not_foDefinable); addition can.

A sentence for the parity of the universe

noncomputable def DescriptiveComplexity.evenCardSentence (L : FirstOrder.Language) : (L.sum FirstOrder.Language.arith).Sentence

The universe has an even number of elements, as a sentence of the arithmetic expansion: no maximum is the double of anything. The two quantifiers are the whole sentence – nothing about the input vocabulary is read, so this is a statement about the size of the instance, which is exactly what a bare order cannot express and the numeric predicates can.

Equations

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

@[simp]

theorem DescriptiveComplexity.realize_evenCardSentence {L : FirstOrder.Language} (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : A ⊨ evenCardSentence L ↔ Even (Nat.card A)