On extending the general recursion theorem to non-wellfounded relations

The principle of definition by recursion on a wellfounded relation [1], can be stated as follows: Let A be any set and let P be the set of all partial functions from A to some set B. Let G : A × P → B be any function and let R ⊆ A × A be any binary relation. Fact 1 (Montague): If R is wellfounded on A then there exists a unique function f: A → B such that ∀x ∈ A(f(x) = G(x,f|x^{R})), (1) where x^{R} = {y ∈ A | y R x}. If R is not wellfounded on the entire domain A, an obvious way of extending this method of definition is to identify a proper subset W of A on which R is wellfounded and to apply the principle to this set. The usual choice for W is the wellfounded part of R, defined as the set of all R-wellfounded points of A. In my talk, after examining several different strategies to prove Fact 1, I will present a new approach to extend this method of definition to all kinds of binary relations.We look at subsets X of A on which R is not necessarily wellfounded, yet there exists a unique function g : X → B which satisfies (1) for all x ∈ X. Let us call such subsets determined. Thenwe can prove Theorem. There exists a unique subset U of A such that (a) U is R-closed, i.e., ∀x ∈ U, xR ⊆ U; (b) U is determined and all R-closed subsets of U are determined; (c) U is the largest subset of A satisfying (a) and (b). This theorem ensures, for any relation R, the existence and uniqueness of a function g : U → B which satisfies (1) on its domain and is defined on a domain U which extends the wellfounded part W of R. [1] R. Montague, Well-founded relations: Generalizations of principles of induction and recursion. Bulletin American Mathematical Society, vol. 61, p. 442.