Excluded middle is not derivable in intuitionistic propositional logic

Identifier: F:excluded-middle-not-intuitionistic
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

There is no derivation of (p or not p), for a propositional variable p, in intuitionistic propositional natural deduction.

Formal statement

theorem ipc_excluded_middle_not_provable : Not (Provable FormulaList.nil (Formula.or_ (Formula.var AxNat.zero) (Formula.imp (Formula.var AxNat.zero) 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-ipc_excluded_middle_not_provable

Kind: kernel-term
Status: checked

Supports: ipc_excluded_middle_not_provable is admitted by the trusted kernel gate with the type recorded in formal.statement: there is no derivation of (p or not p) from the empty context in the Provable relation, the inductive encoding of IPC natural deduction.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example ipc_soundness_inventory -- ipc_excluded_middle_not_provable --require-axiom-free

Evidence notes

The checker FAILS on absence rather than reporting an empty set, verified both directions on 2026-08-30: the real name exits 0, and 'ipc_excluded_middle_not_provable_FABRICATED' exits 1 with 'an absent declaration is a failed check, not an empty report'. It lists every declaration kind, not only Declaration::Theorem, because a theorem inventory returns zero rows for a Definition and would answer the existence question wrongly in both directions. formal.statement is Kernel::render_lean of the admitted type, taken verbatim from that command's stdout, not transcribed by hand. Declared in crates/axeyum-lean-kernel/src/ipc_soundness.rs via declare_pem_not_provable.

kernel-ipc_soundness

Kind: kernel-term
Status: checked

Supports: The soundness theorem the result rests on: 'ipc_soundness : forall ctx phi, Provable ctx phi -> forall v, Le (ipc_ctx_meet ctx v) (ipc_eval phi v)', proved by induction on the DERIVATION -- an eleven-minor application of Provable.rec, one case per natural-deduction rule. This is the mathematical content; the headline theorem is its contraposition against the countermodel.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example ipc_soundness_inventory -- ipc_soundness --require-axiom-free

Evidence notes

Soundness is stated over the MEET of the context, not over a 'every context formula evaluates to top' predicate, because the latter does not carry an induction on derivations: in the imp_intro case the induction hypothesis only says 'if eval phi v = top then eval psi v = top', while the goal needs eval phi v <= eval psi v, and nothing constrains the case where eval phi v is the chain's MIDDLE element. imp_intro goes through by residuation and or_elim by the chain's linearity. Residuation needs ipc_ctx_meet <= 2, which is a real side condition and not decoration -- it is false at m = 3 (meet3 3 1 = 1 <= 1 but 3 <= himp3 1 1 = 2 is not) -- and is discharged by the separate theorem ipc_ctx_meet_le_top.

eleven-cases-and-the-composition

Kind: kernel-term
Status: checked

Supports: All eleven natural-deduction rules -- ax_head, weaken, and_intro, and_elim1, and_elim2, or_intro1, or_intro2, or_elim, imp_intro, imp_elim, bot_elim -- are discharged, each by a chain lemma admitted above it. The prelude does not build unless every one of them type-checks, so a successful build IS the check that no case was skipped.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_soundness::tests::slice_four_prelude_builds_and_declares_everything_it_names

Evidence notes

Mutation-verified on 2026-08-30 that this cannot pass on completion alone: replacing ipc_meet3_le_left with ipc_meet3_le_right in the ax_head case makes all 14 ipc_soundness tests fail. Restored.

countermodel-value-discriminates

Kind: kernel-term
Status: checked

Supports: The countermodel is specific rather than an algebra in which nothing reaches the top. At the SAME valuation p := 1: ipc_eval of (p or not p) is 1, and ipc_eval of the IPC-derivable (p -> p) is the top 2. One is refutable and the other is not, through the same evaluator.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_soundness::tests::pem_evaluates_to_one_and_a_tautology_evaluates_to_top_at_the_same_valuation

Evidence notes

Mutation-verified on 2026-08-30 that the headline theorem depends on this value: moving declare_pem_not_provable's valuation from 1 to 2 -- where (p or not p) IS the top, so nothing is refutable -- makes the kernel REJECT ipc_excluded_middle_not_provable with a TypeMismatch. Restored. This also ties the generic recursor-based evaluator back to F:heyting-3-chain-refutes-excluded-middle's direct-Nat computation of the same value.

positive-control-still-derivable

Kind: kernel-term
Status: checked

Supports: SAME-KIND positive control for an unprovability claim: the very same Provable relation still DERIVES 'p -> p' and '(p and q) -> p' from the empty context, as kernel-checked natural-deduction proof terms. Without this, 'the relation derives nothing' would explain the headline result just as well as the intended reading.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_soundness::tests::the_relation_still_derives_what_intuitionistic_logic_does_derive

Evidence notes

The two example derivations are from slice 2 (crates/axeyum-lean-kernel/src/ipc_provable.rs) and are built from the same eleven constructors the soundness induction eliminates.

sat-is-not-vacuous

Kind: kernel-term
Status: checked

Supports: The context-satisfaction predicate ipc_sat, and the corollary 'ipc_soundness_sat : Provable ctx phi -> forall v, ipc_sat ctx v -> Le 2 (ipc_eval phi v)'. ipc_sat is pinned in BOTH directions: a kernel theorem inhabits it at a satisfying valuation, and ipc_sat_not_vacuous REFUTES 'ipc_sat [var 0] (fun _ => 1)'. A constantly-true sat -- which would make the corollary vacuous and would satisfy any careless evaluation test -- cannot be refuted at all, so it could not pass this.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example ipc_soundness_inventory -- ipc_sat --require-axiom-free

Evidence notes

ipc_sat is a Definition, so kernel admission proves only that it is well-formed; its meaning is pinned by evaluation at concrete arguments (ipc_soundness::tests, magnitudes kept to 0/1/2 because these numerals are unary) plus the refutation above.

ctx-meet-computes-what-it-claims

Kind: kernel-term
Status: checked

Supports: ipc_ctx_meet is a Definition and the trusted gate cannot tell you a Definition is wrong, so its value is checked by reduction at concrete arguments against hand-computed values: 2 at nil, the head formula's value at a singleton, 0 when the tail drags it down, and 0 at [bot]. Two of those are discriminating -- the same list SHAPE with head var 0 gives 0 and with head var 1 gives 1 under the identity valuation, so a definition ignoring the head cannot pass, and [var 1, var 0] gives 0 where a tail-ignoring definition would give 1.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_soundness::tests::ctx_meet

Evidence notes

Four tests. Negative controls vary ONE small numeral rather than a whole term, since a FAILING def_eq has no early exit and a control differing in a large term is itself pathological.

footprint-whole-ipc-package

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- and not only for the headline theorem. All 50 declarations the IPC package adds on top of the Nat prelude (the Formula and FormulaList datatypes, the Provable relation with its eleven constructors and its recursor, the chain operations, the evaluator, and every theorem above) have an empty Kernel::axiom_footprint.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example ipc_soundness_inventory -- --require-axiom-free --expect-count 50

Evidence notes

The row set is a SET DIFFERENCE against a kernel carrying only build_nat_prelude, recomputed on every run, so it is derived from the environment rather than from a hand-maintained list -- a declaration nobody remembered to list still appears. --expect-count fails on drift in either direction.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum-lean-kernel build_ipc_soundness_prelude, lane ipc-soundness (slice 4), over slices 1-3 by lanes logic-excluded-middle, ipc-provable and ipc-eval",
  "source": "authored from the S:logic-and-proof strand of the math-education concept graph; statement written here, not copied",
  "prior_art": [
    {
      "citation": "Godel 1932; Heyting; Kripke 1965",
      "establishes": "the theorem, long settled, by three-valued and Kripke countermodels"
    },
    {
      "measurement": "cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory",
      "date": "2026-08-14",
      "result": "logic: axiom=0 opaque=0 quotient=0 total_trusted=0",
      "establishes": "axeyum's Lean logic prelude assumes nothing classical -- it declares only True, False, And, Or, Iff, Eq, Exists and Not (as `a -> False`). This measures the ABSENCE of a classical axiom in our kernel; it does not by itself prove the non-derivability, which is the cited theorem."
    },
    {
      "measurement": "cargo run -q --release -p axeyum-lean-kernel --example ipc_soundness_inventory -- --require-axiom-free --expect-count 50",
      "date": "2026-08-30",
      "result": "50 IPC declarations; axiom-free: yes (50 declarations checked)",
      "establishes": "The whole formalization -- formulas, contexts, the derivation relation, the evaluator, soundness, and the unprovability theorem -- rests on no axiom, no opaque declaration and no quotient."
    }
  ]
}