[FOM] Proof Assistants and Conjectures (reply to Chow)
pratt at cs.stanford.edu
Sun Jan 18 04:11:30 EST 2009
Brian Hart wrote:
>> Not that this necessarily makes the definition any easier, Goedel
>> had quite a struggle formulating his incompleteness theorems.
>> Vaughan Pratt
> Can you be more specific?
If you think Goedel numbers are easy, try coding them yourself. You'll
soon understand what Goedel was up against. Bear in mind that unlike
you, neither Goedel nor anyone else had ever seen a complex program
before. Goedel had to figure out not only the intricate coding details
of both his interpreter and the datastructures it was going to operate
on, but the entire computational paradigm for what he was doing, which
was at that time completely nonexistent. What could it even mean to
write an interpreter of programs in a logical language that is used
simultaneously to code the programs it is interpreting? The whole
concept is utterly preposterous for anyone who hasn't seen how these
ideas can come together in a way that actually makes sense. This was an
utterly mind-boggling accomplishment for its time.
More information about the FOM