[FOM] Self-referentiality and Godel sentences

[Harvey Friedman]

Reply to Avron /3/03 12:10PM.

It seems like a good time to revisit these old postings

http://www.cs.nyu.edu/pipermail/fom/2003-June/006743.html
http://www.cs.nyu.edu/pipermail/fom/2003-June/006766.html

I discussed the project of developing an extension of ZFCU (I could also
have talked about ZFC or PA instead) that directly supports reference to its
own syntax. 

The reason I brought this up then is in connection with the statement of
Godel's 2nd incompleteness theorem, which concerns the consistency statement
(which we know has very strong uniqueness properties, so "the" is
justified). 

I raised the idea that this cannot be properly done. Bauer objected and said
that this sort of thing has been done in the computer science community.

But my MAJOR point was that even if this cannot be properly done, it does
NOT affect the significance of the Godel 2nd theorem. This is because it is
obvious that one can construct an extension ZFCU' of ZFCU which directly
supports reference to the syntax of ZFCU. And then one proves, according to
Godel, that ZFCU' doesn't even prove the consistency of ZFCU - now stated
directly and honestly - assuming ZFC is consistent.

So for this reason, I did not feel compelled to really getting into this
issue of directly honest reference and self reference.

Now just because we might succeed in supporting directly honest reference by
a system to its own syntax - something I am not sure can be done to meet
high standards - that doesn't automatically mean that we have supported
directly honest self referential sentences within the system. One can again
do a self reference Lemma, this time a more honest one armed with the
directly honest reference.

So my question is: is there a natural way to extend ZFCU so that it directly
and honestly supports reference to its own syntax, through a system of
necessarily nested quote signs, and the like? And how does it affect the
Avron discussion?

Harvey Friedman