[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/
----------------------------------------------------------------
--i0B7BOp26797.1073805084/tau.ac.il--
More information about the FOM
mailing list