Hostname: page-component-cd9895bd7-gvvz8 Total loading time: 0 Render date: 2024-12-23T17:54:35.949Z Has data issue: false hasContentIssue false
  • English
  • Français

Intuitionistic completeness for first order classical logic

Published online by Cambridge University Press:  12 March 2014

Stefano Berardi
Stefano Berardi*
Affiliation:
Dipartimento di Informatica Dell'Università di Torino, C.SO Svizzera 185, 10149 Torino, Italy E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic.

All results included here, but a part of the proposition (a) below, are new. This work is, ideally, a continuation of a paper by McCarty, who considered intuitionistic completeness mostly for first order intuitionistic logic.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 64 , Issue 1 , March 1999 , pp. 304 - 312
Copyright
Copyright © Association for Symbolic Logic 1999

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]Baratella, S. and Berardi, S., Yet another constructivization of classical logic, Proceedings of 1995 Venice congress “Twenty-five years of constructive type theory”.Google Scholar
[2]Coquand, T., A semantic of evidence for classical arithmetic, this Journal, vol. 60 (1995), no. 1.Google Scholar
[3]Herbelin, H., Sequents qu’on calcule, Ph.D. thesis, University of Paris VII, 01 1995.Google Scholar
[4]Kreisel, G., On the interpretation of non-finitist proofs, this Journal, vol. 16 (1951), p. 261.Google Scholar
[5]Krivine, J.-L., Une preuve formelle et intuitionniste du theoreme de completude de la logique classique, Bulletin of Symbolic Logic, to appear, available by ftp from boole.logique.jussiue.fr in pub/distrib/krivine.Google Scholar
[6]McCarty, , Undecidability and intuitionistic incompleteness, Journal of Philosophical Logic, vol. 25 (1996), pp. 559–565.CrossRefGoogle Scholar
[7]McCarty, , Completeness for intuitionistic logic, to appear in P. Odifreddi's book about G. Kreisel, 1997.Google Scholar
[8]Paulin-Mohring, Ch., Extraction de programmes dans le calcul des constructions, These de doctorat, Universite de Paris VII, 1989.Google Scholar
[9]Shoenfield, J. R., Mathematical Logic, ch. 8, Number theory, Addison-Wesley, London, 1967.Google Scholar
[10]Tait, W. W., Normal derivability in classical logic: The syntax and semantic of infinitary languages, Lecture Notes in Mathematics, vol. 72, Springer-Verlag.Google Scholar
[11]Trölstra, and Dalen, Van, Constructivism in Mathematics, ch. 13, Semantic completeness, North-Holland.Google Scholar