Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-24T04:50:40.702Z Has data issue: false hasContentIssue false
  • English
  • Français

μ-definable sets of integers

Published online by Cambridge University Press:  12 March 2014

Robert S. Lubarsky
Robert S. Lubarsky*
Affiliation:
Department of Mathematics, Franklin and Marshall College, Lancaster, Pennsylvania 17604, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.

The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.

There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 1 , March 1993 , pp. 291 - 313
Copyright
Copyright © Association for Symbolic Logic 1993

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[Aa]Aanderaa, S., Inductive definitions and their closure ordinals, Generalized recursion theory (Fenstad, and Hinman, , editors), North-Holland, Amsterdam, 1974, pp. 207–220.Google Scholar
[Ac]Aczel, P., An introduction to inductive definitions, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 739–782.CrossRefGoogle Scholar
[AR]Aczel, P. and Richter, W., Inductive definitions and analogues of large cardinals, Conference in Mathematical Logic, London, 1970, Lecture Notes in Mathematics, vol. 255, Springer-Verlag, Berlin, 1971, pp. 1–10.Google Scholar
[B]Barwise, J., Admissible sets and structures, Springer-Verlag, Berlin, 1975.CrossRefGoogle Scholar
[BM]Barwise, J. and Moschovakis, Y., Global inductive definability, this Journal vol. 43 (1978), pp. 521–534.Google Scholar
[D]Devlin, K., Constructibility, Springer-Verlag, Berlin, 1984.CrossRefGoogle Scholar
[HP]Hitchcock, P. and Park, D. M. R., Induction rules and termination proofs, Proceedings of the 1st International Colloquium on Automata, Languages, and Programming, North-Holland, Amsterdam, 1973, pp. 225–251.Google Scholar
[K]Kozen, D., Results on the propositional μ-calculus, Theoretical Computer Science, vol. 27 (1983), pp. 333–354.CrossRefGoogle Scholar
[M]Moschovakis, Y., Elementary induction on abstract structures, North-Holland, Amsterdam, 1974.Google Scholar
[Pa]Park, D. M. R., Fixpoint induction and proof of program semantics, Machine intelligence V (Meltzer, and Michie, , editors), Edinburgh University Press, Edinburgh, 1970, pp. 59–78.Google Scholar
[P1]Platek, R., Foundations of recursion theory, Ph.D. thesis, Stanford University, 1966.Google Scholar
[R]Richter, W., Recursively Mahlo ordinals and inductive definitions, Logic Colloquium '69 (Gandy, and Yates, , editors), North-Holland, Amsterdam, 1971, pp. 273–288.CrossRefGoogle Scholar
[RA]Richter, W. and Aczel, P., Inductive definitions and reflecting properties of admissible ordinals, Generalized recursion theory, (Fenstad, and Hinman, , editors), North-Holland, Amsterdam, 1974, pp. 301–381.Google Scholar
[SD]Scott, D. and DeBakker, J. W., A theory of programs, unpublished manuscript, IBM, Vienna, 1969.Google Scholar