[FOM] Re: 176:Count Arithmetic

[Harvey Friedman]

Reply to Tennant 6:24PM 6/10/03.

>On Tue, 10 Jun 2003, Harvey Friedman wrote:
>
>>  FIRST ORDER COUNT ARITHMETIC WITHOUT INDUCTION
>>  ...
>>  The vocabularly of COA (count arithmetic) is as follows.
>>  ...
>>  v. the special symbol #.
>>  ...
>>  We inductively define the 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.
>
>Does not this formation clause show that there is not just ONE symbol #,
>but rather a countable infinity of them (#1, #2, #3, ...) with increasing
>arities, to be used as follows:
>
>#1(A,x1;y)
>#2(A,x1,x2;y)
>#3(A,x1,x2,x3;y)
>:
>#k(A,x1,...,xk;y)
>:
>
>...?
>

There is no need to use more than one symbol #. The first order 
axioms and rules of inference for the supporting logic are obvious.

I would have thought that the appropriate "logic of variable binding 
terms" that supports this has been worked out by philosophers a long 
time ago, with supporting completeness theorems??

If you are trying to strictly force this into the usual mold of 
ordinary predicate calculus with equality, then you should go further 
with this than you have. You would introduce n+1-ary relation symbols

#_A,k,n

where A is any formula (with or without these new symbols) whose free 
variables are among x1,...,xk+n. The intended interpretation is given 
by

#_A,k,n(xk+1,...,xk+n,y) iff y is the cardinality of {(x1,...,xk): 
A(x1,...,xk+n)}.