>From Gerard Huet:
Well, I would just like to dispute (lightly) the statement by David
that "It is possible (easy) to define the semantics formally and
formally prove relationships between syntactic operations and semantic
meaning."
Godel's completeness theorem ...
It seems to me that the relevant theorem is Tarki's theorem on the
non-definability of truth. For arithmetic this can be summarized as
the statement that truth, as a property of arithmetic formulas, is
hyper-arithmetic (can not be expressed as a formula of number theory).
In fact, no sufficiently powerful system can define its own truth
predicate. But just assume a few inaccessible cardinals and
set-theoretic truth (in the models provided by those cardinals)
becomes easy to define.
The above paragraph is probably meaningless to those unwilling to
think Platonically about the truth of arithmetic formulas. But if one
just accepts the Platonic style of reasoning it all becomes clear (use
the force).
Ultimately I agree with de Bruijn that mathematics is just language
(plus a brain for manipulating mentalese). But language can be
Platonic or formal. For me, Platonic language is easier to think
with.
David