FOM: infinitesimals and AST

[Vladimir Sazonov]

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


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? 


Vladimir Sazonov