Recursive Definitions and Fixed-Points

AbstractAn expression such as ∀x(P(x)↔ϕ(P)), where P occurs in ϕ(P), does not always define P. When such expression implicitly defines P, in the sense of Beth [Beth, E. W., On Padoa's method in the theory of definitions., Indagationes Mathematicae 15 (1953), pp. 330–339] and Padoa [Padoa, A., Essai d'une théorie algébrique des nombres entiers, precedé d'une introduction logique a une théorie deductive quelconque, in: Bibliothèque Du Congrès International de Philosophie, 1900, pp. 118–123], we call it a recursive definition. In the Least Fixed-Point Logic (LFP), we have theories where interesting relations can be recursively defined [Ebbinghaus, H.-D. and J. Flum, “Finite Model Theory,” Springer-Verlag, 1995; Libkin, L., “Elements of Finite Model Theory,” Springer, 2004]. We will show that for some sorts of recursive definitions there are explicit definitions on sufficiently strong theories of LFP. It is known that LFP, restricted to finite models, does not have Beth's Definability Theorem [Gurevich, Y. and S. Shelah, On finite rigid structures, Journal of Symbolic Logic 61 (1996), pp. 549–562; Hodkinson, I.M., Finite variable logics, Bulletin of the EATCS 51 (1993), pp. 111–140; Dawar, A., L. Hella and P.G. Kolaitis, Implicit definability and infinitary logic in finite model theory, in: ICALP '95: Proceedings of the 22nd International Colloquium on Automata, Languages and Programming (1995), pp. 624–635]. Beth's Definability Theorem states that, if a relation is implicitly defined, then there is an explicit definition for it. We will also give a proof that Beth's Definability Theorem fails for LFP without this finite model restriction. We intend to investigate fragments of LFP for which Beth's Definability Theorem holds