Delta Kernel Syntax Dformula

The δ object logic

In formal logic, a syntax is the bare alphabet and grammar of a language: which strings count as terms, which as formulas, before any meaning is assigned. The declaration DFormula, from the Recognition Science framework's machine-checked library of formal theorems, fixes that grammar for a deliberately tiny object language called the δ object logic. Its terms are built from just five shapes: a variable, zero, a successor step, addition, and multiplication. Its formulas add equality as the only basic predicate, plus the standard connectives (and, or, implies, false) and the two quantifiers (for all, exists). That is the whole language: intuitionistic first-order arithmetic over the signature {0, S, +, ·}.

The choice of signature is not accidental. Zero and successor are the primitive marks of the framework's ledger, a discrete record of events; addition and multiplication are the canonical operations that recursion on that structure licenses. The syntax deliberately excludes much that other logics take for granted. There is no universe hierarchy, no dependent product types, no inductive-type scheme, no propositions-as-types, no membership or comprehension. Most strikingly, formulas are plain data. They never touch the host system's notion of truth: a formula is a syntactic object, and a derivation is a separate piece of data checked by a total function, not a judgment that the host logic endorses.

Because the language is so small, its bookkeeping is simple and fully structural. Variables are de Bruijn indices, numbers that point to the nearest enclosing binder. The operations lift and subst, which shift and replace variables, are defined by primitive recursion: no choice, no classical logic, nothing beyond mechanical symbol manipulation. The module imports nothing beyond the prelude of the proof assistant; it does not depend on any external mathematics library. This is the forcer's base: the free distinction structure ℕδ with its recursion-licensed operations, where the defining equations of addition and multiplication are axiom rules licensed by initiality, the principle the framework calls "freeness is forcing".

In Recognition Science, this syntax is the first layer of a forcing chain that aims to derive physical constants from the cost of recognition. The declaration itself proves nothing about physics. It establishes only that a certain minimal arithmetic can be written down cleanly, with no hidden assumptions from the host logic. What it does not claim is equally precise: it does not prove any arithmetic theorem, it does not interpret its formulas as propositions, and it says nothing about the physical world. It is the grammar, not the sentence.

/-- 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

/-- 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

DFormula does not prove any arithmetic theorem about its own terms or formulas. DFormula does not interpret its formulas as propositions in the host logic. DFormula does not say anything about the physical world or about recognition costs.

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: