From owner-qed Wed Oct 26 14:39:43 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id OAA09197 for qed-out; Wed, 26 Oct 1994 14:39:13 -0500 Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id OAA09187 for ; Wed, 26 Oct 1994 14:39:00 -0500 Received: by SAIL.Stanford.EDU (5.65/25-SAIL-eef) id AA12246; Wed, 26 Oct 1994 12:38:20 -0700 Date: Wed, 26 Oct 1994 12:38:20 -0700 From: John McCarthy Message-Id: <9410261938.AA12246@SAIL.Stanford.EDU> To: Gerard.Huet@inria.fr Cc: dahn@mathematik.hu-berlin.de, dam@ai.mit.edu, 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 Reply-To: jmc@cs.stanford.edu Sender: owner-qed@mcs.anl.gov Precedence: bulk It is naive to regard one side in the long standing controversy over whether mathematics is concerned with truth as naive. To take de Bruijn as authoritative in this matter is to call Goedel naive. I am of Goedel's opinion in this matter. However, there is more to it for us than a philosophical controversy in the foundations of mathematics. If QED is to succeed, then informal mathematical arguments have to be translatable into QED. My opinion is that many of these arguments when formalized in logic will actually concern the relation of formulas to models, i.e. wil involve truth as a concept. I think philosophers know this but can call this informal use of the word truth just a manner of speaking, translatable (in principle) back into arguments about formulas. However, if one decides in advance to work only in terms of formulas, one will be working with one hand behind one's back. The translations will be much longer than the original arguments that we might have allowed but don't for reasons of philosophical purity.