First-order logic with canonical numerical predicates

Canonical expansions make order, BIT, addition, and multiplication available to the existing FO syntax. Numerical atoms have their specified natural-number semantics; input formulas embed without changing truth. The computable expansion agrees with its propositional counterpart, so the existing Boolean evaluator can check formulas on these expansions.

This supplies the semantic interfaces for FO[BIT] and FO[ADD, MUL]. Their equality of expressive power, formula definitions of one arithmetic basis from the other, and the uniform circuit capture theorem remain separate results.

@[simp]

theorem Complexity.DescriptiveComplexity.FinStruct.withNumerical_card {V : Vocabulary} (A : FinStruct V) (predicates : List NumericalPredicate) : (A.withNumerical predicates).card = A.card

Canonical numerical expansion preserves the universe exactly.

@[simp]

theorem Complexity.DescriptiveComplexity.FOInterpretation.forgetNumerical_apply {V : Vocabulary} (A : FinStruct V) (predicates : List NumericalPredicate) : (forgetNumerical V predicates).apply (A.withNumerical predicates) = A

Forgetting the added symbols recovers the original structure.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.withNumerical_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (φ : Formula V n) (predicates : List NumericalPredicate) (σ : Env A.card n) : Sat (A.withNumerical predicates) σ (φ.withNumerical predicates) ↔ Sat A σ φ

Embedding an input formula into the numerical vocabulary preserves satisfaction.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.numerical_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (predicates : List NumericalPredicate) (r : Fin predicates.length) (args : Fin (predicates.get r).arity → Term (V.withNumerical predicates) n) (σ : Env A.card n) : Sat (A.withNumerical predicates) σ (numerical predicates r args) ↔ (predicates.get r).Holds fun (i : Fin (predicates.get r).arity) => ↑(Term.eval (A.withNumerical predicates) σ (args i))

A designated numerical atom has its canonical meaning on the evaluated arguments.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.orderLt_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (x y : Term V.withOrder n) (σ : Env A.card n) : Sat (A.withNumerical [NumericalPredicate.lt]) σ (orderLt x y) ↔ ↑(Term.eval (A.withNumerical [NumericalPredicate.lt]) σ x) < ↑(Term.eval (A.withNumerical [NumericalPredicate.lt]) σ y)

The order atom compares the natural indices of its two elements.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.bit_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (x i : Term V.withBit n) (σ : Env A.card n) : Sat (A.withNumerical [NumericalPredicate.bit]) σ (bit x i) ↔ (↑(Term.eval (A.withNumerical [NumericalPredicate.bit]) σ x)).testBit ↑(Term.eval (A.withNumerical [NumericalPredicate.bit]) σ i) = true

BIT reads the indicated zero-based bit of the element's natural index.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.add_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (x y z : Term V.withArithmetic n) (σ : Env A.card n) : Sat (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ (add x y z) ↔ ↑(Term.eval (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ x) + ↑(Term.eval (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ y) = ↑(Term.eval (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ z)

ADD is the graph of natural addition, with all three elements in the finite universe.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.mul_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (x y z : Term V.withArithmetic n) (σ : Env A.card n) : Sat (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ (mul x y z) ↔ ↑(Term.eval (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ x) * ↑(Term.eval (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ y) = ↑(Term.eval (A.withNumerical [NumericalPredicate.add, NumericalPredicate.mul]) σ z)

MUL is the graph of natural multiplication, without modular wraparound.

@[simp]

theorem Complexity.DescriptiveComplexity.DecFinStruct.withNumerical_toFinStruct {V : Vocabulary} (A : DecFinStruct V) (predicates : List NumericalPredicate) : (A.withNumerical predicates).toFinStruct = A.toFinStruct.withNumerical predicates

The computable expansion has exactly the specified propositional semantics.

theorem Complexity.DescriptiveComplexity.FODefinable.withNumerical {V : Vocabulary} {Q : BooleanQuery V} (hQ : FODefinable Q) (predicates : List NumericalPredicate) : FODefinableWithNumerical predicates Q

Every input FO definition remains a definition after adding numerical predicates.