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

[Vladimir Sazonov]

Torkel Franzen wrote:
>
>   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".

(What about e.g. "disregarding SOME questions of feasibility" 
instead of "all"?)

It seems you have agreed that in the present context we should 
not disregard feasibility.  Otherwise, what are we talking about? 

>   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".

(Only "metamathematicians" consider "infeasible" formal systems 
by using feasible proofs that, e.g., there exists an infeasibly 
long proof, etc.) 

All proofs written by mathematicians are actually feasible.  
These proofs are not always completely formalized.  I.e. we not 
always care of which precisely formal rules we are using. But 
there is no doubt that any mathematical "correct" proof may be 
feasibly represented in an appropriate formal system. Usually it 
is ZFC + some formal rules for abbreviations.  (By the way, the 
main point of my formalization of feasibility concept is a very 
careful work with abbreviations.)

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

Sure! But this is not a vicious circle. Note, that 
non-formalized intuition alone is too weak. We use crude 
intuition on feasibility to describe, say, a formal system FA 
devoted to formalization of "feasible" intuition of 
"0,0+1,0+1+1, and so on". Now, by "feasible" treatment of the 
formal rules of FA we can deduce in FA some simple theorems on 
feasibility concept formalized this way.  The intuition alone 
without support of formal (mechanically used) proof rules may be 
insufficient to get these theorems. Of course, by getting more 
experience with such a formal system our intuition will somewhat 
change and become much stronger. Then we will be able to get 
these and some other theorems by some "insight" so that an 
illusion may arise that it is not due to a formal system. I 
would say, it is *both* due to intuition *and* formal system 
which may only *co-exist* in mathematics and have an essential 
influence one on another. 

>   >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".

(I should repeat that I do not know what is "full power" of 
"0,0+1,0+1+1, and so on", unlike "full power" of PA which is 
determined by the well known axioms.)

We need not "full" but only "feasible" power! For example, we 
even need not know that substitution of a term for all 
occurrences of a variable is always defined, i.e. feasible. 
(This and arithmetical multiplication are only partial recursive 
operations from the point of view of feasibility.) But when we 
have a "ready" result of a substitution we may use it in a 
proof. It is the real practice of doing mathematics (and also 
programming). 


Vladimir Sazonov
--
Program Systems Institute,      | Tel. +7-08535-98945 (Inst.),
Russian Acad. of Sci.           | Fax. +7-08535-20566
Pereslavl-Zalessky,             | e-mail: sazonov at logic.botik.ru
152140, RUSSIA                  | http://www.botik.ru/~logic/SAZONOV/