From owner-qed Wed Oct 26 13:04:12 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA07554 for qed-out; Wed, 26 Oct 1994 13:03:51 -0500 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id NAA07543 for ; Wed, 26 Oct 1994 13:03:43 -0500 Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.6.9/8.6.9) with SMTP id TAA26560; Wed, 26 Oct 1994 19:03:37 +0100 Received: by pauillac.inria.fr; Wed, 26 Oct 94 19:03:36 +0100 Date: Wed, 26 Oct 94 19:03:36 +0100 From: Gerard Huet Message-Id: <9410261803.AA11498@pauillac.inria.fr> To: dahn@mathematik.hu-berlin.de, dam@ai.mit.edu Subject: Re: Remarks on David's Mail of Oct. 25 Cc: qed@mcs.anl.gov Sender: owner-qed@mcs.anl.gov Precedence: bulk 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