From owner-qed Wed Nov 9 13:48:32 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA26261 for qed-out; Wed, 9 Nov 1994 13:45:23 -0600 Received: from catseye.idbsu.edu (catseye.idbsu.edu [132.178.200.125]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id NAA26254 for ; Wed, 9 Nov 1994 13:45:13 -0600 Message-Id: <199411091945.NAA26254@antares.mcs.anl.gov> Received: by catseye.idbsu.edu (1.38.193.4/16.2) id AA15787; Wed, 9 Nov 1994 12:46:01 -0700 Date: Wed, 9 Nov 1994 12:46:01 -0700 From: Randall Holmes To: holmes@catseye.idbsu.edu, qed@mcs.anl.gov, yodaiken@chelm.nmt.edu Subject: Re: Platonism Sender: owner-qed@mcs.anl.gov Precedence: bulk (responding to yodaiken's question) It depends on what level one is working. Suppose that I prove mathematically that there is a proof of theorem X, even prove it constructively. The computer code generated by following the procedure outlined in my proof may be so large as not to be implementable. I'm doing metamathematics, but it is not implementable directly. Of course, this can be avoided by making the theory in which metamathematical reasoning is to be carried out sufficiently weak; but I don't think that PRA is weak enough to forbid metamathematical results of this kind (comments on this question are invited?) One's metamathematics needs to be not only constructive but "feasible" in some sense to make the situation I describe above impossible. Does this clarify my point? --Randall