Canonical numerical predicates for first-order logic

Append selected numerical relation symbols to an input vocabulary and interpret them canonically on Fin card. Order and BIT are binary; addition and multiplication are ternary graphs of natural arithmetic restricted to the universe, without modular wraparound. BIT takes the number before the bit index.

These extensions use the existing relation atoms, substitution, and semantics. Input relations and constants retain their meanings. Definability with numerical predicates is evaluated only on canonical expansions, so it does not assert invariance under arbitrary permutations of the original input structure.

The numerical-predicate convention follows Immerman's Descriptive Complexity and Schweikardt--Schwentick, A note on the expressive power of linear orders (2011), Section 2, https://lmcs.episciences.org/1008/pdf.

inductive Complexity.DescriptiveComplexity.NumericalPredicate : Type

Numerical relations available as designated symbols in a vocabulary extension.

• lt : NumericalPredicate

  Strict canonical order.

• bit : NumericalPredicate

  bit x i tests bit i of the natural number x, starting at zero.

• add : NumericalPredicate

  The ternary graph x + y = z of natural addition.

• mul : NumericalPredicate

  The ternary graph x * y = z of natural multiplication.

@[instance_reducible]

instance Complexity.DescriptiveComplexity.instDecidableEqNumericalPredicate : DecidableEq NumericalPredicate

Equations

• Complexity.DescriptiveComplexity.instDecidableEqNumericalPredicate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.NumericalPredicate.arity : NumericalPredicate → ℕ

Number of arguments of each designated numerical relation.

Equations

• Complexity.DescriptiveComplexity.NumericalPredicate.lt.arity = 2
• Complexity.DescriptiveComplexity.NumericalPredicate.bit.arity = 2
• Complexity.DescriptiveComplexity.NumericalPredicate.add.arity = 3
• Complexity.DescriptiveComplexity.NumericalPredicate.mul.arity = 3

def Complexity.DescriptiveComplexity.NumericalPredicate.Holds (p : NumericalPredicate) : (Fin p.arity → ℕ) → Prop

Interpret a numerical relation on natural-number arguments.

Equations

• Complexity.DescriptiveComplexity.NumericalPredicate.lt.Holds args = (args 0 < args 1)
• Complexity.DescriptiveComplexity.NumericalPredicate.bit.Holds args = ((args 0).testBit (args 1) = true)
• Complexity.DescriptiveComplexity.NumericalPredicate.add.Holds args = (args 0 + args 1 = args 2)
• Complexity.DescriptiveComplexity.NumericalPredicate.mul.Holds args = (args 0 * args 1 = args 2)

@[instance_reducible]

instance Complexity.DescriptiveComplexity.instDecidableHolds (p : NumericalPredicate) (args : Fin p.arity → ℕ) : Decidable (p.Holds args)

Equations

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

def Complexity.DescriptiveComplexity.Vocabulary.withNumerical (V : Vocabulary) (predicates : List NumericalPredicate) : Vocabulary

Append numerical relation symbols, preserving the input vocabulary's constants.

Equations

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

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.withOrder (V : Vocabulary) : Vocabulary

The input vocabulary with canonical strict order.

Equations

• V.withOrder = V.withNumerical [Complexity.DescriptiveComplexity.NumericalPredicate.lt]

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.withBit (V : Vocabulary) : Vocabulary

The input vocabulary with the canonical BIT predicate.

Equations

• V.withBit = V.withNumerical [Complexity.DescriptiveComplexity.NumericalPredicate.bit]

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.withArithmetic (V : Vocabulary) : Vocabulary

The input vocabulary with the graphs of addition and multiplication.

Equations

• V.withArithmetic = V.withNumerical [Complexity.DescriptiveComplexity.NumericalPredicate.add, Complexity.DescriptiveComplexity.NumericalPredicate.mul]

def Complexity.DescriptiveComplexity.FinStruct.withNumerical {V : Vocabulary} (A : FinStruct V) (predicates : List NumericalPredicate) : FinStruct (V.withNumerical predicates)

Expand an input structure by the selected canonical numerical relations.

Equations

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

def Complexity.DescriptiveComplexity.DecFinStruct.withNumerical {V : Vocabulary} (A : DecFinStruct V) (predicates : List NumericalPredicate) : DecFinStruct (V.withNumerical predicates)

The computable Boolean version of canonical numerical expansion.

Equations

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

def Complexity.DescriptiveComplexity.FOInterpretation.forgetNumerical (V : Vocabulary) (predicates : List NumericalPredicate) : FOInterpretation (V.withNumerical predicates) V

Forget the additional symbols through a quantifier-free first-order interpretation.

Equations

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

def Complexity.DescriptiveComplexity.Formula.withNumerical {V : Vocabulary} {n : ℕ} (φ : Formula V n) (predicates : List NumericalPredicate) : Formula (V.withNumerical predicates) n

Regard an input formula as a formula over the extended numerical vocabulary.

Equations

• φ.withNumerical predicates = (Complexity.DescriptiveComplexity.FOInterpretation.forgetNumerical V predicates).translate φ

def Complexity.DescriptiveComplexity.Formula.numerical {V : Vocabulary} {n : ℕ} (predicates : List NumericalPredicate) (r : Fin predicates.length) (args : Fin (predicates.get r).arity → Term (V.withNumerical predicates) n) : Formula (V.withNumerical predicates) n

Apply a selected numerical relation symbol to terms in the extended vocabulary.

Equations

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

def Complexity.DescriptiveComplexity.Formula.orderLt {V : Vocabulary} {n : ℕ} (x y : Term V.withOrder n) : Formula V.withOrder n

Strict canonical order as an ordinary first-order atom.

Equations

• Complexity.DescriptiveComplexity.Formula.orderLt x y = Complexity.DescriptiveComplexity.Formula.numerical [Complexity.DescriptiveComplexity.NumericalPredicate.lt] 0 ![x, y]

def Complexity.DescriptiveComplexity.Formula.bit {V : Vocabulary} {n : ℕ} (x i : Term V.withBit n) : Formula V.withBit n

The zero-based bit test, with the number before its bit index.

Equations

• Complexity.DescriptiveComplexity.Formula.bit x i = Complexity.DescriptiveComplexity.Formula.numerical [Complexity.DescriptiveComplexity.NumericalPredicate.bit] 0 ![x, i]

def Complexity.DescriptiveComplexity.Formula.add {V : Vocabulary} {n : ℕ} (x y z : Term V.withArithmetic n) : Formula V.withArithmetic n

Natural addition restricted to the finite universe, without modular wraparound.

Equations

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

def Complexity.DescriptiveComplexity.Formula.mul {V : Vocabulary} {n : ℕ} (x y z : Term V.withArithmetic n) : Formula V.withArithmetic n

Natural multiplication restricted to the finite universe, without modular wraparound.

Equations

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

def Complexity.DescriptiveComplexity.FODefinableWithNumerical {V : Vocabulary} (predicates : List NumericalPredicate) (Q : BooleanQuery V) : Prop

FO definability on the canonical expansions by the selected numerical predicates.

Equations

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