Peters and Westerståhl (2006): Quantifiers in Language and Logic

The quantifier LIN behind Intermediate Reciprocity, which relates any two distinct elements by a chain, is not definable in FO(Mon), first-order logic with every monadic quantifier added. Hella's bijective game cannot separate a directed cycle of length 2 ^ (r + 1) from two directed cycles of length 2 ^ r in r rounds, so the two satisfy the same sentences of FO(Mon) of quantifier rank ≤ r (duplicatorWinsBijective_oneCycle_twoCycles). LIN holds of the first and fails on the second (oneCycle_mem_lin, twoCycles_not_mem_lin), so no sentence of FO(Mon) defines it (lin_not_monDefinable): the reciprocal reading built on LIN is genuinely polyadic.

Implementation notes

The two models are the successor graphs of + 1 on ZMod (2 ^ (r + 1)) and of + (0, 1) on ZMod 2 × ZMod (2 ^ r), and the game is won by the general result for successor graphs of permutations with long cycles, FirstOrder.Language.duplicatorWinsBijective_successor.

TODO

• The relativization of LIN, Intermediate Reciprocity, is not definable from monadic quantifiers either; stating this needs the language with a unary and a binary relation symbol.

References

• [PW06]

def PetersWesterstahl2006.oneCycle (r : ℕ) : CategoryTheory.Bundled FirstOrder.Language.graph.Structure

One directed cycle of length 2 ^ (r + 1), as a structure in the language of graphs.

Equations

• PetersWesterstahl2006.oneCycle r = { α := ZMod (2 ^ (r + 1)), str := FirstOrder.Language.graphStructure fun (x y : ZMod (2 ^ (r + 1))) => y = (Equiv.addRight 1) x }

def PetersWesterstahl2006.twoCycles (r : ℕ) : CategoryTheory.Bundled FirstOrder.Language.graph.Structure

Two directed cycles of length 2 ^ r, as a structure in the language of graphs.

Equations

• PetersWesterstahl2006.twoCycles r = { α := ZMod 2 × ZMod (2 ^ r), str := FirstOrder.Language.graphStructure fun (x y : ZMod 2 × ZMod (2 ^ r)) => y = (Equiv.addRight (0, 1)) x }

theorem PetersWesterstahl2006.duplicatorWinsBijective_oneCycle_twoCycles (r : ℕ) : FirstOrder.Language.graph.DuplicatorWinsBijective r default default

Duplicator wins r rounds of the bijective game between one cycle of length 2 ^ (r + 1) and two of length 2 ^ r (Theorem 7).

theorem PetersWesterstahl2006.oneCycle_mem_lin (r : ℕ) : oneCycle r ∈ Reciprocal.lin.holds

On one cycle every element reaches every other, so LIN holds.

theorem PetersWesterstahl2006.twoCycles_not_mem_lin (r : ℕ) : twoCycles r ∉ Reciprocal.lin.holds

On two cycles no element reaches the other cycle, so LIN fails.

theorem PetersWesterstahl2006.lin_not_monDefinable : ¬FirstOrder.Language.graph.MonDefinable Set.univ Reciprocal.lin.holds

LIN is not definable in FO(Mon) (Corollary 8).