[FOM] Count Calculus
Harvey Friedman
friedman at math.ohio-state.edu
Mon Jun 16 01:30:36 EDT 2003
This is a reply to Tennant in 3:58PM 6/12/03.
Tennant has inquired whether my Count Arithmetic #176, 6/10/03
8:54AM, can be extended to nonnumerical contexts.
The answer is yes, and profitably so.
First I want to make a minor correction to Count Arithmetic #176.
I did not present axiom 6 correctly. Here is the correct form.
6. #(x < y,x;y).
##################
There are a number of options in the formulation of count calculus. I
don't know which Tennant has in mind.
1. We can require that the intended interpretation of the counts be
the natural numbers. No infinite extension gets counted. In
particular, one can derive that the universal extension does not get
counted.
2. We can require that the intended interpretation of the counts be
the natural numbers. However, infinite extensions may get counted. In
particular, we can require or leave open that the universal extension
gets counted.
3. We can require that in the intended interpretation, every
extension gets counted. We require that the counts are linearly
ordered. We can require or leave open that every object is a count.
4. Whatever....
At least it appears that the language one wants to use is clear.
We can naturally use either a single sorted theory or a two sorted or
more sorted theory. We choose to formulate it as a single sorted
theory.
We will use the special binary relation symbols <,=, and the special
unary relation symbol C. Here C(x) means "x is a count", and x < y
means "x,y are counts and x is less than y".
We use constant, relation, and function symbols as in the usual first
order predicate calculus with equality. I.e., constants cn, n-ary
relations Rnm, n-ary functions Fnm. We use variables xn. Here n,m >=
1.
The formulas and terms are simultaneously defined as follows.
1. cn is a term.
2. if t1,...,tn are terms then Fnm(t1,...,tn) is a term and
Rnm(t1,...,tn) is a formula.
3. if s,t are terms then s = t and s < t and C(t) are formulas.
4. if A is a formula, y1,...,ym are variables, and t is a term, then
#(A,y1,...,ym;t) is a formula.
5. if A,B are formulas and x is a variable, then (notA), (A & B), (A
or B), (A arrows B), (A iff B), (forall x)(A), (therexists x)(A) are
formulas.
I will wait to see what Tennant advises before writing down axioms. I
would like to be responsive to philosopher's concerns, as there are
too many possibilities.
Harvey Friedman
More information about the FOM
mailing list