The mentioned size and density of Whitehead & Russel's Principia make the few dozen pages of Goedel's On Formally Undecidable Propositions of Principia Mathematica and Related Systems one of the greatest "i ain't reading all that/i'm happy for u tho/or sorry that happened" mathematical shitposts of all time.
It's easier if you start from something closer to Peano arithmetic or Boyer-Moore theory. I used to do a lot with constructive Boyer-Moore theory and their theorem prover. It starts with
(ZERO)
and numbers are
(ADD1 (ZERO))
(ADD1 (ADD1 (ZERO)))
etc. The prover really worked that way internally, as I found out when I input a theorem with numbers such as 65536 in it. I was working on proving some things about 16-bit machine arithmetic, and those big numbers pushed SRI International's DECSystem 2060 into thrashing.
Here's the prover building up basic number theory, one theorem at a time.[1]
This took about 45 minutes in 1981 and takes under a second now.
Constructive set theory without the usual set axioms is messy, though. The problem is equality. Informally, two sets are equal if they contain the same elements. But in a strict constructive representation, the representations have to be equal, and representations have order. So sets have to be stored sorted, which means much fiddly detail around maintaining a valid representation.
What we needed, but didn't have back then, was a concept of "objects". That is, two objects can be considered equal if they cannot be distinguished via their exported functions. I was groping around in that area back then, and had an ill-conceived idea of "forgetting", where, after you created an object and proved theorems about it, you "forgot" its private functions. Boyer and Moore didn't like that idea, and I didn't pursue it further.
That was a lovely read, thank you. I particularly enjoyed the analogy between 'a poorly-written computer program' (i.e. one with a lot of duplication due to inadequate abstraction), and the importance of using the appropriate mathematical machinery to reduce the complexity/length of a proof. It brings the the Curry–Howard isomorphism to mind: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
pvg ·10 hours ago
Show replies
Tainnor ·8 hours ago
Either I misunderstand the notation or there seems to be something missing there - the right hand side of that implication arrow is not a formula.
I would assume that what is meant is α⊂β→α∪(β−α)=β
jk4930 ·2 hours ago
https://us.metamath.org/mpeuni/mmset.html#trivia
https://us.metamath.org/mpeuni/2p2e4.html
Animats ·4 hours ago
Here's the prover building up basic number theory, one theorem at a time.[1] This took about 45 minutes in 1981 and takes under a second now.
Constructive set theory without the usual set axioms is messy, though. The problem is equality. Informally, two sets are equal if they contain the same elements. But in a strict constructive representation, the representations have to be equal, and representations have order. So sets have to be stored sorted, which means much fiddly detail around maintaining a valid representation.
What we needed, but didn't have back then, was a concept of "objects". That is, two objects can be considered equal if they cannot be distinguished via their exported functions. I was groping around in that area back then, and had an ill-conceived idea of "forgetting", where, after you created an object and proved theorems about it, you "forgot" its private functions. Boyer and Moore didn't like that idea, and I didn't pursue it further.
Fun times.
[1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
Show replies
awanderingmind ·9 hours ago