A contradiction needs evidence, too.

1. Falsity is a proposition, not a proof

The core node { kind: 'false' }, displayed as ⊥, represents falsity. It differs from an atom merely named False and from the JavaScript boolean false. Writing it down provides no evidence, and there is no falsity introduction rule.

Falsity elimination checks a child proof of ⊥ before concluding an explicitly annotated target P. The builder absurd(evidence, target) constructs that step. It cannot turn ordinary evidence of A into evidence of an unrelated B.

2. Negation uses implication

¬A means A → ⊥. To prove it, temporarily assume A, derive ⊥, and discharge A with implication introduction. Applying evidence of ¬A to evidence of A uses ordinary implication elimination.

The not(A) constructor returns implies(A, False). The proposition AST always shows that expansion, even when the formula uses ¬. Hover over or focus ¬ to inspect its one argument. Not having evidence of A is not evidence of ¬A.

3. Three proofs to inspect

A → ¬¬A: assume a : A and na : ¬A. Applying na to a yields ⊥. Discharge na, then a. This proof needs only assumption and implication rules.

(A → B) → (¬B → ¬A): assume f : A → B, nb : ¬B, and a : A. First apply f to a, then nb to the resulting B. Discharge a, nb, and f to obtain constructive contraposition.

⊥ → A: assume impossible : ⊥, use falsity elimination with target A, then discharge impossible. This is explosion. It proves an implication, not a closed proof of A or ⊥. All three examples can be checked in the playground.

4. Why the reverse is different

The invalid double-negation example offers ¬¬A where falsity elimination requires ⊥. That particular candidate is rejected. Rejecting one candidate does not establish that no proof exists.

To show that ¬¬A → A is not generally derivable, we can use a countermodel: an interpretation that preserves the constructive rules but does not establish this formula. This is a mathematical explanation outside the runtime checker.

5. A two-stage countermodel

Consider stages w₀ ≤ w₁. A is established only at w₁; ⊥ is established at neither stage. Established atoms stay established at later stages. An implication P → Q holds at a stage when every accessible stage, including itself, that establishes P also establishes Q.

Neither stage establishes ¬A, because w₁ establishes A without ⊥. Consequently both establish ¬¬A: there is no accessible stage establishing ¬A. At w₀, ¬¬A holds but A does not, so ¬¬A → A fails there.

The constructive rules preserve validity in these models. Therefore an assumption-free derivation of this formula for an arbitrary atom A cannot exist in this calculus. “Not established” is not the same as an established negation.

6. Search does not add rules

Future search may find candidates faster, but every result still needs the same kernel. A failed or timed-out search is inconclusive; adding search cannot invalidate the countermodel.

A classical axiom such as excluded middle changes the available assumptions and permits further theorems. That belongs to the later explicit-axioms milestone, where dependencies will be shown. It must not be smuggled into falsity elimination.