prop_ne_not
plain-language theorem explainer
Classical logic ensures no proposition equals its negation. Researchers on the self-bootstrap argument cite this meta-fact to separate distinguishability claims from their denials. The tactic proof assumes equality then applies case analysis on the truth value of P, deriving a contradiction in each branch.
Claim. In classical logic, for any proposition $P$, $P$ is never equal to its negation: $P ≠ ¬P$.
background
The SelfBootstrapDistinguishability module records the Lean-checkable meta-level facts for Route A of the absolute-floor program. It establishes that the formal language distinguishes propositions and that the proposition asserting object-level distinguishability differs from its denial, without deriving any object-level carrier from nothing.
proof idea
The proof introduces the assumption h : P = ¬P. It then performs by_cases on hp : P. The positive branch rewrites h to obtain ¬P and applies it to hp. The negative branch rewrites the symmetric h to obtain P and applies it to the assumption. Both branches close by contradiction.
why it matters
This result is invoked directly by dist_claim_self_distinguishes to prove (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y). It supplies the meta-language layer of the self-bootstrap argument in the Recognition framework, securing propositional distinguishability as a prerequisite for later object-level claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.