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 ; 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
"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 , 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.