FOM: infinitesimals and AST
sazonov at logic.botik.ru
Fri Nov 28 03:44:16 EST 1997
Vaughan Pratt wrote:
> Infeasible and infinite are surely orthogonal. \omega collects all
> numbers, feasible and infeasible.
But infeasible and infinite (as well as nonstandard numbers which
are "after" \omega) have the same roots in reality. The difference
you mean arises due to the specific formalization of infinity by ZFC.
Of course, if we need both ZFC (PA, etc.) and feasibility notion in a
unique theory, we will put feasible numbers as an initial part of
\omega. In this case of a unified theory it is interesting to extend
the idea of feasibility to cardinals, etc., as you suggest.
> My position would be that \omega is a feasible ordinal, while \omega + n
> and \omega.n are feasible ordinals iff n is a feasible number (finite
> ordinal). For cardinals, I would take beth_0 through beth_5 to be
> feasible but beth_6 not, via roughly Parikh's reasoning showing that
> 1024 is feasible but 2^1024 is not,
Note, that the main point and novelty of Parikh's work was not just
reasoning, but a *formalization*. It was the first construction of an
(almost consistent) theory where only for *much more big* number like
exponential *tower* of exponential height (of approx. 2^1000 stages)
it was postulated that it denotes infeasible number. In my
formalization just 2^1000 is (almost) consistently postulated as
infeasible. However, we must pay for this by a restriction on using
abbreviations (of terms) in the inferences of the underlying first
order (classical) logic. This payment is inevitable essentially by
the well-known result of V.Orevkov and R.Statman on non-elementary
complexity of cut-elimination (and, actually, of elimination of
abbreviations).Also note, that in my formalization even the feasible
number 1000 is *provably* after (what could be called) Vopenka's
Stephen G Sipson wrote:
> I have my doubts about whether AST provides a decent foundation for
> all of mathematics, as ZFC does.
What does it mean "all"? (ZFC had so strong influence on
mathematics!) Is it true that the future mathematics will
always have some unique formalization/foundation? Is not
believing in (which is of course not equivalent to trying to
find) a *unique* formalization a superfluous self-restriction?
More information about the FOM