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

Torkel Franzen torkel at sm.luth.se
Thu Apr 9 06:09:00 EDT 1998

```  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

```