FOM: Feasibility and (in)determinateness of the standard numbers
sazonov at logic.botik.ru
Thu Apr 9 15:17:42 EDT 1998
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
(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
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/
More information about the FOM