[FOM] 174:Directly Honest 2nd Incompleteness

[Andrej Bauer]

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.

Indeed, the usual solution involves having some sort of quotation
operator, which is usually called "box" (think of drawing a box around
an expression instead of quoting it). In addition, there is an
operator that acts on types, also called Box, such that if e has type
A then (box e) has type (Box A). In this way the difference between
the meaning of an expression and its syntactic form is also visible at
the level of types. It turns out that the type operator Box acts like
a modal operator.

Many intricate issues have to be resolved, but they are not about
having "infinite descent of special quotes". The problems are of the
same kind that arise in modal logic. This is so because simply typed
lambda calculus with a box operator is essentially the theory of proof
terms of the intuitionistic propositional modal logic S4.

In summary, experience with programming languages suggests that there
_are_ formal systems that make assertions about their own syntax in a
completely honest way.

Many people have worked oin this area. In particular, if you are
interested in the essential ideas you can have a look at the work of
Frank Pfenning and coworkers, e.g., http://www.cs.cmu.edu/~fp/papers/jacm00.pdf

Andrej Bauer

Department of Mathematics and Physics
University of Ljubljana
http://andrej.com/