# [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

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--

```