EVEN: the parity of a bare set

The textbook inexpressibility example (Ebbinghaus–Flum 1995, ch. 2; Immerman 1999, §6.1): over the empty vocabulary – a structure is nothing but a finite set – decide whether the universe has an even number of elements.

Nothing could be easier to compute, and nothing is further from first-order logic. No sentence defines it (DescriptiveComplexity.even_not_foDefinableFree) – one line of Ehrenfeucht–Fraïssé given the strategy on bare sets (DescriptiveComplexity.exists_card_bound_of_foDefinableFree): a sentence of quantifier rank n cannot tell a set with 2n + 2 elements from one with 2n + 3, the duplicator's supply of fresh elements outlasting the spoiler's rounds on both sides. And no sentence defines it with a linear order in hand either (DescriptiveComplexity.even_not_foDefinable), which is the theorem with content: the structure then determines the position of every point, and the duplicator still wins, for 2 ^ n rounds' worth of elements (DescriptiveComplexity.efEquiv_linearOrder).

Deciding it, on the other hand, is one walk along that same order – step to the immediate successor, flip a bit – so EVEN is FO(≤, TC) definable (DescriptiveComplexity.even_tcDefinable), hence in DescriptiveComplexity.NL. The two halves together give FO ⊊ FO(TC) (DescriptiveComplexity.exists_tcDefinable_not_foDefinable): a strict inclusion between two logics of this library, proved outright.

Deciding it needs no walk either, once formulas may do arithmetic: the greatest element has rank Nat.card A - 1, so EVEN is AC⁰ definable (DescriptiveComplexity.even_ac0Definable) by a sentence with one addition, whence FO(≤) ⊊ AC⁰ as well (DescriptiveComplexity.exists_ac0Definable_not_foDefinable). That is the parity of the universe; the parity of a marked subset is PARITY, the problem outside AC⁰, about which nothing here is claimed.

Below the addition it is one bit: Nat.card A is even exactly when the greatest element's rank is odd, that is, when its lowest bit is set. So EVEN is also a sentence of the bit-level logic of DescriptiveComplexity.LogTime – two existential registers over one bit atom (DescriptiveComplexity.even_bitDefinable) – hence decided by an alternating machine with a logarithmic clock (DescriptiveComplexity.even_ltDecidable) and, through the multi-head automaton that evaluates that logic, in LOGSPACE a second time (DescriptiveComplexity.even_mem_LOGSPACE_bit). The end of this file is where that stack is exercised end to end, and it is the template for writing any other sentence of that logic: semantically, with the DescriptiveComplexity.BitDef combinators, never as syntax.

This is the first unconditional separation of the library – no complexity assumption enters, in contrast with everything the completeness results say, which is why the game layer is worth its cost.

The problem

def DescriptiveComplexity.EVEN : DecisionProblem FirstOrder.Language.empty

EVEN: the universe has an even number of elements. The vocabulary is empty, so a yes-instance is nothing but a finite set of even size, and the problem is invariant for the strongest possible reason – isomorphic bare sets are equinumerous.

Equations

• DescriptiveComplexity.EVEN = { Holds := fun (A : Type) (x : FirstOrder.Language.empty.Structure A) => Even (Nat.card A), iso_invariant := @DescriptiveComplexity.EVEN._proof_1 }

theorem DescriptiveComplexity.even_holds_iff (A : Type) [FirstOrder.Language.empty.Structure A] : EVEN.Holds A ↔ Even (Nat.card A)

The value of EVEN at a bare set, unfolded.

EVEN is not first-order

The two witnesses are Fin (2 * n + 2) and Fin (2 * n + 3): of different parity, and both larger than the quantifier rank n that would have to tell them apart.

theorem DescriptiveComplexity.even_not_foDefinableFree : ¬FODefinableFree EVEN

EVEN is not first-order definable. A defining sentence of quantifier rank n would have to separate two bare sets of at least n elements each, which the duplicator's strategy (DescriptiveComplexity.efEquiv_bare) forbids.

EVEN is not first-order even with an order

The order-free result above says little on its own: a bare set carries no information beyond its size, and a sentence of quantifier rank n sees that size only up to n. The order-invariant statement is the real theorem – the structure now does determine every point's position, and the sentence may speak about it – and it needs Ehrenfeucht's theorem (DescriptiveComplexity.efEquiv_linearOrder), whose bound is exponential rather than linear in the quantifier rank.

theorem DescriptiveComplexity.even_not_foDefinable : ¬FODefinable EVEN

EVEN is not first-order definable, even order-invariantly: no sentence over the ordered expansion defines it, however it uses the order. A defining sentence of quantifier rank n would have to separate two finite linear orders of 2 ^ n * 2 and 2 ^ n * 2 + 1 elements, which the duplicator's strategy on a line (DescriptiveComplexity.efEquiv_linearOrder) forbids.

Together with DescriptiveComplexity.even_tcDefinable below, this is the unconditional strict inclusion FO ⊊ FO(TC), and, through the inclusions the library proves for the classes above DescriptiveComplexity.NL, the statement that first-order logic is strictly weaker than every logic here.

EVEN is a transitive closure

The other half of the separation: parity is trivially computable, and with a linear order at hand it is a single walk – step to the immediate successor, flip a bit. Written as a DescriptiveComplexity.TCSpec, the walk carries the bit as its mode and the current element as its (one-element) tuple.

noncomputable def DescriptiveComplexity.parityMode {A : Type} [LinearOrder A] [Finite A] (x : A) : Bool

The parity mode carried at an element: true where the rank is even, that is, after an odd number of elements has been visited.

Equations

• DescriptiveComplexity.parityMode x = decide (Even (DescriptiveComplexity.orank x))

noncomputable def DescriptiveComplexity.evenStep (m m' : Bool) : (FirstOrder.Language.empty.sum FirstOrder.Language.order).Formula (Fin 1 ⊕ Fin 1)

The transition of the parity walk: step to the immediate successor, flipping the mode. Between modes that are not opposite there is no transition.

Equations

• DescriptiveComplexity.evenStep m m' = if m' = !m then DescriptiveComplexity.succF (Sum.inl 0) (Sum.inr 0) else ⊥

noncomputable def DescriptiveComplexity.evenSrc (m : Bool) : (FirstOrder.Language.empty.sum FirstOrder.Language.order).Formula (Fin 1)

The walk starts at the minimum, in the mode of a set with one element visited.

Equations

• DescriptiveComplexity.evenSrc m = if m = true then DescriptiveComplexity.minF 0 else ⊥

noncomputable def DescriptiveComplexity.evenTgt (m : Bool) : (FirstOrder.Language.empty.sum FirstOrder.Language.order).Formula (Fin 1)

The walk accepts at the maximum, in the opposite mode: an even number of elements has been visited.

Equations

• DescriptiveComplexity.evenTgt m = if m = true then ⊥ else DescriptiveComplexity.maxF 0

noncomputable def DescriptiveComplexity.evenSpec : TCSpec FirstOrder.Language.empty

EVEN as a single transitive closure: one element walking the order, one bit of parity.

Equations

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

theorem DescriptiveComplexity.realize_evenStep {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] (m m' : Bool) (x y : Fin 1 → A) : (evenStep m m').Realize (Sum.elim x y) ↔ m' = !m ∧ x 0 ⋖ y 0

theorem DescriptiveComplexity.step_evenSpec_iff {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] (m m' : Bool) (x y : Fin 1 → A) : evenSpec.Step (m, x) (m', y) ↔ m' = !m ∧ x 0 ⋖ y 0

theorem DescriptiveComplexity.isSrc_evenSpec_iff {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] (m : Bool) (x : Fin 1 → A) : evenSpec.IsSrc (m, x) ↔ m = true ∧ ∀ (a : A), x 0 ≤ a

theorem DescriptiveComplexity.isTgt_evenSpec_iff {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] (m : Bool) (x : Fin 1 → A) : evenSpec.IsTgt (m, x) ↔ m = false ∧ ∀ (a : A), a ≤ x 0

theorem DescriptiveComplexity.parityMode_covBy {A : Type} [LinearOrder A] [Finite A] {w z : A} (h : w ⋖ z) : parityMode z = !parityMode w

The mode flips along a cover, since the rank increases by one.

theorem DescriptiveComplexity.reach_evenSpec {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] [Finite A] {x₀ : A} (h₀ : ∀ (a : A), x₀ ≤ a) (x : A) : evenSpec.Reach (true, fun (x : Fin evenSpec.k) => x₀) (parityMode x, fun (x_1 : Fin evenSpec.k) => x)

The walk reaches every element, in the mode its rank prescribes.

theorem DescriptiveComplexity.parityMode_of_reach {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] [Finite A] {x₀ : A} (h₀ : ∀ (a : A), x₀ ≤ a) (p : evenSpec.Node A) : evenSpec.Reach (true, fun (x : Fin evenSpec.k) => x₀) p → p.1 = parityMode (p.2 0)

The mode of a reachable node is the parity of its rank: the invariant that reads the walk backwards.

theorem DescriptiveComplexity.accepts_evenSpec_iff {A : Type} [FirstOrder.Language.empty.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : evenSpec.Accepts A ↔ Even (Nat.card A)

The walk accepts exactly the sets of even size: it visits every element once, from the minimum to the maximum, so the mode it ends in is the parity of the cardinality.

theorem DescriptiveComplexity.even_tcDefinable : TCDefinable EVEN

EVEN is FO(≤, TC) definable, by the parity walk.

theorem DescriptiveComplexity.exists_tcDefinable_not_foDefinable : ∃ (P : DecisionProblem FirstOrder.Language.empty), TCDefinable P ∧ ¬FODefinable P

FO ⊊ FO(TC), unconditionally. First-order logic with a transitive closure is strictly stronger than first-order logic on ordered finite structures: the inclusion is DescriptiveComplexity.FODefinable.tcDefinable, and EVEN separates the two – a single walk along the order defines it, and no sentence does. No complexity-theoretic assumption enters either half.

theorem DescriptiveComplexity.even_mem_NL : NL.Mem EVEN

EVEN is in NL – as far from first-order logic as it is easy to compute.

theorem DescriptiveComplexity.even_mem_PTIME : PTIME.Mem EVEN

EVEN is in PTIME.

EVEN is AC⁰: the numeric predicates see the size of the universe

No walk is needed either. A bare set carries no information beyond its size, and the size is exactly what the numeric predicates of DescriptiveComplexity.Arithmetic make visible: the greatest element has rank Nat.card A - 1, so the universe is even precisely when nothing doubles to it (DescriptiveComplexity.evenCardSentence, one ∀ and one ∃, using addition only). With DescriptiveComplexity.even_not_foDefinable this gives FO(≤) ⊊ AC⁰ outright.

This says nothing about PARITY. EVEN asks the parity of the universe – of the input's length, which a circuit family is indexed by and a sentence with + reads off the top rank. PARITY asks the parity of a marked subset, part of the input, and that is the problem outside AC⁰ by the switching lemma. The two must not be confused: nothing here bears on the second, and this library proves no AC⁰ lower bound.

theorem DescriptiveComplexity.even_ac0Definable : AC0Definable EVEN

EVEN is AC⁰ definable: 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 sentence DescriptiveComplexity.evenCardSentence, which mentions the input vocabulary not at all.

Contrast with PARITY, the parity of a marked subset, which is classically not in AC⁰: see the section docstring.

theorem DescriptiveComplexity.exists_ac0Definable_not_foDefinable : ∃ (P : DecisionProblem FirstOrder.Language.empty), AC0Definable P ∧ ¬FODefinable P

FO(≤) ⊊ AC⁰, unconditionally. First-order logic with the numeric predicates is strictly stronger than first-order logic with a bare linear order: the inclusion is DescriptiveComplexity.FODefinable.ac0Definable, and EVEN separates the two – addition reads the parity of the top rank, and no sentence over the order alone defines it, however it uses the order. No complexity-theoretic assumption enters either half.

This is the second unconditional separation of the library, beside DescriptiveComplexity.exists_tcDefinable_not_foDefinable, and it is the one that says the arithmetic is not decoration.

Order-free FO(IFP) does not capture PTIME

The order-invariant capture theorem lfpDefinable_iff_mem_PTIME says that over ordered structures a least fixed point defines exactly the polynomial time properties. Drop the order and the inflationary logic – which is the same logic there – no longer reaches all of PTIME, and EVEN is the witness: a k-variable induction cannot count past k pebbles, and two bare sets with k elements each are k-pebble equivalent whatever their sizes (DescriptiveComplexity.equivK₂_bare).

theorem DescriptiveComplexity.even_not_ifpDefinableFree : ¬IFPDefinableFree EVEN

EVEN is not order-free FO(IFP) definable: a defining induction with variable budget k – covering also the quantifier depth of its output sentence – would have to separate two bare sets of 2 * k + 2 and 2 * k + 3 elements, which DescriptiveComplexity.StepDef.ifpHolds_equivK₂ forbids.

theorem DescriptiveComplexity.exists_mem_PTIME_not_ifpDefinableFree : ∃ (P : DecisionProblem FirstOrder.Language.empty), PTIME.Mem P ∧ ¬IFPDefinableFree P

Order-free FO(IFP) does not capture PTIME, unconditionally – against DescriptiveComplexity.lfpDefinable_iff_mem_PTIME, which says it does over ordered structures. The order in every capture theorem of this library is therefore doing real work.

theorem DescriptiveComplexity.even_not_le_of_foDefinable {L : FirstOrder.Language} [L.IsRelational] {Q : DecisionProblem L} (hQ : FODefinable Q) : IsEmpty (OrderedFOReduction EVEN Q)

EVEN reduces to no first-order definable problem, whatever the target's vocabulary: parity escapes FO(≤) even with an order (DescriptiveComplexity.even_not_foDefinable), and definability travels backward along ordered reductions (DescriptiveComplexity.FODefinable.of_orderedReduction).

This is the library's first statement that a reduction does not exist; everything else it proves about the reduction order exhibits one.

EVEN in the bit-level logic

The parity of the universe is the lowest bit of its greatest element, so EVEN is a sentence of DescriptiveComplexity.BitDefinable – and therefore a machine, and therefore an automaton. Nothing here is new about EVEN; what it exercises is the bit-level stack of DescriptiveComplexity.LogTime, on the smallest instance there is.

theorem DescriptiveComplexity.even_iff_bitIx (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : Even (Nat.card A) ↔ ∃ (m : A) (z : A), (∀ (k : A), k ≤ m) ∧ orank z = 0 ∧ BitIx z m

The whole content of the bit-level reading: Nat.card A is even exactly when the greatest element's rank has its lowest bit set, orank of it being Nat.card A - 1.

theorem DescriptiveComplexity.even_bitDefinable : BitDefinable EVEN

EVEN is bit-definable: two existential registers over a single bit atom. The sentence is built with the DescriptiveComplexity.BitDef combinators – bitDef_isMax, bitDef_isZero, bitDef_bit, .and, .ex – and read off only at the end, exactly as DescriptiveComplexity.ArithDef is used one logic up. The variable layout is the only bookkeeping: an .ex binds the variables of Fin 1 in α ⊕ Fin 1, so the register bound first is the outer one and is reached through Sum.inl.

theorem DescriptiveComplexity.even_ltDecidable : LTDecidable EVEN

EVEN is decided by an alternating machine with a logarithmic clock: the compilation of the sentence above, register by register.

theorem DescriptiveComplexity.even_mem_LOGSPACE_bit : LOGSPACE.Mem EVEN

EVEN is in LOGSPACE by the bit-level route: the machine is evaluated by a deterministic multi-head automaton whose bit atom is the halving loop DescriptiveComplexity.HeadProgram.bitP. A second proof of a known fact – DescriptiveComplexity.even_ac0Definable gives it through AC⁰ – and the one that uses no part of Immerman's mutual definability.