[FOM] Count Calculus

[Harvey Friedman]

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