[FOM] 176:Count Arithmetic
friedman at math.ohio-state.edu
Tue Jun 10 08:54:26 EDT 2003
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
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
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
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
More information about the FOM