[FOM] 174:Directly Honest 2nd Incompleteness

[Harvey Friedman]

Reply to Bauer 12:14PM 6/6/03.

>Harvey Friedman <friedman at math.ohio-state.edu> writes:
>>
>>  OBJECTION TO SECOND THEOREM. It appears that no formal system can make
>>  assertions, in a completely honest and direct way, about its own
>>  syntax.
>>
>>  [...material deleted....]
>>
>>  The only way around this would seem to be to construct a system that
>>  handles the limit of this procedure properly. But this is very
>>  delicate. One would probably have to add an operator corresponding to
>>  "placing quote signs", with appropriate axioms involving this
>>  operator. But then, the symbol for the operator itself creates
>>  additional syntactic structure, which itself must be discussed.
>
>People who work in the theory of programming languages have thought
>about these points and worked them out in detail. Their motivation is
>manipulation of source code of programs by programs themselves.

The context of my posting was possible reservations about the 
significance of the 2nd incompleteness theorem. So one strives to 
adhere to an excruciatingly high standard of naturalness of any 
proposed formalism as a model of mathematical practice.

ZFCU, and fragments, with abbreviation power, does meet this standard 
(and can be easily modified to meet higher and higher relevant 
standards). It is well known that abbreviation power does not affect 
consistency statements. So one can reasonably use ZFCU and various 
fragments in connection with the 2nd incompleteness theorem.

In any discussion of the (un)provability of consistency, obviously we 
must model the mathematician's consideration of consistency. Hence 
the clear motivation behind adding constants for symbols of ZFCU to 
create ZFCU'.

Beyond that, more and more powerful quoting mechanisms may not hold 
up very well under the criticism that one is talking about ad hoc 
formal systems based on ad hoc formal devices, rather than naturally 
obvious models of mathematical practice.

The key point I was making in my posting #174 of 1:39PM 6/3/03, was 
that the 2nd incompleteness theorem is, once again, so robustly 
important, that it is immune to such considerations. For even if one 
adds the constants for symbols of ZFCU to create ZFCU', one cannot 
even prove the consistency of ZFCU in ZFCU'. There is no need to even 
consider the consistency of ZFCU' at all.

As far as programming languages are concerned, I am aware that simple 
ad hoc devices - natural from the point of view of programming 
languages - are  known that ensure that a machine will be able to 
unambiguously disentangle nested quotes.

However, I still doubt if there is such a setup that would meet the 
test of corresponding directly and honestly to any kind of existing 
mathematical practice. ZFCU and ZFCU' do meet this test (at least 
sufficiently for the defense of the 2nd incompleteness theorem).

I may well be seriously wrong. E.g., I haven't tried to prove any 
relevant theorem about this, nor have I spent any quality time trying 
to construct formal systems that refute my impossibility assertion.

So I stand to learn something. It would be helpful if somebody thinks 
that this can be done in close connection with natural mathematical 
practice, to see them outline this on the FOM.

That is a reasonable division of labor, as I am right now too busy to 
think deeply about this matter myself. I was satisfied to see that 
this issue does NOT have to be addressed in order to fully defend the 
2nd incompleteness theorem from such attacks - my main point.

Harvey Friedman