From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5860 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Tue, 25 May 2010 20:08:01 -0700 Message-ID: References: Reply-To: Toby Bartels NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: dough.gmane.org 1274968105 32105 80.91.229.12 (27 May 2010 13:48:25 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 27 May 2010 13:48:25 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Thu May 27 15:48:23 2010 connect(): No such file or directory Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OHdRc-0002IE-AU for gsmc-categories@m.gmane.org; Thu, 27 May 2010 15:48:20 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OHd8a-0005w3-KE for categories-list@mta.ca; Thu, 27 May 2010 10:28:40 -0300 Content-Disposition: inline In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5860 Archived-At: Vaughan Pratt wrote in part: >Moreover most of us would agree that the proposition "the prime factors >of M = 7^7^7^7 + 5^5^5^5 + 1 (7#4 + 5#4 + 1 where m#n denotes an >exponential stack of n m's) are all greater than 2 billion and there are >more than a thousand distinct such" not only makes perfect sense but is >either true or false. However fewer might be willing to join me in >insisting that it is certainly true. Since I know very little about these issues, I'm not ready to accept your claim that it is true. (I know that you sketched a way for me to verify it by performing some calculations on my laptop, but it would take a while for me to figure out what to program and then to convince myself that the output meant what you say.) However, I am happy to agree that the statement is true or false. >Those who question excluded middle for this proposition may have >received different wisdom about N than the rest of us, though if I'm >right then there's a constructive proof of the proposition that can be >checked on any laptop in under an hour, which should then oblige the >intuitionistic objectors to stand down. Anyone who doubts excluded middle for *this* proposition is not merely a constructivist, or even an intuitionist. Excluded middle for this proposition is provable in Heyting arithmetic. While a straightforward calculation of the factors of M would not fit into the physical universe, it is still finite. Those who doubt excluded middle (or meaningfulness) for this proposition go beyond intuitionism; they have been called "ultra-intuitionists", although the preferred term these days is "ultra-finitists". As someone who is quite comfortable with constructivism, I still find ultra-finitism a very strange way to think. Ultra-finitists definitely have a different recieved wisdom about N from what the rest of us have received. Ob categories: Does anybody know any work on ultra-finitism from the perspective of categorial logic? (somewhat in the way that topos theory can provide a perspective on constructivism). I doubt that any exists, but I would it would be nice if it did. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]