Created
November 15, 2025 11:17
-
-
Save MikuroXina/9937933860fea882e50105ae8ace07cd to your computer and use it in GitHub Desktop.
Hilbert-style 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
| -- Hilbert-style logic | |
| axiom Ax1 (A B : Prop) : A > (B > A) | |
| axiom Ax2 (A B C : Prop) : (A > (B > C)) > ((A > B) > (A > C)) | |
| axiom Ax3 (A B : Prop) : (¬A > ¬B) > (B > A) | |
| axiom Mp (x : A) (f : A > B) : B | |
| theorem Intro {A B : Prop} (y : B) : A > B := by | |
| have h1 : B > (A > B) := Ax1 B A | |
| Mp y h1 | |
| theorem Mp1 {A B C : Prop} (x : A > B) (y : A > (B > C)) : A > C := by | |
| have h1 : (A > (B > C)) > ((A > B) > (A > C)) := Ax2 A B C | |
| have h2 : (A > B) > (A > C) := Mp y h1 | |
| exact Mp x h2 | |
| theorem Mp2 {A B C : Prop} (x : A > B) (y : B > C) : A > C := by | |
| have h1 : (B > C) > (A > (B > C)) := Ax1 (B > C) A | |
| have h2 : A > (B > C) := Mp y h1 | |
| have h3 : (A > (B > C)) > ((A > B) > (A > C)) := Ax2 A B C | |
| have h4 : (A > B) > (A > C) := Mp h2 h3 | |
| exact Mp x h4 | |
| theorem Id {A : Prop} : A > A := by | |
| have h1 : (A > ((B > A) > A)) > ((A > (B > A)) > (A > A)) := Ax2 A (B > A) A | |
| have h2 : A > ((B > A) > A) := Ax1 A (B > A) | |
| have h3 : (A > (B > A)) > (A > A) := Mp h2 h1 | |
| have h4 : A > (B > A) := Ax1 A B | |
| exact Mp h4 h3 | |
| theorem DelIntro {A B : Prop} (x : A > (A > C)) : A > C := by | |
| have h1 : (A > (A > C)) > ((A > A) > (A > C)) := Ax2 A (B > A) C | |
| have h2 : (A > A) > (A > C) := Mp x h1 | |
| have h3 : A > A := Id | |
| exact Mp h3 h2 | |
| theorem Dist {A B C : Prop} (x : B > C) : (A > B) > (A > C) := by | |
| have h1 : (B > C) > (A > (B > C)) := Ax1 (B > C) A | |
| have h2 : A > (B > C) := Mp x h1 | |
| have h3 : (A > (B > C)) > ((A > B) > (A > C)) := Ax2 A B C | |
| exact Mp h2 h3 | |
| theorem Contradict {A B : Prop} : ((A > A) > B) > B := by | |
| have X := A > A | |
| have Y := X > B | |
| have h1 : X := Id | |
| have h2 : Y > (X > Y) := Ax1 P X | |
| have h3 : X > (Y > X) := Ax1 X P | |
| have h4 : Y > X := Mp h1 h3 | |
| have h5 : (Y > (X > B)) > ((Y > X) > (Y > B)) := Ax2 Y X B | |
| have h6 : Y > Y := Id | |
| have h7 : (Y > X) > (Y > B) := Mp h6 h5 | |
| exact Mp h4 h7 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment