[FOM] Another comment on Church Thesis

[Arnon Avron]

In a sort of continuation to Friedman recent comment on Church Thesis,
here is another new characterization of recursive enumerability
which has a completely different flavour:


Let V_0 be the set of Lisp S-expressions, i.e., the smallest set  
which contains 0 and is closed under the pairing operation. 
 
Define the langauge  PTC^+ as follows: 
 
Terms of  PTC^+: 
 
1) The constant 0 is a term. 
2) Every (individual) variable is a term. 
3) If t and s are terms then so is (t,s). 
 
Formulas of PTC^+: 
 
1) If t and s are terms then t=s is a formula. 
2) If A and B are formulas then so are A\/B and A&B.
3) If A is a formula, x,y are two different variables, 
   and t,s are terms, then (TC_{x,y}A)(t,s) is a formula. in this
   formula all occurences in A  of x and y are bound. 
 
Semantics of PTC^+: TC_{x,y}A denotes the transitive closure of the 
relation between x and y defined by A (note that A may have other free
variables which are taken as parameters). The meaning in V_0 of the other
components of PTC^+ is obvious.

Theorem: An n-ary realation on V_0 is r.e. iff it is definable
by some formula of PTC^+ with exactly n free variables.


A proof of this Theorem may be found in my paper: "Transitive Closure
and the Mechanization of Mathematics", in The book "Thirty-Five
Years of Automating Mathematics" (F. Kamareddine, ed.), Kluwer
Academic Publishers, 2003 (pp. 149-171).


Arnon Avron





----------------------------------------------------------------
                                | +972-3-640-6352   Office
Prof. Arnon Avron               | +972-3-640-8040   secretary
School of Computer Science      | +972-3-640-9357   Fax
Tel Aviv University             | +972-3-641-0043   Home
Tel Aviv, 69978                 |-------------------------------
ISRAEL                          | email: aa at math.tau.ac.il
                                | http://www.math.tau.ac.il/~aa/
----------------------------------------------------------------



--i0B7BOp26797.1073805084/tau.ac.il--