The 3-element Gödel/Łukasiewicz Heyting chain refutes excluded middle

Identifier: F:heyting-3-chain-refutes-excluded-middle
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Represent the 3-element linearly ordered Heyting algebra {0, 1, 2} directly as Nat values, with join3 = max, and himp3 a b = 2 (top) if a <= b else b (the Gödel/relative-pseudocomplement implication), and not3 a := himp3 a 0. At the valuation p := 1, join3(1, not3(1)) = 1, which is NOT the algebra's top element 2. So 'p or not p', evaluated in this Heyting algebra at p := 1, is not valid.

Formal statement

theorem ipc_heyting_join_not_ne_top : Not (Eq.{1} AxNat (join3 (AxNat.succ AxNat.zero) (not3 (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero)))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

kernel-ipc_heyting_join_not_ne_top

Kind: kernel-term
Status: checked

Supports: ipc_heyting_join_not_ne_top is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_heyting::tests::excluded_middle_countermodel_theorem_admits

Evidence notes

Declared in crates/axeyum-lean-kernel/src/ipc_heyting.rs via declare_excluded_middle_countermodel, proved from Nat.ne_of_beq_eq_false applied to Eq.refl at Eq Bool (Nat.beq 1 2) Bool.false -- the kernel's own ι-reduction discharges the proof, and the SAME proof term is accepted at the stronger stated type only because join3(1, not3(1)) is independently definitionally 1. formal.statement is Kernel::render_lean of the admitted type, captured verbatim from a temporary eprintln! in this test (not transcribed by hand).

compute-chain-operations

Kind: kernel-term
Status: checked

Supports: The evaluation table for meet3/join3/himp3/not3 at small, discriminating concrete arguments (never a single symmetric pair) matches the module docs' definitions of the 3-element chain exactly.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_heyting::tests::chain_operations_compute_the_intended_values

Evidence notes

meet3=min, join3=max, himp3=Gödel implication (top when a<=b, else b), not3(a)=himp3(a,0), all checked at every pairing of {0,1,2} that discriminates the three operations from each other.

non-vacuity-non-contradiction

Kind: kernel-term
Status: checked

Supports: The SAME-KIND positive control: at the SAME valuation p := 1 that refutes excluded middle, 'not (p and not p)' (the law of non-contradiction) DOES evaluate to top (2). The algebra rejects exactly the classically-but-not-intuitionistically-valid instance and accepts a genuinely IPC-valid one, which is what a real countermodel is supposed to do rather than reject everything.

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_heyting::tests::non_contradiction_holds_at_the_same_valuation_that_refutes_excluded_middle

Evidence notes

not3(meet3(1, not3(1))) = not3(0) = 2, computed and checked in-kernel.

footprint-ipc_heyting_join_not_ne_top

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- Kernel::axiom_footprint for this declaration is empty

Checker command

cargo test -p axeyum-lean-kernel --lib ipc_heyting::tests::excluded_middle_countermodel_theorem_is_axiom_free

Evidence notes

Reads Kernel::axiom_footprint(join_not_ne_top) directly (this kernel's #print axioms) and asserts it is empty, rather than inferring axiom-freedom from the absence of an Axiom variant in the source.

Provenance

{
  "date": "2026-08-29",
  "established_by": "axeyum-lean-kernel build_ipc_heyting_prelude, lane logic-excluded-middle",
  "source": "Standard result: the 3-element linearly ordered Gödel/Łukasiewicz Heyting algebra is a model of IPC in which excluded middle fails (see e.g. Rasiowa & Sikorski, or any Heyting-algebra-semantics treatment of IPC). Formalized here directly against Nat rather than as a Lean import.",
  "prior_art": [
    {
      "citation": "Standard Heyting-algebra semantics for IPC; the 3-element Gödel chain as the smallest algebra separating IPC from classical propositional logic.",
      "establishes": "That a finite linearly ordered Heyting algebra with more than 2 elements refutes excluded middle -- long settled."
    }
  ]
}