[FOM] Buckner 1,2

[Harvey Friedman]

Reply to Buckner 5/13/03  8:10PM.

>Harvey,
>
>Thanks for the note.  I understand perfectly what you're saying, but you
>don't understand perfectly what I'm saying.
>
>Of course: if we need to define the term "natural number", we are going to
>to run into the sort of problem I am complaining about.

In all of the formal systems we are talking about, natural numbers 
are taken as primitive. Let us organize where we are.

We have been talking about foundations of mathematics under various 
restrictions
of what is allowed.

In Buckner 1, the restriction is that no use of sets be made. Under 
Buckner 1, PA and PA' are accepted. There is an interpretation of 
ACA0 in PA' and WKL0 in PA. In fact, of WKL in PA, where WKL is WKL0 
with full induction in the language. These systems ACA0 and WKL are 
sufficient to reasonably directly conduct a significant amount of 
mathematics including real analysis.

In Buckner 2, the restriction is that no use of sets be made, and in 
addition, no use of induction be made. However, the concept of 
natural number is taken as primitive.

In Buckner 3, the restriction is that no use of sets be made, no use 
of induction be made, AND EVEN no concept of natural number is used.

I now want to deal with Buckner 2 and postpone any discussion of 
Buckner 3 until later.

FIRST ORDER COUNT ARITHMETIC WITHOUT INDUCTION.

We will avoid induction, but instead directly support "the number of 
x such that A(x) is y". We call this

count arithmetic

and it leads to a first order formal system COA.

This is not a silly matter for f.o.m. for the following reason. If we 
take the standard approach, and use induction as the driving 
principle of arithmetic, then we still have to use (something like) 
addition and multiplication.

In this approach, we do NOT have the use anything like addition and 
multiplication. Instead, we can use only <.

DIGRESSION. Of course, we are talking about FIRST ORDER logic 
versions of arithmetic. In second order logic versions, one does not 
need addition and multiplication with the induction approach, either.

However, a second order system intended to be used for axiomatic 
purposes (supporting actual proofs), must be ultimately cast into a 
first order logic system. I.e., there are comprehension axioms in the 
background.

So relevant second order versions supporting proofs are really rather 
complicated first order versions. The first order versions we discuss 
here are more basic and fundamental and appropriate to the 
minimalistic discussion being engaged in, than second order versions 
- i.e., first order versions that arise from a formally second order 
version.

In fact, the challenge in this thread is to avoid at all costs, the 
use of predicates-as-objects, which (seems to) precludes any second 
order approach.

Incidentally, there is much fundamental confusion about first 
order/second order axiomatizations, generally, in f.o.m. That can be 
another thread on the FOM list, if need be.

There appears to be a minority of philosophers of mathematics and 
philosophical logicians who properly understand the issues and 
nonissues regarding first order/second order axiomatizations for 
f.o.m.

However, there are even far far fewer people who properly understand 
this, AND who are able to put together any convincing interchange 
about it in order to get others who don't properly understand this to 
"get it".  In fact, there is no proof that a single such person 
exists. I have never witnessed the conversion of anyone on such 
matters. END OF DIGRESSION.

The vocabularly of COA (count arithmetic) is as follows.

i. not, and, or, implies, iff.
ii. forall, therexists.
iii. the binary relation symbol <, and the special binary relation symbol =.
iv. variables (intuitively ranging over natural numbers only).
v. the special symbol #.
vi. Comma, semicolon, parentheses.

We inductively define the formulas.

a. If x,y are variables then x = y and x < y are formulas.
b. If A,B are formulas then (notA). (A and B), (A or B), (A implies 
B), (A iff B) are formulas.
c. If A is a formula and x is a variable then (forall x)(A), 
(therexists x)(A) are formulas.
d. If A is a formula, k >= 1, x1,...,xk are distinct variables, and y 
is a variable, then #(A,y1,...,yk;y) is a formula.

The idea in d is that #(A,x1,...,xk;y) is read:

the number of k-tuples x1,...,xk such that A, is y.

We emphasize that we are not committed to any notion of ordered 
tuples, and certainly not any notion of set or predicate-as-object.

We will give these axioms informally, as I don't right now have the 
time to give a completely formal treatment. The completely formal 
treatment is rather straightforward, except that it is quite 
difficult to do without any bugs. There are issues about clashes of 
variables, free and bound, that have to be done just right.

1. All tautologies.
2. < is a strict linear ordering.
3. (therexists y)(#(A,x1,...,xk;y) if and only if the x1,...,xk such 
that A holds are bounded in the sense of <. In this case, y is unique.
4. Various equality axioms. Besides the completely obvious, there is 
the one that asserts that #(A,x1,...,xk;y) depends only on just what 
x1,...,xk are such that A holds of x1,...,xk.
5. Suppose that the x1,...,xk such that A, and the y1,...,yp such 
that B, are bounded. Suppose that the former are in one-one 
correspondence with a proper portion of the latter, where this 
one-one correspondence is presented by a formula in the language of 
this system. Then for the unique y,z such that #(A,x1,...,xk;y) and 
#(B,y1,...,yp;z), we have y < z.
6. #(x < y,y).

There is a natural fragment of the language of COA in which no 
quantifiers are allowed in any formula that starts with #. We can 
restrict COA to all axioms of COA that live in this restricted 
language. Call this COA'.

We can also view the language of COA and COA' as consisting of <,=, 
and infinitely many new relation symbols. I.e., a symbol R where the 
meaning of R(y1,...,yn,z) is that the number of x1,...,xk such that 
A(x1,...,xk,y1,...,yn) is z. (One has to worry about clashes of free 
and bound variables, etc.). The various R's can be used to support 
other R's.

THEOREM. COA and COA' prove induction for all formulas in the language.

THEOREM. PA, COA, COA', when suitably formulated as in the previous 
paragraph, are mutually interpretable. In fact, they are synonymous, 
with objects and <,= unchanged.

The main point is that there are very natural and obvious definitions 
of 0,1,+,times, and the usual quantifier free axioms involving <,= 
are provable in COA and COA'.

In particular, can interpret WKL in COA and COA'. One has also 
conservative extension results.

What I don't see how to do is to treat PA' this way. Could it be that 
COUNTING has a very natural canonical stopping place at PA, yet 
INDUCTION/RECURSION does not? Induction/recursion does not because 
of, e.g., PA' and somewhat beyond.

I should add that PA' is naturally extended to be stronger than even 
ACA (ACA0 with full induction).