Article contents
Algebraic theories with definable Skolem functions
Published online by Cambridge University Press: 12 March 2014
Extract
(1.1) A well-known example of a theory with built-in Skolem functions is (first-order) Peano arithmetic (or rather a certain definitional extension of it). See [C-K, pp. 143, 162] for the notion of a theory with built-in Skolem functions, and for a treatment of the example just mentioned. This property of Peano arithmetic obviously comes from the fact that in each nonempty definable subset of a model we can definably choose an element, namely, its least member.
(1.2) Consider now a real closed field R and a nonempty subset D of R which is definable (with parameters) in R. Again we can definably choose an element of D, as follows: D is a union of finitely many singletons and intervals (a, b) where – ∞ ≤ a < b ≤ + ∞; if D has a least element we choose that element; if not, D contains an interval (a, b) for which a ∈ R ∪ { − ∞}is minimal; for this a we choose b ∈ R ∪ {∞} maximal such that (a, b) ⊂ D. Four cases have to be distinguished:
(i) a = − ∞ and b = + ∞; then we choose 0;
(ii) a = − ∞ and b ∈ R; then we choose b − 1;
(iii) a ∈ R and b ∈ = + ∞; then we choose a + 1;
(iv) a ∈ R and b ∈ R; then we choose the midpoint (a + b)/2.
It follows as in the case of Peano arithmetic that the theory RCF of real closed fields has a definitional extension with built-in Skolem functions.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1984
References
REFERENCES
- 32
- Cited by