Successor on full tuple universes

A non-wrapping successor increments one coordinate, keeps earlier coordinates fixed and carries all later coordinates from maximum to zero. This is equivalent to increasing the arbitrary-base lexicographic rank by exactly one. The full tuple universe is essential to the interval argument.

The native carry compiler preserves quantifier-freeness when its supplied source successor is quantifier-free, as in Immerman's Exercise 1.33(2) with source SUC available. In the library's ≤/BIT basis, the canonical source successor instead uses a universal adjacency formula. Its compiled tuple formula is first-order, with one element quantifier in each carry alternative; no unconditional quantifier-free claim is made for this basis. Native full-tuple BIT is supplied in Ordered.TupleBit; numeric-preserving full-tuple composition is in Ordered.FullTuple.Composition.

Main definitions

• Cslib.Logic.FO.Ordered.IsCarrySuccessor: the coordinatewise carry condition.
• Cslib.Logic.FO.Ordered.tupleSuccOf: compile any supplied source successor using finite carries.
• Cslib.Logic.FO.Ordered.successor: canonical source adjacency, with one universal quantifier.
• Cslib.Logic.FO.Ordered.tupleSucc: the canonical full-tuple successor formula.

Main results

• Cslib.Logic.FO.Ordered.isCarrySuccessor_iff: the carry condition is exact rank successor.
• Cslib.Logic.FO.Ordered.isQF_tupleSuccOf: conditional preservation of quantifier-freeness.
• Cslib.Logic.FO.Ordered.realize_tupleSuccOf, Cslib.Logic.FO.Ordered.realize_tupleSucc: the generic and canonical formulas hold exactly at consecutive ranks.
• Cslib.Logic.FO.Ordered.not_realize_tupleSucc_zero, Cslib.Logic.FO.Ordered.not_realize_tupleSucc_of_max: zero-dimension and maximum boundaries.

References

• N. Immerman, Descriptive Complexity, Remark 1.32 and Exercise 1.33(2).

def Cslib.Logic.FO.Ordered.IsCarrySuccessor {n k : ℕ} (x y : Fin k → Fin n) : Prop

Non-wrapping increment of a tuple: one digit increases, with a maximum-to-zero suffix.

theorem Cslib.Logic.FO.Ordered.lexRank_succ_iff {n k : ℕ} (x y : Fin k → Fin n) : lexRank y = lexRank x + 1 ↔ lexRank x < lexRank y ∧ ∀ (z : Fin k → Fin n), ¬(lexRank x < lexRank z ∧ lexRank z < lexRank y)

Consecutive ranks are exactly strict tuple intervals with no intermediate tuple.

theorem Cslib.Logic.FO.Ordered.IsCarrySuccessor.lexRank_succ {n k : ℕ} {x y : Fin k → Fin n} (h : IsCarrySuccessor x y) : lexRank y = lexRank x + 1

A carry increment has no intermediate tuple in lexicographic order.

theorem Cslib.Logic.FO.Ordered.isCarrySuccessor_iff {n k : ℕ} (x y : Fin k → Fin n) : IsCarrySuccessor x y ↔ lexRank y = lexRank x + 1

The coordinatewise carry condition is exactly non-wrapping numerical successor.

noncomputable def Cslib.Logic.FO.Ordered.tupleSuccOf {L : FirstOrder.Language} (σ : (language L).Formula (Fin 2)) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Compile a supplied source successor formula into full-tuple successor by finite carries.

theorem Cslib.Logic.FO.Ordered.isQF_tupleSuccOf {L : FirstOrder.Language} {σ : (language L).Formula (Fin 2)} (hσ : FirstOrder.Language.BoundedFormula.IsQF σ) (k : ℕ) : FirstOrder.Language.BoundedFormula.IsQF (tupleSuccOf σ k)

The carry compiler introduces no quantifiers beyond those of the supplied successor.

noncomputable def Cslib.Logic.FO.Ordered.successor (L : FirstOrder.Language) : (language L).Formula (Fin 2)

Source successor in the canonical ≤ language: strict order with no intermediate point. The formula universally quantifies one element; it is not asserted quantifier-free.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_successor {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 → Fin n) : (successor L).Realize v ↔ ↑(v 1) = ↑(v 0) + 1

The canonical source formula defines ordinary, non-wrapping successor.

theorem Cslib.Logic.FO.Ordered.realize_tupleSuccOf {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {σ : (language L).Formula (Fin 2)} (hσ : ∀ (v : Fin 2 → Fin n), σ.Realize v ↔ ↑(v 1) = ↑(v 0) + 1) (v : Fin 2 × Fin k → Fin n) : (tupleSuccOf σ k).Realize v ↔ (lexRank fun (i : Fin k) => v (1, i)) = (lexRank fun (i : Fin k) => v (0, i)) + 1

Any correct source successor formula compiles to exact successor of lexicographic ranks.

noncomputable def Cslib.Logic.FO.Ordered.tupleSucc (L : FirstOrder.Language) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Canonical non-wrapping successor on the full arbitrary-base tuple universe.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_tupleSucc {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin k → Fin n) : (tupleSucc L k).Realize v ↔ (lexRank fun (i : Fin k) => v (1, i)) = (lexRank fun (i : Fin k) => v (0, i)) + 1

The canonical tuple successor formula holds exactly at consecutive numerical ranks.

theorem Cslib.Logic.FO.Ordered.not_realize_tupleSucc_zero {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin 0 → Fin n) : ¬(tupleSucc L 0).Realize v

The zero-dimensional full tuple universe is a singleton, so it has no successor pair.

theorem Cslib.Logic.FO.Ordered.not_realize_tupleSucc_of_max {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin k → Fin n) (hmax : (fun (i : Fin k) => v (0, i)) = tupleMax) : ¬(tupleSucc L k).Realize v

The maximum tuple has no successor; in particular, the formula does not wrap to zero.