Article contents
On Skolemization in constructive theories
Published online by Cambridge University Press: 12 March 2014
Abstract
In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied to the constructive theories of equality and groups.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2008
References
REFERENCES
- 9
- Cited by