EXPOSITION
Language:
Primitives:
Basic primitives
= denoting equality, is a binary relation symbol
O denoting zero, is a zero-ary function symbol (i.e. a constant).
S denoting the binary function successor
Pn;i denoting projection, is an n-ary function symbol for n>=1; 1=<i<=n
Composite primitives.
if f is a k-ary primitive function symbol and g1,..,gk are m-ary primitive function symbols, then the symbol fog1..gk, denoting the composition of f and the gi's, is an m-ary primitive function symbol.
if f is a k-ary function symbol and g is a k+2-ary function symbol, then
f@g, denoting the primitive recursive function of f and g, is a k+1-ary primitive function symbol.
Terms of the language:
1. sorted variables:
x_i, x_(j_k), for i=0,1,2,3,...; (j_k)=0,1,2,... for k=1,2,3,... are terms.
2. function symbols:
The constant O is a term
S(x_i) is a term for i=0,1,2,3,...
Pn;i(x_(j_1),...,x_(j_n)) for n>=1, 1=<i=<n is a term.
if f is a k-ary primitive function symbol and t1,..,tk are terms, then
f(t1,..,tk) is a term.
Formula formation rules:
The atomic formulas are composed of a single primitive predicate symbol which is = between two term symbols. All variable symbols must be sorted
Composition of formulas from atomic formulas proceed as in the usual manner for first order logic.
Axioms:
Identity axioms:
I. for i=0,1,2,3,.....
x_i = x_i is an axiom.
II. for i=0,1,2,3,....; j=0,1,2,3,...; if phi(x_i) is a formula in which
x_i is free and phi(x_i|x_j) is the formula obtained from phi(x_i) by
merely replacing all occurrences of the symbol x_i in it by the symbol x_j,
and replacing all bounded occurrences of x_j in phi(x_i) by a symbol that
is new to all symbols in phi(x_i), then:
phi(x_i) ^ x_i = x_j -> phi(x_i|x_j)
is an axiom.
Axioms about O:
1. x_0 = O
2. for i=0,1,2,3,....
~ O=S(x_i) is an axiom.
Axioms about sorts:
1'. for i=0,1,2,3,...
for all x_i Exist x_(i+1) [ x_(i+1) = x_i ] is an axiom
2'. for i=0,1,2,3,...
Exist! x_(i+1) for all x_i [ ~ x_(i+1) = x_i ] is an axiom.
Define Peculiar(x_i):- Peculiar(x_i)=y_i <-> ~Exist x_(i-1) (x_(i-1)=y_i)
3'. for i=0,1,2,3,...
Exist! y_i for all x_i (~ x_i= S(y_i)) is an axiom
Exist! y_i for all x_i (~ y_i= S(x_i)) is an axiom
Define end(x_i):- y_i = end(x_i) <-> for all x_i (~ x_i= S(y_i))
Define start(x_i):- y_i=start(x_i) <-> for all x_i (~ y_i= S(x_i))
4'. for i=0,1,2,3,...
S(end(x_(i-1)))= Peculiar(x_i) is an axiom.
Axioms about successor "S":
1". for i=0,1,2,3,...; j=0,1,2,3,...
for all x_i,x_j (S(x_i) = S(x_j) -> x_i=x_j) is an axiom.
Axioms about Projections:
for n=1,2,3,...; 1=<i=<n,
Pn;i(x_(j_1),...,x_(j_n)) = x_(j_i)
Axioms about Compositions:
for m=1,2,3,...; k=1,2,3,...; (i_r)=0,1,2,... for r=1,2,..,m; If f is a primitive k-ary function and g1,..,gk are primitive m-ary functions, then:
for all x_(i_1),..,x_(i_m)
[fog1..gk(x_(i_1),..,x_(i_m)) = f(g1(x_(i_1),..,x_(i_m)),...,gk(x_(i_1),..,x_(i_m))]
is an axiom.
Axioms about Primitive Recursions:
for j=0,1,2,3,...; (i_r)=0,1,2,3,..for 1=<r<=k; If f is a primitive k-ary function symbol and g is a primitive k+2-ary function, then:
for all x_(i_1),..,x_(i_k),y_j
[f@g(O,x_(i_1),..,x_(i_k)) = f(x_(i_1),..,x_(i_k))
^
f@g(S(y_j),x_(i_1),..,x_(i_k)) = g(y_j, f@g(y_j,x_(i_1),..,x_(i_k)), x_(i_1),..,x_(i_k))]
is an axiom
/Theory definition finished.
Main theorem is:
Induction Theorem schema: for i=0,1,2,3,...; if phi is a formula in which x_i is free, then:
phi (O) ^ for all x_i [phi(x_i) -> phi(S(x_i))] -> for all x_i phi(x_i)
is a theorem.
I still think that this theory is both Categorical and Complete. All kinds of ordinary arithmetic can be done within this theory.
Zuhair April 1 2017
EXPOSITION
Language: infinitely many multi-sorted FOL with Peano arithmetic primitives in predicate forms (except O),
The BASIC atomic formulas of this language are:
x_i = y_j ; S(x_i,y_j) ; Pi,n (x_(j_1),..,x_(j_i),..,x_(j_n), x_(j_i)),
for i=0,1,2,3,…; j=0,1,2,3,…; j_r=0,1,2,3,... for r=1,2,3,....,n;
n=1,2,3,...
Formation of primitive recursive predicate and function symbols:
O is a primitive recursive zero-ary function symbol
S is a primitive recursive binary predicate symbol
Pi,n is a primitive recursive n+1_ary predicate symbol for n>=1, 1=<i=<n.
If f is a primitive recursive k+1_ary predicate symbol and g1,..,gk are primitive recursive m+1_ary predicate, then the symbol
f_g1_..._gk is a primitive recursive m+1_ary predicate symbol
If f is a primitive recursive k+1_ary predicate symbol, and g
is a primitive recursive k+3_ary predicate symbol, then the symbol
f-g is a primitive recursive k+2_ary predicate symbol
A non basic primitive recursive n_ary predicate symbol followed by an n_ary string of sorted variables, constitutes a SECONDARY atomic formula.
The rest of rules of formation of non-atomic formulae proceed in the customary manner
Axioms:
Identity axioms:
I. for i=0,1,2,3,.....
x_i = x_i is an axiom.
II. for i=0,1,2,3,....; j=0,1,2,3,...; if phi(x_i) is a formula in which
x_i is free and phi(x_i|x_j) is the formula obtained from phi(x_i) by
merely replacing all occurrences of the symbol x_i in it by the symbol x_j,
and replacing all bounded occurrences of x_j in phi(x_i) by a symbol that
is new to all symbols in phi(x_i), then:
phi(x_i) ^ x_i = x_j -> phi(x_i|x_j)
is an axiom.
Axioms about O:
1. x_0 = O
2. for i=0,1,2,3,....
~ S(x_i,x_0) is an axiom.
Axioms about sorts:
1'. for i=0,1,2,3,...
for all x_i Exist x_(i+1) [ x_(i+1) = x_i ] is an axiom
2'. for i=0,1,2,3,...
Exist! x_(i+1) for all x_i [ ~ x_(i+1) = x_i ] is an axiom.
Define Peculiar(x_i):- Peculiar(x_i)=y_i <-> ~Exist x_(i-1) (x_(i-1)=y_i)
3'. for i=0,1,2,3,...
Exist! y_i for all x_i (~ S(y_i,x_i)) is an axiom
Exist! y_i for all x_i (~ S(x_i,y_i)) is an axiom
Define end(x_i):- y_i = end(x_i) <-> for all x_i (~ S(y_i,x_i))
Define start(x_i):- y_i=start(x_i) <-> for all x_i (~ S(x_i,y_i))
4'. for i=0,1,2,3,...
S(end(x_(i-1)),Peculiar(x_i)) is an axiom.
Axioms about successor "S":
1". for i=0,1,2,3,...; j=0,1,2,3,.., k=0,1,2,3,..
for all x_i,x_j,x_k (S(x_i,x_k) ^ S(x_j,x_k) -> x_i=x_j) is an axiom.
2". for i=0,1,2,3,...; j=0,1,2,3,.., k=0,1,2,3,..
for all x_i,x_j,x_k (S(x_k,x_i) ^ S(x_k,x_j) -> x_i=x_j) is an axiom.
Axioms about Composition: for m=1,2,3,...; k=1,2,3,...; d=0,1,2,3,....; i_r=0,1,2,... for r=0,1,2,...
If f is a primitive recursive k+1_ary predicate symbol and g1,..,gk are primitive recursive m+1_ary predicate symbols, then:
for all x_(i_1),..,x_(i_m) exist! y_(j_1) (g1(x_(i_1),..,x_(i_m),y_(j_1)))^..^for all x_(i_1),..,x_(i_m) exist! y_(j_k) (gk(x_(i_1),..,x_(i_m),y_(j_k)))
for all x_(i_1),..,x_(i_k) exist! z_d (f(x_(i_1),..,x_(i_k),z_d))
->
for all x_(i_1),..,x_(i_m),y_(j_1),...,y_(j_k) [g1(x_(i_1),..,x_(i_m),y_(j_1))^ ..^ gk(x_(i_1),..,x_(i_m),y_(j_k)) ->
for all z_d (f_g1_.._gk(x_(i_1),..,x_(i_m),z_d) <-> f(y_(j_1),...,y_(j_k),z_d)]
is an axiom.
Axioms about Primitive Recursion: for k=1,2,3,...; j=0,1,2,3,...; d=0,1,2,3,..; p=0,1,2,3,...; i_r=0,1,2,... for r=0,1,2,...
If f is a primitive recursive k+1_ary predicate symbol and g is a primitive recursive k+3_ary predicate symbol, then:
for all x_(i_1),..,x_(i_k) exist! y_j (f(x_(i_1),..,x_(i_k),y_j)) ^ for all x_(i_1),..,x_(i_k+2) exist! y_j (g(x_(i_1),..,x_(i_k+2),y_j))
->
for all x_(i_1),..,x_(i_k) ,y_j, z_p [f-g (y_j, x_(i_1),..,x_(i_k),z_p) ->
for all z_d ((f-g(O,x_(i_1),..,x_(i_k),z_d) <-> f(x_(i_1),..,x_(i_k),z_d)) ^
for all z-d (f-g(S(y_j),x_(i_1),..,x_(i_k),z_d) <-> g(y_j, z_p , x_(i_1),..,x_(i_k),z_d))]
is an axiom
/Theory definition finished.
Main Theorem:
Induction theorem scheme: for i=0,1,2,3,...; if phi is a formula in which x_i is free, then:
phi (O) ^ for all x_i,x_(i+1) [phi(x_i) ^ S(x_i,x_(i+1)) -> phi(x_(i+1))]
-> for all x_i phi(x_i)
is a theorem.
Also the main claim is that this theory is complete and Categorical.
Zuhair March 28 2017