Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-22T20:23:28.020Z Has data issue: false hasContentIssue false
  • English
  • Français

On Skolemization in constructive theories

Published online by Cambridge University Press:  12 March 2014

Matthias Baaz  and
Rosalie Iemhoff
Matthias Baaz
Affiliation:
Technical University Vienna, Institute for Discrete Mathematics and Geometry, Wiedner Hauptstrasse 8-10, 1040 Vienna, Austria, E-mail: [email protected]
Rosalie Iemhoff
Affiliation:
University Utrecht, Department of Philosophy, Heidelberglaan 6–8, 3584 CS Utrecht, The Netherlands, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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
The Journal of Symbolic Logic , Volume 73 , Issue 3 , September 2008 , pp. 969 - 998
Copyright
Copyright © Association for Symbolic Logic 2008

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

[1]Baaz, M. and Iemhoff, R., Gentzen calculi for the existence predicate, Stadia Logica, vol. 82 (2005), no. 1, pp. 7–23.CrossRefGoogle Scholar
[2]Baaz, M. and Iemhoff, R., On interpolation in existence logics, LPAR 2005 (Sutcliffe, G. and Voronkov, A., editors), Lecture Notes in Computer Science, vol. 3835, Springer, 2005, pp. 697–711.Google Scholar
[3]Baaz, M. and Iemhoff, R., On the proof theory of the existence predicate, We will show them! Essays in honour of Dov Gabbay (Artëmov, S. N.et al., editors), King's College Publications, 2005, pp. 125–166.Google Scholar
[4]Baaz, M. and Iemhoff, R., The Skolemization of existential quantifiers in intuitionistic logic, Annals of Pure and Applied Logic, vol. 142 (2006), no. 1-3, pp. 269–295.CrossRefGoogle Scholar
[5]Buss, S. R., On Herbrand's theorem, Logic and Computational Complexity, Lecture Notes in Computer Science, vol. 960, 1995, pp. 195–209.CrossRefGoogle Scholar
[6]Buss, S. R. (editor), Handbook of Proof Theory, Elsevier, 1998.Google Scholar
[7]Fitting, M., Resolution for intuitionistic logic, International Symposium on Methodologies for Intelligent Systems (Ras, Z. and Zemankovaet, M., editors), North-Holland, 1987, pp. 400–407.Google Scholar
[8]Kreitz, G., Otten, J., Schmitt, S., and Pientka, B., Matrix-based constructive theorem proving, Intellectics and Computational Logic: Papers in honour of Wolfgang Bibel (Hölldobler, Steffen, editor), Kluwer, 2000, pp. 189–205.CrossRefGoogle Scholar
[9]Mints, G. E., An analogue of Herbrand's theorem for the constructive predicate calculus, Soviet Mathematics Doklady, vol. 3 (1962), pp. 1712–1715.Google Scholar
[10]Mints, G. E., Herbrand's theorem for the predicate calculus with equality and function symbols, Soviet Mathematics Doklady, vol. 7 (1966), pp. 911–914.Google Scholar
[11]Mints, G. E., The Skolem method in intuitionistic calculi, Proceedings of the Steklov Institute of Mathematics, vol. 121 (1972), pp. 73–109.Google Scholar
[12]Mints, G. E., Resolution strategies for the intuitionistic predicate logic, Constraint Programming (Mayoh, B., Tyugu, E., and Penjaam, J., editors), NATO ASI Series F, vol. 131, Springer, 1994, pp. 289–311.CrossRefGoogle Scholar
[13]Mints, G. E., Axiomatization of a Skolem function in intuitionistic logic, Formalizing the Dynamics of Information (Faller, M., Kaufmann, S., and Pauly, M., editors), Center for the Study of Language and Information Lecture Notes, vol. 91, 2000, pp. 105–114.Google Scholar
[14]Mints, G. E., Thoralf Skolem and the epsilon substitution method for predicate logic, Nordic Journal of Philosophical Logic, vol. 1 (2000), no. 2, pp. 133–146.Google Scholar
[15]Scott, D. S., Identity and existence in intuitionistic logic, Applications of Sheaves (Fourman, M. P., Mulvey, C. J., and Scott, D. S., editors), Lecture Notes in Mathematics, vol. 753, 1979, pp. 660–696.CrossRefGoogle Scholar
[16]Shankar, N., Proof search in the intuitionistic sequent calculus, Automated deduction, CADE-11 (Kapur, D., editor), Lecture Notes in Computer Science, vol. 607, Springer, Berlin, 1992, pp. 522–536.Google Scholar
[17]Troelstra, A. S. and Schwichtenberg, H., Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol. 43, Cambridge University Press, Cambridge, 1996.Google Scholar
[18]Troelstra, A. S. and van Dalen, D., Constructivism in Mathematics, vol. I, North-Holland, Amsterdam, 1988.Google Scholar
[19]Wallen, L. A., Automated Proof Search in Non-classical Logics, MIT Press, 1990.Google Scholar