From owner-qed Mon Nov 7 11:04:11 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id LAA18801 for qed-out; Mon, 7 Nov 1994 11:00:22 -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 LAA18786 for ; Mon, 7 Nov 1994 11:00:01 -0600 Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA16012; Mon, 7 Nov 94 11:59:54 EST From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA01078; Mon, 7 Nov 94 11:59:52 EST Date: Mon, 7 Nov 94 11:59:52 EST Message-Id: <9411071659.AA01078@spock> To: podnieks@mii.lu.lv Cc: qed@mcs.anl.gov In-Reply-To: Karlis Podnieks's message of Fri, 4 Nov 1994 12:11:36 +0200 (EET) Subject: Semantics Sender: owner-qed@mcs.anl.gov Precedence: bulk Well that was quite a chapter. I didn't read it in entirety but you have clearly spent a lot of time thinking about these issues. The parts I did read seemed to focus on the issue of the actual existence of mathematical objects. To me, this "actual" existence is irrelevent. To me, the issue is simply what we talk about when we do mathematics. If we talk about numbers, and sets and so on, then we are acting as Platonists. If we talk about formulas (which are about numbers or sets) then we are acting as formalists. Theorem proving systems can either manipulate formulas about numbers (anologous to sentences in conversations between Platonists) or they can manipultate formulas about formulas which are about numbers (analogous to sentences in conversations between formalists). Pragmatically, the Platonic style of reasoning has advantages for both humans and machines. Although I believe that Platonism is just a style of reasoning, and all reasoning is based ultimately on symbol manipulation, I also believe that the axioms of ZFC have a distinguished status in mathematics which is not simply a result of arbitrary social convention. The structure of ZFC is derived from intuitions about "logical neccessity". Intuitions about the real numbers seem different, more empirical, than intuitions about domain independent logic. The axiom of choice is equivalent to the correctness of Skolemization, a purely logical principle. I believe that our intuitions about logical neccessity reflect an innate logical system, a "mentalese". To me, the "clear validity" of Skolemization is evidence that the axiom of choice is hard-coded into human mentalese. Replacing choice by AD, and giving up Skolemization, would make my head hurt (but perhaps other heads have learned to work other ways). To say that accepting AD would make my head hurt seems different form saying that AD is false in some deep metaphysical sense. I just think AD violates the axiom system hard wired into my brain. I choose to accept the mentalese engine in my brain and "use the force" as it was so elequently put in a recent message. David