[FOM] A Framework for the Study of Feasible and Utterable Numbers

[Andrew Boucher]

There has been an interesting discussion on feasible and utterable  
numbers, by Sazonov, Mannucci, and Podnieks, among others.

On  18 Aug 2006, at 6:09 PM, Mirco Mannucci wrote:
>
> 2) an approach in the Parikh-Sazonov spirit, i.e. using a  
> "feasibility predicate" F() on
> top of a standard arithmetic theory (such as Q).

Here is an alternative framework.  First, do not use Q as a base  
theory!!  Q, by assuming the totality of the successor function,  
implicitly assumes that the natural numbers - all of them - are  
there, contrary to an ultrafinitist viewpoint. Instead, use as base  
the system (call it F) which is second-order PA minus the Successor  
Axiom.  This system has as models the standard model as well as all  
initial segments, so it is agnostic whether the natural numbers go on  
and on ad infinitum, or whether there exists a maximum number.   It  
also has a nice property for a base theory, in that it can prove its  
own consistency.   Note that Q and F are incomparable in strength:   
on the one hand, Q does not have induction while F assumes full  
induction; on the other, Q makes ontological assumptions  
(infinitely!) stronger than F.  So neither is weaker (or stronger)  
than the other.

F behaves normally in many ways.  Addition, multiplication, and  
exponential relationships can be defined, and their normal properties  
can be proved, except for totality.  [1] As a rule of thumb, one  
reasons in F as one would in full PA, except that, when given a  
natural number n, one can only infer that natural numbers less than n  
exist, and not that any greater exist.

Def.  A sequence is a relationship R (an upper-case or second-order  
entity) with domain {x : x <= n}.  In this case set top(R) = n.

Sequences behave normally in F, except that the concatenation of two  
sequences R and S exists if and only if top(R) + top(S) + 1 exists  
(we are beginning the natural number series with 0).

For exposition purposes assume now that 1 exists and that a set of  
operations, along with parentheses, OPS = {+,*,^,(,)}, disjoint from  
the natural numbers, exists.  Let D = {0,1}, the set of digits.

Def.  A numeral is a sequence R such that:
1/  image(R) = D
2/  with top(R) = n, either n = 0 or not Rn,0.
As is standard write a numeral in "reverse" order, where the value of  
top(R) is written first, and the value of 0 is written last.  Then 0  
is a numeral, 10010 is a numeral, but 010010 is not a numeral  
(because of the leading 0).

Def.  An utterable natural number (written UNN) is a sequence R such  
that either:
1/  R is a numeral, or
2/  there exist utterable natural numbers S and T such that R is the  
concatenation of
a/ "(",
b/ S,
c/ an element of OPS,
d/ T, and
e/ ")".
So e.g. ((100 ^ 101) + 101) is a UNN, provided of course that this  
sequence exists, i.e. if fourteen exists.  Remark that the definition  
is "downwardly" recursive and so it can be expressed in F.  That is,  
it expresses conditions for a sequence, which must exist, to be a  
UNN.  It does not make any ontological assertions (as one sometimes  
finds in definitions in logic books).  In particular, it does not  
assert the existence of a larger thing (the UNN R), given the  
existence of smaller ones (the UNNs S and T).  This, of course,  
cannot be asserted in general in F.  In fact, the existence of R  
follows if and only if top(S) + top(T) + 4 exists.

It is possible to define formulas EQ_NN and EQ_NUM such that:
1/ EQ_NN(R,n) expresses intuitively that R is a UNN which represents  
the natural number n, and
2/ EQ_NUM(R,S) expresses intuitively that R is a UNN which represents  
the numeral S.
So e.g. if ten exists, then ((10 ^ 10) + 1) represents the number  
five or the numeral 101.

Note of course that one cannot assume in general, for any UNN R, that  
there exists an n or an S such that EQ_NN(R,n) or EQ_NUM(R,S).   
However, if there exists an n such that EQ_NN(R,n), then there exists  
an S such that EQ_NUM(R,S), since the length of a numeral is always  
less than or equal to the number which it represents.  So three  
classes of UNN spring to mind:
1/  R such that there exists n with EQ_NNN(R,n)
2/  R such that there exists S with EQ_NUM(R,S) but not such there  
exists n with EQ_NN(R,n)
3/  the rest - the utterable numbers which are not equivalent to  
numerals.  Under suitable conditions a tower of powers of 10 (i.e.  
two) would fall into this category.

UNNs of categories 1/ and 2/  have nice features.  One is easily able  
to define an equality formula which is reflexive, symmetric, and  
transitive.  It would seem (though I have not rigorously checked for  
2/) that standard properties, such as the Euclidean Algorithm and the  
existence and uniqueness of Prime Factorization, apply.

UNNs of category 3/ are a different matter.  It would seem there is a  
problem, as Sazanov has noted in regards to his framework, of  
defining a formula for equality which is transitive.  The most  
natural manner of defining equality would be to say that two UNNs are  
equal if they can be transformed from one to the other using various  
transformation steps, such as using commutativity of addition, or  
distribution, or certain power rules.  The problem is that R might be  
transformed to S in n steps, and S to T in m steps, but n + m might  
not exist, so there may be no permissible transformation from R to  
T.  So:

QUESTION 1.  Does there exist a formula EQUAL such that F proves that  
EQUAL(R,S) precisely when R and S are UNNs representing, intuitively,  
"equal numbers"?

This leads to another, associated, question:

QUESTION 2.  Does there exist a formula LESS_THAN such that F proves  
that LESS_THAN(R,S) precisely when R and S are UNNs with R  
representing, intuitively, "a number less than" that represented by S?

One possible way forward, should the answer to Question 1 be in the  
negative, might be to define the natural formula for equality and  
only look at UNNs for which transitivity applies.

[1]  Details may be found in "Arithmetic Without the Successor  
Axiom", located at http://www.andrewboucher.com/papers/arith-succ.pdf.