[FOM] Re: Formal nature of mathematics

[Dmytro Taranovsky]

Vladimir Sazonov wrote,
> For example, I ASSERT, not as a mere speculation, that there is a
> simple, but rather unusual FORMAL system of axioms and proof
> rules in which a (semi)set of natural numbers 0,1,2,... < 1000
> is FORMALLY definable which is PROVABLY closed under successor
> and is also upper bounded by the number 1000. Quite intuitive
> informal examples of such semisets from our real world are well
> known (e.g. presented by P. Vopenka).

I think Sazonov meant 2^1000 instead of 1000, and even that is
insufficient if we allow binary representations and closure under
feasible addition.  Something like 2^2^64 would be needed for
contemporary computer science, and even more for an accurate
representation of physical reality.

However, we can restrict natural numbers to those less than 2^1024 if we
also allow, as a different type, arbitrary sets of those numbers (or
alternatively, binary sequences of integral length).  

Anyway, the system would be cleaner if we do not postulate closure under
successor.  We do not know that no future storage device will hold
2^1024 symbols, and it is logically true that there is the largest
feasible natural number.  

Another approach is that of finite quasi-models, as I described in
http://www.cs.nyu.edu/pipermail/fom/2005-November/009318.html
In a finite quasi-model of, say, Peano Arithmetic, unfeasible statements
can be meaningless, which prevents it from being contradictory.  

Sincerely,
Dmytro Taranovsky