Created
November 14, 2025 10:35
-
-
Save MikuroXina/68c906af05c42a4b77132a1372d4fada to your computer and use it in GitHub Desktop.
NAND calculus proofs for [The Incredible Proof Machine](https://incredible.pm/).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /- | |
| NAND 演算子 `↑` からなる計算系. `A` は「A が真」を, `A ↑ A` は「A が偽」を意味する. | |
| `A ↑ B` は「A と B が同時に真にならない」あるいは「A と B のいずれかが偽」を意味する. | |
| -/ | |
| def nand (a b : Prop): Prop := ¬(a ∧ b) | |
| infix:65 " ↑ " => nand | |
| variable {A B C : Prop} | |
| /-- | |
| 「A ならば not B」のとき,「A と B のいずれかが偽」を証明できる. | |
| -/ | |
| axiom nandI1 (x : A → B ↑ B) : A ↑ B | |
| /-- | |
| 「A が真」かつ「B と A のいずれかが偽」のとき, 「B が偽」を証明できる. | |
| -/ | |
| axiom nandE1 (x : A) (y : B ↑ A) : B ↑ B | |
| /-- | |
| 「A が真」かつ「A ならば B」のとき, 「B が真」を証明できる. | |
| -/ | |
| axiom nandE2 (x : A) (y : (B ↑ B) ↑ A) : B | |
| theorem nand_comm (x : A ↑ B) : B ↑ A := by | |
| apply nandI1 | |
| -- x : A ↑ B |- B → A ↑ A | |
| intro b | |
| -- x : A ↑ B, b : B |- A ↑ A | |
| exact nandE1 b x | |
| theorem nandI2 (x : A → B ↑ B) : B ↑ A := by | |
| exact nand_comm (nandI1 x) | |
| theorem ex_middle : (A ↑ A) ↑ A := by | |
| exact nandI1 (fun a => a) | |
| theorem or_right (b : B) : (B ↑ B) ↑ A := by | |
| have h1 : B ↑ B → A ↑ A := by | |
| intro not_b | |
| -- not_b : B ↑ B |- A ↑ A | |
| have h2 : A → B ↑ B := fun _ => not_b | |
| exact nandE1 b (nandI1 h2) | |
| exact nandI1 h1 | |
| theorem or_left (b : B) : A ↑ (B ↑ B) := by | |
| exact nand_comm (or_right b) | |
| theorem double_neg (x : A) : (A ↑ A) ↑ (A ↑ A) := by | |
| exact nandE1 x ex_middle | |
| theorem double_neg_inv (x : (A ↑ A) ↑ (A ↑ A)) : A := by | |
| have h1 : ((A ↑ A) ↑ A) ↑ (A ↑ A) := nandI1 (fun _ => x) | |
| have h2 : (A ↑ A) ↑ ((A ↑ A) ↑ A) := nand_comm h1 | |
| exact nandE2 ex_middle h2 | |
| theorem and (a : A) (b : B) : (A ↑ B) ↑ (A ↑ B) := by | |
| have h1 : (A ↑ B) ↑ B := nandI1 (fun (x : A ↑ B) => | |
| nandE1 a (nand_comm x) | |
| ) | |
| exact nandE1 b h1 | |
| theorem deduct (f : A → B) : (B ↑ B) ↑ A := by | |
| have h1 : A ↑ (B ↑ B) := nandI1 (fun a => | |
| double_neg (f a) | |
| ) | |
| exact nand_comm h1 | |
| theorem chain (x : (B ↑ B) ↑ A) (y : (C ↑ C) ↑ B) : (C ↑ C) ↑ A := by | |
| apply deduct | |
| intro a | |
| apply nandE2 _ y | |
| apply nandE2 _ x | |
| exact a | |
| theorem neg_explosive (x : A ↑ A) : (B ↑ B) ↑ A := by | |
| exact deduct (fun a => nandE2 x (nand_comm (deduct (fun _ => | |
| a | |
| )))) | |
| theorem contra (x : ((B ↑ B) ↑ (B ↑ B)) ↑ (A ↑ A)) : (A ↑ A) ↑ B := by | |
| apply deduct | |
| intro b | |
| apply double_neg_inv | |
| apply deduct | |
| intro na | |
| have nb := nandE2 na x | |
| have h : (A ↑ A) ↑ B := neg_explosive nb | |
| exact nandE2 b h | |
| theorem and_left (x : (A ↑ B) ↑ (A ↑ B)) : A := by | |
| apply double_neg_inv | |
| apply deduct | |
| intro na | |
| have h1 : (A ↑ A) ↑ (A ↑ B) := neg_explosive x | |
| have h2 : A ↑ B → A := fun ab => nandE2 ab h1 | |
| apply h2 | |
| apply nandI1 | |
| intro a | |
| have h3 : ((B ↑ B) ↑ (B ↑ B)) ↑ A := neg_explosive na | |
| have h4 : A → B ↑ B := fun a => nandE2 a h3 | |
| apply h4 | |
| exact a | |
| theorem and_right (x : (A ↑ B) ↑ (A ↑ B)) : B := by | |
| apply double_neg_inv | |
| apply deduct | |
| intro nb | |
| have h1 : (B ↑ B) ↑ (A ↑ B) := neg_explosive x | |
| have h2 : A ↑ B → B := fun ab => nandE2 ab h1 | |
| apply h2 | |
| apply nandI2 | |
| intro b | |
| have h3 : ((A ↑ A) ↑ (A ↑ A)) ↑ B := neg_explosive nb | |
| have h4 : B → A ↑ A := fun b => nandE2 b h3 | |
| apply h4 | |
| exact b |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment