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

[Torkel Franzen]

  Vladimir Sazonov says:

  >It is this unqualified "in principle" which is unclear. (In 
  >which "principle"?)

  The "principle" is rather like the "sake" in "for clarity's sake".
The phrase "in principle" means "disregarding all questions of
feasibility".

   >As I have replied to another participant of FOM, each concrete 
   >(i.e. feasible) formal proof in a concrete formal system is 
   >rather clear (fixed, concrete, unambiguous).

  Maybe so, but a "representation of my beliefs and intuitions by a formal
system" requires a formal system in my sense, not a feasible formal
system (a formal system with attention restricted to feasible
formal proofs). For example, the formal system must settle every
equation of the form s+t=r, not only "feasible equations".

  >Yes. But I actually said somewhat different: that we usually 
  >introduce a formal system to *formalize* some unclear intuition 
  >(limits, continuity, infinity, feasibility, etc.)

  Yes, but any formal system that I introduce to formalize my
intuition of "0,0+1,0+1+1, and so on" will itself be based on
that intuition.

  >But we hardly need the full power of PA to understand what is a 
  >formal language, a formal proof rule, how to use it, etc.

  Indeed not, but we do need the "full power" of "0,0+1,0+1+1, and so on".

---
Torkel Franzen