From owner-qed Wed Nov  9 15:13:49 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id PAA27599 for qed-out; Wed, 9 Nov 1994 15:12:14 -0600
Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id PAA27594 for <qed@mcs.anl.gov>; Wed, 9 Nov 1994 15:12:08 -0600
Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id OAA03119; Wed, 9 Nov 1994 14:15:35 -0700
Message-Id: <199411092115.OAA03119@chelm.nmt.edu>
From: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Wed, 9 Nov 1994 14:15:35 -0700
In-Reply-To: Randall Holmes <holmes@catseye.idbsu.edu>
       "Re: Platonism" (Nov  9, 12:46pm)
reply_to: yodaiken@chelm.nmt.edu
X-Mailer: Mail User's Shell (7.2.5 10/14/92)
To: Randall Holmes <holmes@catseye.idbsu.edu>, qed@mcs.anl.gov,
        yodaiken@chelm.nmt.edu
Subject: Re: Platonism
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

On Nov 9, 12:46pm, Randall Holmes wrote:
 Subject: Re: Platonism
>(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.

Sure, but I do not see why this requires one to have faith  that
the syntactic objects (which clearly exist) represent similarly
"real" objects.

>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

There is no number less than 100! that  has property X:
    proof: for i=1 to 100! test X on i

If you can define exponentiation or factorial you are able to define
infeasible computations.