16.01.2003

Transitive Closure, Induction, and Church Thesis

We argue that the concept of transitive closure is the key for understanding finitary inductive definitions and reasoning, and we provide evidence for the thesis that logics which are based on it (in which induction is a logical rule) are the right logical framework for the formalization and development of the more significant parts of mathematics.

We investigate the expressive power of languages with the most basic transitive closure operation TC, and show that with TC one can define all recursive predicates and functions from 0, the successor function and addition, yet with TC alone addition is not definable from 0 and the successor function.

We further show that nevertheless, in the presence of a pairing function TC does suffice for having all types of finitary inductive definitions of relations and functions. This leads to a particularly simple characterization of recursive enumerability, and so to a new, concise version of Church thesis. The language which is used for this characterization has only TC, disjunction, conjunction, equality, a constant 0, and a pairing function.