Falsehood is not derivable from the empty context in the first-order calculus

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

Recorded description

There is no derivation of bottom from the empty context in the first-order natural-deduction calculus FO.Provable. Established by pushing a hypothetical derivation through soundness at a concrete model -- the natural numbers with zero, successor, addition and strict order -- where the empty context is satisfied at every valuation and bottom is satisfied at none.

Formal statement

theorem FO.consistency : Not (FO.Provable FO.Context.nil FO.Formula.bot)

Dependencies

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

1 direct dependencies 2 direct dependents

Evidence

kernel-FO.consistency

Kind: kernel-term
Status: checked

Supports: FO.consistency is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. Its proof term is one line: 'fun d => FO.soundness AxNat FO.natStructure FO.Context.nil FO.Formula.bot d (fun _ => AxNat.zero) True.intro'. Soundness sends the assumed derivation to satisfaction of bot at the constant-zero valuation; ctxSat of the empty context iota-reduces to True, discharged by True.intro; and sat of bot iota-reduces to False.

Checker command

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

Evidence notes

The checker FAILS on absence rather than reporting an empty set. Declared in crates/axeyum-lean-kernel/src/fo_soundness.rs by declare_consistency.

statement-is-the-one-claimed

Kind: kernel-term
Status: checked

Supports: The theorem's inferred type is rebuilt in the test module as 'Not (FO.Provable FO.Context.nil FO.Formula.bot)' and compared by Kernel::def_eq, so a theorem that landed at some weaker statement about some other context or formula fails.

Checker command

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

Evidence notes

An unprovability claim is exactly the kind whose statement must be pinned: 'Not X' for the wrong X reads the same in prose.

the-model-is-not-degenerate

Kind: kernel-term
Status: checked

Supports: SAME-KIND POSITIVE CONTROL. A model in which NOTHING is satisfied would refute bot just as well and would make this fact worthless. FO.natStructure satisfies two genuine sentences, each landed as an axiom-free kernel theorem and each proved by kernel reduction: 'forall x, not (x < x)' and 'forall x, exists y, x < y'. So the same structure that refutes bot does satisfy first-order sentences with quantifiers in them.

Checker command

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

Evidence notes

Environment::contains is asserted BEFORE the footprint in that test, because axiom_footprint of an undeclared name is also empty -- so without it the test would pass for a theorem that failed to admit.

the-existential-sentence-reads-the-right-valuation-slots

Kind: kernel-term
Status: checked

Supports: The second sentence is the discriminating one. 'all (ex (rel2 0 (var 1) (var 0)))' has two nested binders reading de Bruijn indices 1 and 0, and its satisfaction reduces to 'forall x, exists y, x < y' ONLY IF the existential clause extends the valuation with the witness on top of the one the universal clause already extended. The test rebuilds that reduced form and compares by def_eq, and asserts the SWAPPED reading -- which is what an ex clause reading the wrong slot produces -- is NOT def_eq to it.

Checker command

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

Evidence notes

MUTATION-VERIFIED: making FO.sat's ex clause read the outer valuation is one of the two mutations lane model-theory ran. Kill counts are in docs/plan/archive/lanes/model-theory-2026-09-05.md.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_fo_soundness_prelude, lane model-theory (W3-6, ADR-1636)",
  "source": "authored from the roadmap item; the statement is written here, not extracted",
  "prior_art": [
    {
      "who": "standard",
      "what": "consistency of first-order logic follows from soundness together with the existence of a model; the argument is the textbook one",
      "year": 1935,
      "where": "any first-order logic text; the route here is soundness plus one concrete structure",
      "attribution": "standard textbook attribution; this lane did not consult a primary source"
    }
  ]
}