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.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.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.

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.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.

Quantifiers

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.

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. Registered in the Lax archive as Lax895169.ACZeroIsBitLogic.bitDefinable_ac0Definable.