Re: Remarks on David's Mail of Oct. 25

Gerard Huet (Gerard.Huet@inria.fr)
Wed, 26 Oct 94 19:03:36 +0100

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 is the simple constatation that if we postulate
in our semantics the same closure conditions than in our syntax, then
the two notions correspond. If you believe it says a lot more than that
about absolute truths of mathematical statements you are under an illusion.
The only possible search for consistency is Gentzen's program of relative
consistency, which boils down to metamathematical investigation of the syntax
(a bunch of rewrite rules is terminating, a purely syntactic matter).
You just hope for the best concerning the metamathematics you use...

Concerning the statement "Mathematicians are concerned with truth", this
looks to me like a naive view of mathematics. At the Automath Symposium
two weeks ago, de Bruijn summed up 50 years of his own mathematics
practice into "Mathematics is just language after all".

Cheers!
Gerard