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/ ]