The bit-level logic, and definability in it

The syntax the machines of DescriptiveComplexity.LogTime.Machine decide, and an API for building sentences of it the way DescriptiveComplexity.LogTime.Definable builds sentences of FO(≤, +, ×): semantically, from the connectives and the quantifiers, with the sentence read off only at the end.

The logic

DescriptiveComplexity.BitAtom, over an arbitrary type of variables: the order, the addition of ranks, the bit at an index BitIx i x, and an input relation at a tuple of variables. Four atoms, and nothing here is ×. This is FO(≤, +, BIT) in the classical naming – BIT(x, i) with i an element – which is what makes the bit atom a reading the machine can perform at a guessed address, and the arithmetic of positions the plain arithmetic of the universe.

A DescriptiveComplexity.BitSentence is a quantifier prefix – a polarity per variable, exactly the shape a machine's registers have – over a quantifier-free DescriptiveComplexity.BitKernel. It is prenex by construction, and that is the point: a machine has no normal form to apply, so the logic must arrive in one.

Definability, and why the API is not the one for ArithDef

DescriptiveComplexity.BitDef says that a family of relations on valuations is realized by a prefix over a kernel, not by an arbitrary formula. So the closure lemmas cannot simply build a larger formula: each of them has to prenex as it goes, and the three lemmas that let it do so are in DescriptiveComplexity.LogTime.Machine – DescriptiveComplexity.prefixHolds_not (negation dualizes a prefix), DescriptiveComplexity.prefixHolds_and_const (a prefix absorbs a side condition) and DescriptiveComplexity.prefixHolds_add (two prefixes concatenate). That is what replaces a normal-form theorem, and it is why disjunction is derived from negation and conjunction rather than proved: doing so costs one congr instead of a fourth prefix lemma.

Where it lands

DescriptiveComplexity.BitDef.bitDefinable reads a closed relation as a sentence, and DescriptiveComplexity.BitDefinable.ac0Definable translates the whole logic into FO(≤, +, ×) atom by atom. Three of the four atoms translate outright (DescriptiveComplexity.arithDef_le, _plus, _rel); the bit atom goes through DescriptiveComplexity.powArithDef, the definability of i ↦ 2 ^ i, which is proved in DescriptiveComplexity.LogTime.Pow and so costs the statement no hypothesis. The converse direction, that a machine's acceptance is a sentence of this logic rather than of the arithmetic one, is DescriptiveComplexity.LogTime.Simulate.

The syntax

inductive DescriptiveComplexity.BitAtom (L : FirstOrder.Language) (γ : Type) : Type

The atoms of the bit-level logic: the order, the addition of ranks, the bit of an element at an index, and an input relation at a tuple of variables.

• le {L : FirstOrder.Language} {γ : Type} (x y : γ) : BitAtom L γ

  x ≤ y.

• plus {L : FirstOrder.Language} {γ : Type} (x y z : γ) : BitAtom L γ

  orank x + orank y = orank z.

• bit {L : FirstOrder.Language} {γ : Type} (i x : γ) : BitAtom L γ

  The bit of x at the index i is set.

• rel {L : FirstOrder.Language} {γ : Type} {a : ℕ} (R : L.Relations a) (arg : Fin a → γ) : BitAtom L γ

  An input relation at a tuple of variables.

inductive DescriptiveComplexity.BitKernel (L : FirstOrder.Language) (γ : Type) : Type

A quantifier-free kernel over the bit-level atoms.

• atom {L : FirstOrder.Language} {γ : Type} (a : BitAtom L γ) : BitKernel L γ

  An atom.

• tt {L : FirstOrder.Language} {γ : Type} : BitKernel L γ

  The constant true, so that a trivial relation needs no dummy variable.

• not {L : FirstOrder.Language} {γ : Type} (k : BitKernel L γ) : BitKernel L γ

  Negation.

• and {L : FirstOrder.Language} {γ : Type} (k k' : BitKernel L γ) : BitKernel L γ

  Conjunction.

• or {L : FirstOrder.Language} {γ : Type} (k k' : BitKernel L γ) : BitKernel L γ

  Disjunction.

structure DescriptiveComplexity.BitSentence (L : FirstOrder.Language) : Type

A sentence of the bit-level logic, in prenex form: a polarity per variable and a quantifier-free kernel. Prenex by construction, which is what makes the compilation into a machine a matter of atoms rather than of normal forms.

• vars : ℕ

  The number of quantified variables.

• pol : Fin self.vars → Bool

  The quantifier at each variable: true existential, false universal.

• kernel : BitKernel L (Fin self.vars)

  The quantifier-free kernel.

def DescriptiveComplexity.BitAtom.Holds {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] [Finite A] : BitAtom L γ → (γ → A) → Prop

What an atom says of a valuation.

Equations

• (DescriptiveComplexity.BitAtom.le x_2 y).Holds x✝ = (x✝ x_2 ≤ x✝ y)
• (DescriptiveComplexity.BitAtom.plus x_2 y z).Holds x✝ = (DescriptiveComplexity.orank (x✝ x_2) + DescriptiveComplexity.orank (x✝ y) = DescriptiveComplexity.orank (x✝ z))
• (DescriptiveComplexity.BitAtom.bit i x_2).Holds x✝ = DescriptiveComplexity.BitIx (x✝ i) (x✝ x_2)
• (DescriptiveComplexity.BitAtom.rel R arg).Holds x✝ = FirstOrder.Language.Structure.RelMap R fun (t : Fin a) => x✝ (arg t)

def DescriptiveComplexity.BitAtom.relabel {L : FirstOrder.Language} {γ δ : Type} (f : γ → δ) : BitAtom L γ → BitAtom L δ

Renaming the variables of an atom.

Equations

• DescriptiveComplexity.BitAtom.relabel f (DescriptiveComplexity.BitAtom.le x_1 y) = DescriptiveComplexity.BitAtom.le (f x_1) (f y)
• DescriptiveComplexity.BitAtom.relabel f (DescriptiveComplexity.BitAtom.plus x_1 y z) = DescriptiveComplexity.BitAtom.plus (f x_1) (f y) (f z)
• DescriptiveComplexity.BitAtom.relabel f (DescriptiveComplexity.BitAtom.bit i x_1) = DescriptiveComplexity.BitAtom.bit (f i) (f x_1)
• DescriptiveComplexity.BitAtom.relabel f (DescriptiveComplexity.BitAtom.rel R arg) = DescriptiveComplexity.BitAtom.rel R fun (t : Fin a) => f (arg t)

theorem DescriptiveComplexity.BitAtom.holds_relabel {L : FirstOrder.Language} {γ δ A : Type} [L.Structure A] [LinearOrder A] [Finite A] (f : γ → δ) (a : BitAtom L γ) (v : δ → A) : (relabel f a).Holds v ↔ a.Holds (v ∘ f)

Renaming is composition on the valuation.

def DescriptiveComplexity.BitKernel.Holds {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] [Finite A] : BitKernel L γ → (γ → A) → Prop

What a kernel says of a valuation.

Equations

• (DescriptiveComplexity.BitKernel.atom a).Holds x✝ = a.Holds x✝
• DescriptiveComplexity.BitKernel.tt.Holds x✝ = True
• k.not.Holds x✝ = ¬k.Holds x✝
• (k.and k').Holds x✝ = (k.Holds x✝ ∧ k'.Holds x✝)
• (k.or k').Holds x✝ = (k.Holds x✝ ∨ k'.Holds x✝)

def DescriptiveComplexity.BitKernel.relabel {L : FirstOrder.Language} {γ δ : Type} (f : γ → δ) : BitKernel L γ → BitKernel L δ

Renaming the variables of a kernel.

Equations

• DescriptiveComplexity.BitKernel.relabel f (DescriptiveComplexity.BitKernel.atom a) = DescriptiveComplexity.BitKernel.atom (DescriptiveComplexity.BitAtom.relabel f a)
• DescriptiveComplexity.BitKernel.relabel f DescriptiveComplexity.BitKernel.tt = DescriptiveComplexity.BitKernel.tt
• DescriptiveComplexity.BitKernel.relabel f k.not = (DescriptiveComplexity.BitKernel.relabel f k).not
• DescriptiveComplexity.BitKernel.relabel f (k.and k') = (DescriptiveComplexity.BitKernel.relabel f k).and (DescriptiveComplexity.BitKernel.relabel f k')
• DescriptiveComplexity.BitKernel.relabel f (k.or k') = (DescriptiveComplexity.BitKernel.relabel f k).or (DescriptiveComplexity.BitKernel.relabel f k')

theorem DescriptiveComplexity.BitKernel.holds_relabel {L : FirstOrder.Language} {γ δ A : Type} [L.Structure A] [LinearOrder A] [Finite A] (f : γ → δ) (k : BitKernel L γ) (v : δ → A) : (relabel f k).Holds v ↔ k.Holds (v ∘ f)

Renaming is composition on the valuation.

def DescriptiveComplexity.BitSentence.Holds {L : FirstOrder.Language} (φ : BitSentence L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] : Prop

What a sentence says of an instance: the prefix, played over the kernel.

Equations

• φ.Holds A = DescriptiveComplexity.prefixHolds φ.vars φ.pol fun (v : Fin φ.vars → A) => φ.kernel.Holds v

def DescriptiveComplexity.BitDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is bit-definable when a prenex sentence over the order, the addition and the bit at an index – FO(≤, +, BIT) – decides it on every nonempty finite ordered structure.

Equations

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

Definable relations with free variables

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

A family of relations is bit-definable when one quantifier prefix over one quantifier-free bit-level kernel realizes it in every nonempty finite ordered structure. The free variables are indexed by α, the quantified ones by Fin k, exactly as a machine's registers are.

Equations

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

theorem DescriptiveComplexity.elim_comp_map {γ δ α A : Type} (v : α → A) (u : γ → A) (f : δ → γ) : Sum.elim v u ∘ Sum.map id f = Sum.elim v (u ∘ f)

Composing a valuation with a renaming that fixes the free variables.

theorem DescriptiveComplexity.BitDef.congr {α : Type} {L : FirstOrder.Language} {R S : ArithRel L α} (h : BitDef R) (he : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A] (v : α → A), R A v ↔ S A v) : BitDef S

Definability transfers along a pointwise equivalence of relations.

theorem DescriptiveComplexity.BitDef.relabel {α β : Type} {L : FirstOrder.Language} {R : ArithRel L α} (h : BitDef R) (f : α → β) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : β → A) => R A (v ∘ f)

Renaming the free variables.

Connectives

theorem DescriptiveComplexity.BitDef.not {α : Type} {L : FirstOrder.Language} {R : ArithRel L α} (h : BitDef R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ¬R A v

The negation of a bit-definable relation is bit-definable: the prefix dualizes.

theorem DescriptiveComplexity.BitDef.and {α : Type} {L : FirstOrder.Language} {R S : ArithRel L α} (h : BitDef R) (h' : BitDef S) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => R A v ∧ S A v

The conjunction of two bit-definable relations is bit-definable: the two prefixes concatenate.

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

The always-true relation is bit-definable.

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

The always-false relation is bit-definable.

theorem DescriptiveComplexity.BitDef.or {α : Type} {L : FirstOrder.Language} {R S : ArithRel L α} (h : BitDef R) (h' : BitDef S) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => R A v ∨ S A v

The disjunction of two bit-definable relations is bit-definable, by De Morgan: one congr rather than a fourth prefix lemma.

theorem DescriptiveComplexity.BitDef.imp {α : Type} {L : FirstOrder.Language} {R S : ArithRel L α} (h : BitDef R) (h' : BitDef S) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => R A v → S A v

An implication between bit-definable relations is bit-definable.

theorem DescriptiveComplexity.BitDef.iff {α : Type} {L : FirstOrder.Language} {R S : ArithRel L α} (h : BitDef R) (h' : BitDef S) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => R A v ↔ S A v

An equivalence between bit-definable relations is bit-definable.

theorem DescriptiveComplexity.BitDef.ite {α : Type} {L : FirstOrder.Language} {R S : ArithRel L α} (c : Prop) [Decidable c] (h : BitDef R) (h' : BitDef S) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => if c then R A v else S A v

A case distinction made outside the structure is bit-definable when both branches are.

theorem DescriptiveComplexity.BitDef.prop {α : Type} {L : FirstOrder.Language} (c : Prop) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (x_5 : α → x) => c

A truth value fixed outside the structure is bit-definable.

theorem DescriptiveComplexity.BitDef.forallFin {α : Type} {L : FirstOrder.Language} {k : ℕ} {R : Fin k → ArithRel L α} : (∀ (j : Fin k), BitDef (R j)) → BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (j : Fin k), R j A v

A finite conjunction of bit-definable relations, the index ranging over a Fin k of the machine rather than of the instance.

theorem DescriptiveComplexity.BitDef.forallFinite {α : Type} {L : FirstOrder.Language} {ι : Type} [Finite ι] {R : ι → ArithRel L α} (h : ∀ (j : ι), BitDef (R j)) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (j : ι), R j A v

A conjunction over any finite index of the machine.

theorem DescriptiveComplexity.BitDef.existsFinite {α : Type} {L : FirstOrder.Language} {ι : Type} [Finite ι] {R : ι → ArithRel L α} (h : ∀ (j : ι), BitDef (R j)) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∃ (j : ι), R j A v

A disjunction over any finite index of the machine, by De Morgan.

Quantifiers

theorem DescriptiveComplexity.BitDef.block {α : Type} {L : FirstOrder.Language} {m : ℕ} (polB : Fin m → Bool) {R : ArithRel L (α ⊕ Fin m)} (h : BitDef R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => prefixHolds m polB fun (w : Fin m → A) => R A (Sum.elim v w)

A quantifier prefix of m variables, prepended. The new block is outermost, so it is the first m indices of Fin (m + k); this is the one construction that touches the prefix, and exs/alls below are its constant-polarity instances. A machine's register list is the general case.

theorem DescriptiveComplexity.BitDef.exs {α : Type} {L : FirstOrder.Language} {m : ℕ} {R : ArithRel L (α ⊕ Fin m)} (h : BitDef R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∃ (w : Fin m → A), R A (Sum.elim v w)

Existential quantification of a block of m variables at once.

theorem DescriptiveComplexity.BitDef.alls {α : Type} {L : FirstOrder.Language} {m : ℕ} {R : ArithRel L (α ⊕ Fin m)} (h : BitDef R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (w : Fin m → A), R A (Sum.elim v w)

Universal quantification of a block of m variables at once.

theorem DescriptiveComplexity.BitDef.ex {α : Type} {L : FirstOrder.Language} {R : ArithRel L (α ⊕ Fin 1)} (h : BitDef R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∃ (a : A), R A (Sum.elim v fun (x : Fin 1) => a)

Existential quantification of one variable, in the layout the ArithDef API uses.

theorem DescriptiveComplexity.BitDef.all {α : Type} {L : FirstOrder.Language} {R : ArithRel L (α ⊕ Fin 1)} (h : BitDef R) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (a : A), R A (Sum.elim v fun (x : Fin 1) => a)

Universal quantification of one variable, in the same layout.

Atoms

Every atom is a kernel with an empty prefix, so each of these is Iff.rfl.

theorem DescriptiveComplexity.bitDef_le {α : Type} {L : FirstOrder.Language} (x y : α) : 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) => v x ≤ v y

The order between two variables is bit-definable.

theorem DescriptiveComplexity.bitDef_plus {α : Type} {L : FirstOrder.Language} (x y z : α) : 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) + orank (v y) = orank (v z)

Addition of the ranks of three variables is bit-definable.

theorem DescriptiveComplexity.bitDef_bit {α : Type} {L : FirstOrder.Language} (i 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) => BitIx (v i) (v x)

The bit at an index is bit-definable: it is an atom of this logic, and the one the machine reads by addressing.

theorem DescriptiveComplexity.bitDef_rel {α : Type} {L : FirstOrder.Language} {a : ℕ} (R : L.Relations a) (arg : Fin a → α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => FirstOrder.Language.Structure.RelMap R fun (t : Fin a) => v (arg t)

Reading the input: an input relation at a tuple of variables is bit-definable. In the machine reading of this logic it is the query instruction.

theorem DescriptiveComplexity.bitDef_lt {α : Type} {L : FirstOrder.Language} (x y : α) : 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) => v x < v y

The strict order is bit-definable.

theorem DescriptiveComplexity.bitDef_isZero {α : Type} {L : FirstOrder.Language} (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) = 0

Being the least element is bit-definable: x + x = x.

theorem DescriptiveComplexity.bitDef_isOne {α : Type} {L : FirstOrder.Language} (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) = 1

Being the least nonzero element is bit-definable. Where FO(≤, +, ×) reads orank x = 1 off the idempotence x * x = x, this logic has no × and reads it off the order: nonzero, and below every nonzero element.

theorem DescriptiveComplexity.bitDef_isMax {α : Type} {L : FirstOrder.Language} (x : α) : BitDef fun (A : Type) (x_1 : L.Structure A) (x_2 : LinearOrder A) (x_3 : Finite A) (x_4 : Nonempty A) (v : α → A) => ∀ (k : A), k ≤ v x

Being the greatest element is bit-definable, through the order alone.

theorem DescriptiveComplexity.bitDef_isTopIx {α : Type} {L : FirstOrder.Language} (i : α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => IsTopIx (v i)

The top index is bit-definable, and with nothing but the order and the bit atom: it is the highest index carrying a bit of the greatest element (DescriptiveComplexity.isTopIx_iff_bits). This is where the index naming pays for itself – the end of the tape is read, where the place-value naming had to compute a doubling that overflows.

theorem DescriptiveComplexity.bitDef_isLowIx {α : Type} {L : FirstOrder.Language} (i : α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => IsLowIx (v i)

A low index is bit-definable in the same way: one with a bit of the greatest element above it.

theorem DescriptiveComplexity.bitDef_eq {α : Type} {L : FirstOrder.Language} (x y : α) : 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) => v x = v y

Equality is bit-definable, through the order.

Into FO(≤, +, ×)

The translation that makes the bit-level logic a sub-notion of DescriptiveComplexity.AC0Definable without going through the machine: atom by atom, then the Boolean structure, then the prefix. Doing it here rather than through DescriptiveComplexity.LTDecidable.ac0Definable is what lets the simulation of a machine land in this logic rather than in the arithmetic one.

theorem DescriptiveComplexity.BitAtom.arithDef {L : FirstOrder.Language} {γ : Type} (a : BitAtom L γ) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : γ → x) => a.Holds v

Every bit-level atom is an atom of FO(≤, +, ×) – the bit atom through the naming bridge DescriptiveComplexity.powArithDef, the other three outright.

theorem DescriptiveComplexity.BitKernel.arithDef {L : FirstOrder.Language} {γ : Type} (k : BitKernel L γ) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : γ → x) => k.Holds v

Every quantifier-free kernel is a formula of FO(≤, +, ×).

def DescriptiveComplexity.peelVar {α : Type} (k : ℕ) : α ⊕ Fin (k + 1) → (α ⊕ Fin k) ⊕ Fin 1

The renaming that peels the innermost quantified variable, moving it out of the block and into the Fin 1 the ArithDef quantifiers bind.

Equations

• DescriptiveComplexity.peelVar k = Sum.elim (fun (a : α) => Sum.inl (Sum.inl a)) fun (i : Fin (k + 1)) => Fin.lastCases (Sum.inr 0) (fun (j : Fin k) => Sum.inl (Sum.inr j)) i

theorem DescriptiveComplexity.elim_comp_peelVar {α A : Type} {k : ℕ} (u : α ⊕ Fin k → A) (a : A) : (Sum.elim u fun (x : Fin 1) => a) ∘ peelVar k = Sum.elim (fun (x : α) => u (Sum.inl x)) (Fin.snoc (fun (j : Fin k) => u (Sum.inr j)) a)

Peeling a variable is Fin.snoc on the valuation.

theorem DescriptiveComplexity.arithDef_prefixHolds {L : FirstOrder.Language} {α : Type} (k : ℕ) (pol : Fin k → Bool) {S : ArithRel L (α ⊕ Fin k)} : ArithDef S → ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => prefixHolds k pol fun (w : Fin k → A) => S A (Sum.elim v w)

A quantifier prefix is a block of ArithDef quantifiers.

From a closed relation to a sentence

theorem DescriptiveComplexity.BitDef.bitDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} {R : ArithRel L Empty} (h : BitDef R) (hP : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], P.Holds A ↔ R A Empty.elim) : BitDefinable P

The bridge to DescriptiveComplexity.BitDefinable: a bit-definable relation with no free variables is a sentence of the bit-level logic.

theorem DescriptiveComplexity.BitDefinable.ac0Definable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : BitDefinable P) : AC0Definable P

The bit-level logic is inside FO(≤, +, ×): a BitSentence is an AC⁰ definition, proved directly rather than through the machine. Its bit atom is translated by DescriptiveComplexity.powArithDef, which is Immerman 1999 Thm 1.17(2); every other atom is a formula of the two numeric predicates outright.