[FOM] Another comment on Church Thesis

Arnon Avron aa at tau.ac.il
Sun Jan 11 04:51:00 EST 2004

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/


More information about the FOM mailing list