The internet, we all know, some to very considerable cost, is a mixed blessing. But my experience with Logic Matters at least has been all positive. In particular, in 2012 when I was getting near to finalising the second edition of my Gödel book, it led to a very cheering episode. In late July that year, I posted:
In the immortal words of Douglas Adams, “I love deadlines. I like the whooshing sound they make as they fly by.” The second edition of my Gödel book was supposed to be off to CUP today for the proof-reading stage. But it will be two or three weeks yet. Still, the end is in sight …
I’ll be sending out the complete draft PDF to a few very kind people who have given me comments on the early chapters that I’ve posted here. But would you like to see the whole draft PDF when it is done in a couple of weeks (and maybe see your name in illuminated letters on the Acknowledgements page for the book)? Then here’s the deal …
Send me an email with the subject line “Proof reading Gödel” … from an academic email address, with a sentence or two about you, promising
- not to pass on the PDF,
- to do a very careful proof-reading for typos, cross-checking of references etc., of an assigned chunk of the book [about 30 pages] as quickly as you can, and definitely within three weeks of getting the PDF,
- to comment on any issues of readability etc. in that chunk.
Of course, comments on more would always be most welcome, even at this late stage! Since I’ll be producing the camera-ready copy for the book, I can make changes up to the wire (which will no doubt be at least a couple of months after I first send in the draft to CUP for their proof reader and production team to take a first look at).
Oh, how can you resist the offer!?
I also posted the same offer on the FOM list. The response to the two postings, as I reported a few days later, was terrific:
I’ve had a wonderful response to the invitation here to proof-read/comment on chunks of Gödel Mark II, enough to ensure that every chapter will be covered at least a couple of times. There was a (very) small bribe attached: but quite a few made friendly offers saying that they’d like to join in as they had enjoyed the first edition. Which is very nice to know! Corrections and suggestions from these new recruits assigned early chapters to review are already beginning to arrive, to add to those from some previous much-valued correspondents, as I finishing tinkering with the last chapters. Just terrific. It’s going to be a very busy few weeks ahead, but the book will end up a lot better for it.
The possibility of this kind of supportive exchange via the internet, and the availability of wonderful resources like mathoverflow.net of math.stackexchange.com, make trying to write a logic book in 2012 so very much more enjoyable (and a much less stressful experience) than even ten years ago. Many thanks to all my virtual logical colleagues out there!
And a couple of weeks later:
This last phase of writing has been a lot more enjoyable and less stressful than it might have been because of the input and warm encouragement I have had from over forty kind people in response to my invitation here and elsewhere to help proof-read chunks of the book. With most of the responses in, that has worked quite wonderfully well. Most chapters have now been looked at by three readers, with different readers bringing a different mix to the party. Some are particularly eagle-eyed at spotting typos, some very helpful about picking up sentences that don’t read well to non-native English speakers, some are good at finding nice ways of rephrasing to avoid possible misunderstanding, some have helpful suggestions about when yet-another-reference or yet-another-footnote would in fact be a good idea, some are stern about ‘that’ vs ‘which’, some have an enviably secure grasp of the True Difference Between a Colon and a Semi-colon, and so it goes. And everyone has evidently put a lot of care into their close-reading.
The proof-readers have been a very mixed bunch, lots of grad students of course, but also senior undergraduates, established professors, and a sprinkling of ‘amateurs’ who have done some logic in the past and are now out of academia. And (perhaps rather useful info for anyone thinking of emulating this exercise in crowd-sourcing the fine-tuning of a logic text), there seems to have been zero correlation between official status and the giving of particularly valuable comments.
I’m really grateful to everyone. All shall have prizes. Or at least, have their name in lights in the book.
And indeed they did have their names in lights. The result wasn’t perfect — see the corrections list! However, as you’ll also see from the list, the residual errors were almost all tiny and not likely to put a reader off their stride. So the experiment certainly worked. But, as I say, more than that, it was a rather cheering experience of friendly helpfulness from a lot of people.
Smorynski’s proof seems fine; but he doesn’t say anything about infinite looping or deliberately engineered failure or about anything being so trivial it doesn’t even count as a problem.
If you don’t want to explain the relevance of the joke, then of course you don’t have to. I also don’t understand why you are repeating ‘Exactly, WHY does the theorem could imply “the human mind not being mechanical” ???’ Or even asking me that question in the first place.
I am a bit puzzled with all the waffling around Gödel incompleteness theorems.
If you read Smoryński paper ( http://www.compstat2004.cuni.cz/~krajicek/smorynski.pdf ) which is 45 pages, in only 2 pages 827-828 he definitely deal with the whole crux of the matter, that is WHY there is incompleteness, furthermore if you take care to translate the diagonalization sentence:
ψ = φ(“ψ”)
To plain lambda calculus you get:
λφ.(φ ((λx.(φ (x x))) (λx.(φ (x x)))))
Which, whenever applied to ANY function of one argument, thus including the “unprovability” predicate λx.(¬∃y.proof(y,x)), turns it to a looping runaway because the reduction of the inner argument goes:
((λx.(φ (x x))) (λx.(φ (x x))))
((λx.(φ (x x))) (λx.(φ (x x))))
((λx.(φ (x x))) (λx.(φ (x x))))
…
IMHO, that a function deliberately engineered to fail does fail doesn’t count as a “problem” even less so as a “metaphysical problem”, so I wonder how you could write 350 pages about this as well as was done by the innumerable other authors who produced, likely, 100 of 1000 of pages about a 1-2 line lambda expression…
What am I missing?
Smoryński’s classic paper gives the headline news. Some readers, depending on their background, need more (some a lot more) than the headlines and also a lot of context. Hence different length treatments for different audiences (as indeed I’ve given myself).
What I don’t get is precisely what “more” is needed and how this gave way to such weird speculations about “the human mind not mechanical”, Penrose “quantum mind”, etc…
Do you know that the Templeton foundation funded Harvey Friedman (good for him…) and that he produced a report:
“A Divine Consistency Proof for Mathematics”. December 25, 2012, 70 pages
( https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/ )
With an appropriate disclaimer:
” The opinions expressed here are those of the author and do not necessarily reflect the views of the John Templeton Foundation.”
I have a really, really hard time to make the slightest connections between such questions and a purposely looping lambda reduction and how this can linger on for thousands and thousands of pages.
If people don’t get the point they will never, ever get it no matter how much is provided.
I don’t quite understand your lambda expression. Shouldn’t diagonalization be a fixed point expression rather than an infinite loop?
In any case, however brief or trivial the proof, the theorem is still the incompleteness theorem, and it’s the theorem that leads to the philosophical questions.
Like you, I have a hard time making connections between such questions and a looping lambda expression; instead the connections are between such questions and incompleteness.
The lambda expression comes from the proof of existence of the diagonalization sentence at the bottom of page 827:
Given φx, let θx φ(sub(x,x)) be the diagonalization of φ :
θx = λx.(φ(sub(x,x))) the “informal” θx is in fact a lambda binding
let m = “θx” and ψ = θm :
m = “λx.(φ(sub(x,x)))”
ψ = (λx.(φ(sub(x,x))))(m)
… we see that :
ψ = φ(sub(m,m)) applying ‘θ’ to ‘m’
ψ = φ(sub(“θx”,m)) since m = “θx”
‘sub’ as construed by Smorynski substitues its second argument for the ‘x’ :
ψ = φ(“θm”) applying ‘sub’
ψ = φ(“ψ”) by definition of ‘m’ and ‘ψ’
Now we expand the above definitions into lambda expressions, ‘sub(m,m)’ translates directly to application (m m) in lambda calculus, all function applications ‘f(x)’ translate to (f x)
ψ = (φ “(φ sub(m,m))”)
ψ = φ(“(φ (m m))”)
ψ = φ(“(φ ((λx.(φ (x,x))) (λx.(φ (x,x)))))”) by definition of ‘m’
ψ = λφ.(φ “(φ ((λx.(φ (x,x))) (λx.(φ (x,x)))))”) wrap in lambda abstraction
So, fortunately :-), the (m m) expression is inside quotes and we don’t need to try to reduce it but whenever the ‘φ’ caller need to unquote and access its argument it will find itself in double jeopardy, not only it finds its own code inside the quotes but if it tries to reduce (m m)… blam…
This is why I say that “it’s deliberately engineered to fail” and failure is no surprise.
It’s also an abuse of language to say that the Gödel sentence built with this is “true” but unprovable because it (supposedly) says of itself that it is unprovable, it is neither true nor false it just fails…
“it’s the theorem that leads to the philosophical questions.”
Huh?
Which philosophical questions?
Do you get this old joke:
– “Did you stop beating your wife?”
– True or false?
It still seems to me that a lambda-expression that corresponds to diagonalisation should be a fixed point, not an infinite loop. In any case, I also don’t see why you put so much emphasis on “deliberately engineered to fail”. Of course the diagionalisation argument is deliberately designed to reach its conclusion.
Re “Huh? Which philosophical questions?” — I meant questions such as the ones you mentioned about the human mind not being mechanical.
And I have now unapproved a few further comments, as things were starting to go round in circles in an unhelpful way.