Q with the order axioms is consistent, by exhibiting a model

Identifier: F:fo-qle-consistency
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

There is no derivation of falsity from the thirteen axioms of FO.Qle -- Robinson's seven plus the six order axioms -- in the first-order natural-deduction calculus: Not (FO.Provable FO.Qle FO.Formula.bot). The proof is soundness applied at the ℕ structure with the constant-zero valuation, exactly as for FO.Q: a derivation of bot from Qle would give FO.sat Nat FO.natStructureQ FO.Formula.bot v, which iota-reduces to False.

Formal statement

theorem FO.Qle.consistency : Not (FO.Provable FO.Qle FO.Formula.bot)

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

2 direct dependencies 0 direct dependents

Evidence

kernel-FO.Qle.consistency

Kind: kernel-term
Status: checked

Supports: FO.Qle.consistency is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. The proof term is one line: fun d => FO.soundness Nat FO.natStructureQ FO.Qle FO.Formula.bot d (fun _ => Nat.zero) (FO.Qle.natModels (fun _ => Nat.zero)).

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_order_inventory -- FO.Qle.consistency --exact --require-axiom-free

Evidence notes

The ℕ structure is doing real work: an arbitrary FO.Structure M would not do, because M could be empty and the argument still needs a valuation Nat -> M to exist.

it-is-about-Qle-and-not-about-Q

Kind: kernel-term
Status: checked

Supports: The type is rebuilt from FO.Provable, FO.Qle and FO.Formula.bot inside the test and compared by Kernel::def_eq rather than by rendering, with a negative control that the SAME statement over FO.Q -- which is fo_robinson.rs's already-landed FO.Q.consistency -- is a DIFFERENT type. So a fact that had silently degraded to the strictly weaker statement about the smaller theory is a failure here.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_order::tests --test-threads=4

Evidence notes

fo_order::tests::qle_consistency_states_the_underivability_of_bot_from_qle.

Provenance

{
  "date": "2026-09-06",
  "established_by": "axeyum-lean-kernel build_fo_order_prelude, lane fo-diagonal-lemma (W3-7, ADR-1669)",
  "source": "authored from the roadmap item; the soundness route is fo_soundness.rs's, applied at the larger context",
  "prior_art": [
    {
      "who": "Raphael M. Robinson",
      "what": "the finitely axiomatised essentially undecidable arithmetic Q",
      "year": 1950,
      "where": "R. M. Robinson, 'An essentially undecidable axiom system', Proc. ICM 1950, vol. 1, 729-730",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}