Delta Kernel Syntax

The delta kernel language

Delta kernel syntax is the formal language at the base of the Recognition Science framework. It defines the symbols and rules for writing statements about the natural numbers: zero, the successor function (adding one), addition, and multiplication. These are the standard building blocks of arithmetic, expressed here in a formal system. The language is deliberately minimal, containing no sets, no functions that take other functions as input, and no way to treat a statement as a type. It only describes a structure of distinct, countable elements.

Within the framework, this structure is called the free distinction structure. The idea is that the natural numbers arise from a process of making distinctions, starting with zero and repeatedly taking a successor step. The syntax formalizes this by treating zero and successor as primitive, with addition and multiplication defined by recursion. Formulas are built from these terms using equality, logical connectives (and, or, implies), and quantifiers (for all, there exists). Negation is defined as implying falsehood, a choice consistent with intuitionistic logic.

The framework also handles the mechanics of variables. Variables are represented by de Bruijn indices, a standard technique where a variable is identified by how many binders (like a quantifier) are above it. The operations lift and subst shift and substitute variables correctly when moving under a binder. These are implemented as structural recursion, meaning they are simple, primitive operations with no hidden logical assumptions. A quantifier-free test is included to support a specific rule about Markov's principle.

In Recognition Science, this syntax is the foundation for a forced base. The framework's broader theory derives physical constants and structures from a cost function. This language provides the vocabulary in which that derivation is expressed, ensuring it rests on a clearly defined, minimal set of primitives. It establishes the basic grammar for all subsequent formal work in the framework.

/-- Terms over the distinction signature: de Bruijn variables, zero,
successor (the distinction step), addition, multiplication.
`0` and `S` are the primitive signature of the free distinction structure;
`+` and `·` are the canonical recursion-licensed extensions (their defining
equations are axiom rules in `Check.lean`, licensed by initiality:
"freeness is forcing"). -/
inductive DTerm : Type where
  | var  : Nat → DTerm
  | zero : DTerm
  | succ : DTerm → DTerm
  | add  : DTerm → DTerm → DTerm
  | mul  : DTerm → DTerm → DTerm

/-- Formulas of intuitionistic first-order arithmetic over the distinction
signature. Equality is the sole atomic predicate (identity of ledger
content). Negation is defined: `¬φ := φ → ⊥`. -/
inductive DFormula : Type where
  | eq   : DTerm → DTerm → DFormula
  | fls  : DFormula
  | conj : DFormula → DFormula → DFormula
  | disj : DFormula → DFormula → DFormula
  | impl : DFormula → DFormula → DFormula
  | all  : DFormula → DFormula
  | ex   : DFormula → DFormula

/-- Shift the free variables `≥ c` up by `d`. -/
def lift (d c : Nat) : DTerm → DTerm
  | var n   => if n < c then var n else var (n + d)
  | zero    => zero
  | succ t  => succ (t.lift d c)
  | add t s => add (t.lift d c) (s.lift d c)
  | mul t s => mul (t.lift d c) (s.lift d c)

/-- Substitute `s` for variable `k` (binder instantiation: free variables
above `k` shift down by one). -/
def subst (k : Nat) (s : DTerm) : DTerm → DTerm
  | var n   => if n = k then s else if k < n then var (n - 1) else var n
  | zero    => zero
  | succ t  => succ (subst k s t)
  | add t u => add (subst k s t) (subst k s u)
  | mul t u => mul (subst k s t) (subst k s u)

What this page does not claim

This module does not prove any theorems about arithmetic. This module does not define the cost function or derive any physical constants. This module does not introduce a universe hierarchy or dependent types.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/DeltaKernel/Syntax.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: