FOM: Feasibility and (in)determinateness of the standard numbers

[Torkel Franzen]

  Vladimir Sazonov says:

  >The stronger are axioms the more we will have examples of concrete Turing 
  >machines which could be (feasibly) proved to halt and therefore 
  >the more we will have corresponding "provably recursive/existing 
  >natural numbers". (Examples of such comparatively small numbers 
  >provably existing in PRA or even in much weaker systems of 
  >arithmetic:  2^1000, 2^{2^1000}), etc.)
  >Therefore the "length" of the "standard model" seems to be rather
  >indeterminate.

  Your argument until the last sentence is clearly correct, but that last
sentence is a non sequitur. How do you arrive at the conclusion "therefore..."?

  Of course I suspect that I know how you arrived at it: by identifying
"the standard model [according to a theory T]" with "the numbers that
can feasibly be proved in T to have notations in the language of T" (or
some closely related concept). Such a terminology is non-standard, and
can only serve to confuse. Much better to explain your views by saying
that you reject the concept of the standard model.

  Such formulations as "the length of the standard model is indeterminate"
are of course more striking and newsworthy. Brouwer consistently formulated
his criticism of classical mathematics in similarly dramatic terms.

  >Nevertheless, we have an *informal model* of 
  >feasible numbers which is therefore very different from the 
  >ordinary first order models. This is the place where the basic 
  >intuition and experience does not work or is insufficient and 
  >should be somewhat corrected or extended.

  This is clear, I think, already because "feasible" is a vague
concept, and ordinary mathematical induction is invalid for vague
concepts.

  >However, what about the ordinary intention of mathematicians to 
  >embed "everything" in a unique mathematical "universe" like that 
  >for ZFC?  I only say that feasibility concept taken 
  >"foundationally" is not embeddable straightforwardly in the 
  >ordinary mathematics as we know it.  This seems to touch on some 
  >illusions we have.

  I'm sure you're right about feasibility not being straightforwardly
embeddable in ordinary mathematics. But the illusion you invoked
before was an illusion involving the natural numbers as classically
(non-feasibly) understood. It's the claim that our classical
understanding of and use of arithmetic is somehow based on an illusion
that I reject.

  >If you, Torkel, can fully realize this 
  >concept without changing anything in your views, I am very glad.  
  >However, I have some doubts on this especially in connection 
  >with the very unusual intended "model" for FA.

  Undoubtedly it's difficult for most of us to absorb and take
seriously concepts that we didn't absorb when we were young. However,
I think many people will be prepared to study feasibility if they see
it as potentially useful or enlightening. Even Yesenin-Volpin's stuff,
with its tactics of attention and whatnot, is not beyond the realm of
the potentially mathematically meaningful. But we lazy bums who are
not captured by the intrinsic interest of such developments need some
incentive to study them.

  >Which rule then generates 2^1000 (as a set of binary strings)? 
  >Of course, enumerating all these strings in the lexicographical 
  >order is irrelevant as an infeasible and highly non-realistic 
  >process.

  My comment was ambiguous (in the ordinary way): by "generated by a rule"
I didn't mean "actually generated" but "potentially generated". 2^1000 is
generated by the rule(s)

     s0 is in M, where s0 is the sequence of zeroes of length 1000
     if s is in M then s' is in M, where s' results from s by
                   changing a 0 to 1

  There are no such rules that generate 2^N.

---
Torkel Franzen