[FOM] 176:Count Arithmetic

[Harvey Friedman]

This axiomatization of Peano Arithmetic using counting in place of 
induction was buried in an extended informal/semiformal interchange 
with Buckner on the FOM. It merits a numbered posting. I have edited 
out the matters that only pertain to the Buckner/Friedman 
interchange. I have also polished the language somewhat.

For the original message, see Buckner 1,2, 5/14/03, 6:17AM.

The essential point is that if we use counting instead of induction, 
then we do not need to single out any special arithmetic operations 
such as addition and multiplication - these (or related) ones) have 
to be singled out in the usual axiomatization of Peano Arithmetic.

FIRST ORDER COUNT ARITHMETIC WITHOUT INDUCTION
by
Harvey M. Friedman
May 14, 2003

We give a first order axiomatization of arithmetic that avoids 
induction, but instead directly supports "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.

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

This suggests the fundamental nature of this approach.

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.

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 standard purely logical axioms and rules pertaining to the 
language, with our variable binding operator #.
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. This is an alternative to using the variable binding 
operator #.

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'.

How does this pertain to Frege's foundations for arithmetic, and 
subsequent work in the philosophy community on this? Note that COA is 
a first order system.


*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 176th in a series of self contained numbered postings to 
FOM covering a wide range of topics in f.o.m. The list of previous 
numbered postings #1-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM

Harvey Friedman