Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-25T06:03:08.507Z Has data issue: false hasContentIssue false
  • English
  • Français

Completeness and incompleteness for intuitionistic logic

Published online by Cambridge University Press:  12 March 2014

Charles Mccarty
Charles Mccarty*
Affiliation:
Wolfson College, University of Oxford, Linton Road, Oxford OX2 6UD, UK
Get access Rights & Permissions [Opens in a new window]

Abstract

We call a logic regular for a semantics when the satisfaction predicate for at least one of its nontheorems is closed under double negation. Such intuitionistic theories as second-order Heyting arithmetic HAS and the intuitionistic set theory IZF prove completeness for no regular logics, no matter how simple or complicated. Any extensions of those theories proving completeness for regular logics are classical, i.e., they derive the tertium non datur. When an intuitionistic metatheory features anticlassical principles or recognizes that a logic regular for a semantics is nonclassical, it proves explicitly that the logic is incomplete with respect to that semantics. Logics regular relative to Tarski, Beth and Kripke semantics form a large collection that includes propositional and predicate intuitionistic, intermediate and classical logics. These results are corollaries of a single theorem. A variant of its proof yields a generalization of the Gödel-Kreisel Theorem linking weak completeness for intuitionistic predicate logic to Markov's Principle.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 73 , Issue 4 , December 2008 , pp. 1315 - 1327
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

[1985]Beeson, M., Foundations of constructive mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge, vol. 6, Springer-Verlag, Berlin, DE, 1985.CrossRefGoogle Scholar
[2004]Carter, N., Reflexive intermediate logics, Ph.D. Dissertation, Department of Mathematics, Indiana University, Bloomington, IN, 2004.Google Scholar
[2006]Carter, N., Reflexive intermediate prepositional logics, Notre Dame Journal of Formal Logic, vol. 47 (2006), no. 1, pp. 39–62.CrossRefGoogle Scholar
[2000]Dummett, M., Elements of intuitionism, second ed., Oxford Logic Guides, vol. 39, The Clarendon Press, Oxford, UK, 2000.CrossRefGoogle Scholar
[1978]Friedman, H., Classically and intuitionistically provably recursive functions, Higher set theory (Müller, G., editor), Lecture Notes in Mathematics, vol. 669, Springer-Verlag, Berlin, DE, 1978, pp. 21–27.CrossRefGoogle Scholar
[1981]Gabbay, D., Semantical investigations in Heyting's intuitionistic logic, Synthese Library, vol. 148, Springer-Verlag, Berlin, DE, 1981.CrossRefGoogle Scholar
[1962]Kreisel, G., Weak completeness of intuitionistic predicate logic, this Journal, vol. 27 (1962), pp. 139–158.Google Scholar
[1970]Kreisel, G., Church's Thesis: a kind of reducibility axiom for constructivemathematics, Intuitionism and proof theory (Kino, A., Myhill, J.. and Vesley, R., editors), North-Holland, Amsterdam, NL, 1970, pp. 121–150.Google Scholar
[1976]Leivant, D., Failure of completeness properties of intuitionistic predicate logic for constructive models, Annales Scientifiques de l'Université de Clermont. Série Mathématique, (1976), no. 13, pp. 93–107.Google Scholar
[1988]McCarty, C., Constructive validity is nonarithmetic, this Journal, vol. 53 (1988), pp. 1036–1041.Google Scholar
[1991]McCarty, C., Incompleteness in intuitionistic metamathematics, Notre Dame Journal of Formal Logic, vol. 32 (1991), no. 3. pp. 323–358, Summer 1991.CrossRefGoogle Scholar
[1996]McCarty, C., Undecidahility and intuitionistic incompleteness, Journal of Philosophical Logic, vol. 25 (1996), pp. 559–565.CrossRefGoogle Scholar
[2002]McCarty, C., Intuitionistic completeness and classical logic, Notre Dame Journal of Symbolic Logic, vol. 43 (2002), no. 4, pp. 243–248.Google Scholar
[1979]Rautenberg, W., Klassische und nichtklassische Aussagenlogik, Vieweg & Sohn, Braunschweig/Wiesbaden, DE. 1979.CrossRefGoogle Scholar
[1973]Troelstra, A., Metamathematical investigation of intuitionistic arithmetic and analysis. Springer Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin. DE, 1973.CrossRefGoogle Scholar
[1977]Troelstra, A., Completeness and validity for intuitionistic predicate logic, Colloque International de Logique (Clermont-Ferrand 1975), Colloques Internationaux du CNRS, vol. 249, Éditions du Centre National de la Recherche Scientifique, Paris, FR, 1977, pp. 39–58.Google Scholar
[1988]Troelstra, A. and van Dalen, D., Constructivism in mathematics. An introduction, vol. 1, North-Holland Publishing Co, Amsterdam, NL, 1988.Google Scholar