[FOM] 174:Directly Honest 2nd Incompleteness
friedman at math.ohio-state.edu
Fri Jun 6 18:58:14 EDT 2003
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
>> [...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
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.
More information about the FOM