I've finally managed to introduce the provability predicate and its properties without mentioning representability and recursiveness. The exercise is then to derive Löb's theorem and Gödel's incompleteness theorems. Unfortunately these deductions are not as simple as I thought they were. Probably too difficult for an introductory book.
I've also just made up this puzzle, which is not very difficult I think. ("Not very difficult" even in the ordinary sense of "not very difficult", not only in the David Chalmers sense.)
I'm still doing exercises for the logic book. This is rather unpleasant because I have to use Microsoft Word. Getting back to Word after using reasonable document formats (like LaTeX) and editors (like Alpha) for a while is a very frustrating experience.
At the moment, I'm trying to find nice and simple versions of Gödel's Theorems that still leave something formal to prove (like deducing Löb's Theorem from provability properties). This turns out to be difficult because I don't have the space to introduce the concepts of representability and recursiveness.
First, the puzzle:
In a certain country there are two Gods, called A and B. One of them (A or
B, you don't know which) only tells the truth, the other one only
falsehoods. One day you meet a God in this country and want to find out
whether it's A or B. You're only allowed to ask a single yes/no question.
Unfortunately, you don't understand the language of the Gods (even though
they understand yours). All you know is that their words for "yes" and
"no" are "qwer" and "poiu", but you don't know which of these means "yes",
and which "no". With what question will you be able to find out whether it's A
or B you're talking to?
I can't really say that I have made up this puzzle. Well, I have made it
up, but I took all the main ingredients from puzzles by George Boolos, who
himself owes them mainly to Raymond Smullyan and a computer scientist whose
name I forgot.
My logfiles show that an alarming number of people (namely more than 10
per day) look at my blogger and diffbot scripts. Don't do that. Don't use them. I
have almost finished programming much better versions of both that might be
worth trying. But since they have been in the "almost finished" state for
quite some time now, I thought I'd better add this note here.
Apologies in advance for another somewhat political entry.
Given the current state of everything, there is little hope that the easily available oil reserves won't be exploited until they are eshausted. There is also little hope that anything like the Kyoto protocol will prevent this from happening rather soon. For well-known reasons this is not good at all. So maybe those governments and institutions that care about the environment should try a different strategy: We could move forward with the exploitation of oil reserves, but instead of burning the oil and blowing all the carbon dioxide into the atmosphere, it could be bound in plastic.
On a more positive note, Prof. Beckermann found my speculations
convincing: The next edition of his logic book won't contain "incorrect"
quantifier rules any more.
I can't count how often I wished to live in that very close possible
world in which Al Gore won the presidency (very close in terms of Lewis'
similarity standards for counterfactuals, not in terms of overall
similarity, sadly).
What worries me most is how many US Americans seem to back the Bush
administration. I mean, when Clinton, like so many other people, had an
extramarital affair and lied about it, that was a big scandal and
caused an impeachment process. When Bush, quite unlike most people,
violates the UN charta by going to war against a country that doesn't
threaten the US at all, and keeps lying about his alleged knowledge of
Iraq's weapons of mass destruction and links with Al Quaeda, Americans just
seem to buy it. Then again, they are renaming French fries. There goes my princple of charity... For now,
I blame it all on the absence of a free press in the US, but I'm not sure
if that's a sufficient reason. I also tried to read blogs of the
war-mongers, but that didn't help much, it just left me very depressed for
the rest of the day. It's like shopping at Kottbusser Tor.
Oh well, I should better be blogging about quantifier rules in axiomatic
systems of predicate logic.
The fact that it turned out so difficult to explain my
question in sci.logic made me have a closer look at common axiomatic
systems of the kind I was critizising. This was a good idea, because I
found out that the systems used by Mendelson and Hodges are not of that
kind after all. The only such system is the one used by Kutschera and
Breitkopf, and as their logic book is German (and post-war), it is
not surprising that nobody understood my problem. It is however
interesting to compare the Kutschera/Breitkopf system with the systems of
Mendelson, Hodges and others:
Posting to newsgroups has some clear advantages over lonesome blogging.
Most notably, when I write something
incomprehensible in a newsgroup, somebody
will tell me that I do. Whereas here in this blog, nobody ever
complains even when I post absolutely unintelligible gibberish.
Maybe adding a comments section would help. But then I don't really have
a lot of readers. Maybe I should just add an "incomprehensible" button
under each entry, which when pressed would send me an email asking for
clarification.
Call for logicians: I have to convince Prof. Beckermann to drop an
incorrect rule of inference from the axiomatic system for predicate
logic used in his logic book. The incorrect rule is that from
A
B
one may derive
A
x B(t/x)
provided that t does not occur in A.