From owner-qed Mon Nov  7 11:52:50 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id LAA19715 for qed-out; Mon, 7 Nov 1994 11:52:30 -0600
Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id LAA19710 for <qed@mcs.anl.gov>; Mon, 7 Nov 1994 11:52:18 -0600
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA19440; Mon, 7 Nov 94 12:51:27 EST
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI-4.10) id AA01103; Mon, 7 Nov 94 12:51:26 EST
Date: Mon, 7 Nov 94 12:51:26 EST
Message-Id: <9411071751.AA01103@spock>
To: Gerard.Huet@inria.fr
Cc: dahn@mathematik.hu-berlin.de, qed@mcs.anl.gov
In-Reply-To: Gerard Huet's message of Wed, 26 Oct 94 19:03:36 +0100 <9410261803.AA11498@pauillac.inria.fr>
Subject:  Remarks on David's Mail of Oct. 25
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

For some reason I seem to have missed a message that came by
a couple weeks ago.  (I get way too much mail, things seem to get
lost in the noise).

>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