Hacker Remix

One Plus One Equals Two (2006)

94 points by lemper 19 hours ago | 49 comments

pvg 13 hours ago

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.

oglop 12 hours ago

Gödel had great respect for their work and was considered one of only a few people at the time to have read and understood the work. He wrote an entire paper later in life explaining he wouldn’t have come to his result without Principia because it showed him a base case to work from. Him and Russell would continue to meet and discuss logic well into the 50’s.

libraryofbabel 2 hours ago

First, you’re arguing with someone making a joke, and second, yes, he understood the axioms very well and was able to use the system to prove his incompleteness theorems, but, citation needed on whether he actually read the full three volumes? Russell himself said that “I used to know of only six people who had read the later parts of the book. Three of these were Poles... The other three were Texans [Gödel was neither Polish, nor Texan]”

Tainnor 11 hours ago

> theorems like ∗22.92: α⊂β→α∪(β−α)

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 α⊂β→α∪(β−α)=β

Animats 7 hours ago

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.

Fun times.

[1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

anthk 5 hours ago

The Computational Beauty of Nature has a tiny Lisp implementing integers and aritmethics by hand too, by consing t's.

awanderingmind 13 hours ago

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...