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