Logical Foundations

This page describes the formal foundations of ImandraX's logic for readers interested in the theoretical underpinnings.

The big idea: everything is computation

In ImandraX, there is no separation between "programs" and "specifications." Your mathematical models, conjectures, and theorems are all written in one unified computational language — the same language you use to define functions is the language you use to state properties about them.

Every goal you want to prove is a boolean-valued function. Proving a theorem means showing that this function evaluates to true for all possible inputs. Refuting it means finding a counterexample — a concrete input you can plug in and watch the function evaluate to false.

This is what makes ImandraX's logic so natural:

Write a function. It's real, executable code.
Write a property. It's also a function — one that returns true or false.
Prove it. ImandraX shows the property-function always returns true.
Or refute it. ImandraX finds a specific input where it returns false — and you can run it yourself to see.

All goals are quantifier-free: universal quantification is implicit (the property must hold for all inputs), and existential witnesses are constructed automatically as counterexamples.

Recursion instead of quantifiers

In the spirit of Skolem's Primitive Recursive Arithmetic and Boyer-Moore logics like Nqthm and ACL2, ImandraX uses recursive functions where traditional logic would use quantifiers. This is far more than a stylistic choice — it has profound consequences for automated reasoning.

Consider the Fundamental Theorem of Arithmetic. In classical logic, you'd write:

∀n. ∃d. d is a prime decomposition of n ∧ d is unique up to permutation

That existential quantifier (∃d) is opaque — it asserts that a decomposition exists but says nothing about how to find it, hiding the very structure an automated prover would need to discover.

In ImandraX, you instead define a recursive function prime_factorization that actually computes the decomposition, and then prove:

theorem fta_existence n =
  n >= 2
  ==> product (prime_factorization n) = n
      && all_prime (prime_factorization n)
 
theorem fta_uniqueness n ps =
  n >= 2
  && product ps = n
  && all_prime ps
  ==> is_perm ps (prime_factorization n)

The existential is now a computable Skolem function — a real program that constructs the witness. ImandraX can mine this function's recursive structure to discover the right induction scheme, and it can run the function on concrete inputs to validate the theorem computationally before attempting a proof. The quantifier hasn't been "eliminated" — it's been implemented.

This pattern pervades ImandraX reasoning: instead of asserting that objects exist, you write functions that construct them. The result is that every theorem comes with a computational certificate, and ImandraX's automation has concrete recursive structure to work with rather than opaque logical connectives.

Classical reasoning, constructive validity

ImandraX uses reasoning principles of classical logic while being guaranteed its results are constructively valid. Since every proposition in the logic is a boolean-valued total function, classical reasoning (case splits, contradiction, excluded middle) is always sound with respect to constructive semantics — for any input, the function either returns true or false, so there is no tension between classical and constructive validity. This is closely related to the notion of decidable propositions in dependent type theory, where classical axioms are admissible for propositions with decidable truth values.

Absoluteness and set-theoretic robustness

There is a striking connection to absoluteness in set theory. By reducing mathematical statements to concrete computations over natural numbers and recursively defined data, ImandraX keeps reasoning within a fragment whose truth is highly invariant across models of set theory. In set-theoretic terms, statements about such computable predicates are highly absolute: their truth cannot change between different universes of sets.

This phenomenon is reflected in results such as Shoenfield's Absoluteness Theorem, which shows that sufficiently concrete analytic statements about integers and reals (Σ¹₂ statements) have the same truth value in all transitive models of ZFC with the same ordinals. Informally, once a mathematical claim has been reduced to the existence and properties of explicit computations, its truth becomes set-theoretically robust.

ImandraX's design deliberately pushes reasoning into this computationally explicit domain. When existence is realized as a program and propositions reduce to total boolean functions, theorems become not just logically provable but computationally witnessed and model-independent — a modern automated reasoning incarnation of the foundational insights behind Skolem arithmetic and recursive mathematics.

Portability across proof assistants

The recursive programs ImandraX reasons about correspond to well-founded computations whose termination can be measured by ordinals below ε₀ — the very same ordinal that Gentzen used to calibrate the strength of arithmetic itself. This fragment is remarkably robust across foundations: whether one works in classical higher-order logic (HOL), dependent type theory, or constructive type theory, these computational facts remain valid.

As a result, conjectures expressed in ImandraX live in a domain where essentially all modern theorem proving systems agree. Proof assistants such as Lean, Rocq/Coq, Isabelle/HOL, Agda, HOL-Light, and PVS may differ in their logical foundations — classical vs constructive, higher-order logic vs dependent types — but they all validate reasoning about total recursive functions and concrete computations over the natural numbers. When an ImandraX theorem reduces to such computational content, its proof obligations amount to statements about explicit programs and arithmetic. Those statements can be encoded and proved within each of these systems, meaning that the mathematical content of ImandraX theorems is portable across foundational frameworks.

In this sense, ImandraX operates near the shared intersection of modern proof assistants. Rather than depending on features unique to a particular logic, it concentrates on the common computational substrate that underlies them all.

The computational core of mathematics

Seen from the perspective of logic, this reflects a deep theme running through twentieth-century foundations. Gödel showed that arithmetic can encode computation, Skolem emphasized the role of recursive definitions in mathematics, and modern computability theory clarified that many mathematical truths ultimately reduce to properties of effective procedures. Results such as Shoenfield's Absoluteness Theorem then reveal that sufficiently concrete statements about such computations have stable truth across models of set theory.

If a theorem ultimately reduces to the correctness of a terminating computation, then any foundational system capable of expressing that computation must agree about its truth. In this sense, ImandraX operates at the computational core of mathematics — a domain where proofs are programs, witnesses are computations, and the resulting theorems are portable across the entire landscape of modern theorem provers.

Unrolling: surveying symbolic call-graphs

Recursive function unrolling then surveys the space of symbolic call-graphs that could possibly lead to a goal evaluating to false on symbolic inputs — incrementally expanding function definitions and checking satisfiability at each step. This gives ImandraX a beautiful way to combine rigorous formal logic with efficient construction of both counterexamples and proofs, all grounded in computation.

The core logic

ImandraX's logic is characterized as:

A (specializable) computational fragment of HOL extended with transfinite induction up to ε₀.

Let's unpack this:

Computational fragment of HOL

ImandraX's logic lives within Higher-Order Logic (HOL), but is restricted to the computational fragment — every function in the logic is executable. Unlike full HOL (as in HOL4, HOL Light, or Isabelle/HOL), you cannot define non-computable functions in ImandraX.

Specializable

The logic permits higher-order functions (functions taking functions as arguments), but these are always eliminable through:

Lambda lifting — Anonymous functions become named top-level definitions
Specialization — Higher-order functions applied to specific arguments are monomorphized into first-order recursive definitions
Monomorphization — Polymorphic type parameters are instantiated to concrete types

This means ImandraX can use higher-order syntax for expressiveness while targeting first-order reasoning backends for automation.

Induction up to ε₀

The proof-theoretic strength is computational HOL extended with transfinite induction up to ε₀ — a typed, higher-order analogue of Peano arithmetic and ACL2 (which are untyped and first-order, respectively) at the same proof-theoretic ordinal. This is powerful enough for virtually all program verification and concrete, scientifically relevant mathematics while remaining within well-understood theoretical bounds.

ε₀ (epsilon-zero) is the smallest ordinal not reachable by finite iterations of exponentiation from ω. Ordinals below ε₀ are encoded as a datatype in ImandraX using a variant of Cantor normal form.

This ordinal occupies a central place in the foundations of mathematics. In Gentzen's famous proof of the consistency of Peano Arithmetic, ε₀ appears as the proof-theoretic ordinal measuring the strength of arithmetic induction. Many sophisticated termination arguments for recursive programs correspond to decreasing measures in ordinals below ε₀. By allowing recursive definitions whose termination is justified by such well-founded measures, ImandraX can automatically reason about programs whose correctness ultimately relies on induction principles reaching up to this classical ordinal bound.

Conservative extensions

The most important principle in ImandraX's logic is the discipline of conservative extensions. Every new definition (type or function) must satisfy admissibility criteria that preserve the consistency of the logic:

Types must be well-founded

Every algebraic datatype must have no infinite descending chains. This ensures induction principles over the type are valid. In practice, this means every recursive type must have at least one non-recursive constructor (base case).

Functions must be total

Every recursive function must be proved terminating on all inputs. The termination proof uses an ordinal-valued measure — a function from the input to ordinals below ε₀ that strictly decreases on each recursive call.

The well-foundedness of the ordering on ordinals below ε₀ is an axiom of ImandraX's logic (one of only two axioms — the other being excluded middle).

Dual purpose of termination proofs

Termination proofs serve two roles:

Consistency preservation — Ensuring the defining equation doesn't introduce contradictions
Induction scheme synthesis — The recursion pattern of a function generates a tailored induction principle for proving properties about it

Relationship to other systems

vs. ACL2 / Boyer-Moore

The strongest acknowledged influence. ImandraX's inductive waterfall is "a lifting of the Boyer-Moore waterfall to our typed, higher-order setting." Key differences from ACL2:

	ACL2	ImandraX
Types	Untyped (dynamically typed)	Statically typed (algebraic datatypes)
Order	First-order	Higher-order (with specialization)
Surface language	Lisp (Common Lisp)	OCaml subset (IML)
Proof strength	Induction up to ε₀	Induction up to ε₀ (same)

vs. HOL (HOL4, HOL Light, Isabelle/HOL)

ImandraX's logic is a computational fragment of HOL. It shares the semantic foundation of classical higher-order logic but restricts to executable terms. Every ImandraX function can be evaluated, which is not generally true in HOL systems.

vs. Lean / Coq

Lean and Coq are based on dependent type theory (Calculus of Inductive Constructions), which is a more general logical foundation. ImandraX deliberately restricts to the computational subset — equivalent to the fragment of these systems in which all models and goals are executable. Every function is a terminating program, every proposition is a boolean-valued total function, and every existential witness is a computable Skolem function.

This restriction is what enables ImandraX's automation. By working in a logic where everything is computation, ImandraX can mine recursive structure for induction schemes, run functions on concrete inputs to validate conjectures, and synthesize counterexamples when properties fail. The result is that most proofs succeed with [@@by auto] — ImandraX's Boyer-Moore-style inductive waterfall handles them end-to-end without manual tactic guidance. And when conjectures are false, ImandraX's recursive function unrolling method can typically synthesize concrete counterexamples very efficiently — including counterexamples to higher-order goals that require synthesizing functions as witnesses. This matters enormously in practice: in real-world formal verification, most conjectures are initially false, and the bottleneck is not proving correct theorems but rapidly refuting incorrect ones and understanding why they fail. A system that can only say "proof failed" leaves the user stranded; one that produces a concrete, executable counterexample turns a dead end into actionable insight.

The mathematical content of ImandraX theorems lives in the shared intersection of all major proof assistants — see Portability across proof assistants.

vs. SMT solvers (Z3, CVC5, ...)

ImandraX is not an SMT solver, but it soundly integrates a configurable collection of both internal and external decision procedures and SMT solvers for ground theory reasoning, orchestrating a combination of them as appropriate. ImandraX has its own built-in decision procedures for arithmetic, datatypes, and congruence closure, and can also leverage external solvers (such as Z3 and CVC5) as ground-level backends. The key differentiator is that ImandraX adds induction, rewriting, and the full waterfall on top of ground reasoning, as well as support for higher-order functions and terms (SMT is traditionally limited to monomorphic multisorted first-order logic without recursion or induction) — lifting SMT-style techniques to a typed, higher-order setting with recursion and induction.

Soundness

ImandraX's consistency argument rests on:

Conservative extension discipline — Every admitted definition preserves consistency
Axiomatic well-foundedness — The well-foundedness of ordinals below ε₀ is taken as an axiom
Proof-theoretic correspondence — The logic is computational HOL extended with transfinite induction up to ε₀, placing it at the proof-theoretic strength of Peano arithmetic

Axioms break the guarantee

User-introduced axiom declarations bypass the conservative extension discipline and can introduce inconsistency. Only use axioms when you're confident they are consistent.