Hostname: page-component-7c8c6479df-5xszh Total loading time: 0 Render date: 2024-03-29T00:18:03.662Z Has data issue: false hasContentIssue false

On the strong semantical completeness of the intuitionistic predicate calculus

Published online by Cambridge University Press:  12 March 2014

Richmond H. Thomason*
Affiliation:
Yale University

Extract

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1968

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

[1]Beth, E., Formal methods, Reidel, Dordrecht, 1962.Google Scholar
[2]Church, A., Introduction to mathematical logic, vol. 1, Princeton Univ. Press, Princeton, N.J., 1956.Google Scholar
[3]Fitch, F., Symbolic logic, Ronald, New York, 1952.Google Scholar
[4]Gentzen, C., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934), pp. 176210 and 405–431.CrossRefGoogle Scholar
[5]Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines mathematischen Kolloquiums, Heft 2 (1932), pp. 3438.Google Scholar
[6]Henkin, L., The completeness of the first-order functional calculus, this Journal, vol. 14 (1949), pp. 159166.Google Scholar
[7]Kleene, S., Introduction to metamathematics, Van Nostrana, Princeton, N.J., 1952.Google Scholar
[8]Kripke, S., Semantical analysis of intuitionistic logic. I, Formal systems and recursive functions, ed. Crossley, J. and Dummett, M., Amsterdam, 1965, pp. 92130.CrossRefGoogle Scholar
[9]Leblanc, H. and Thomason, R., On the demarcation line between intuitionist logic and classical logic, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 12 (1966), pp. 257262.CrossRefGoogle Scholar
[10]Montague, R. and Henkin, L., On the definition of ‘formal deduction’, this Journal, vol. 21 (1957), pp. 129136.Google Scholar
[11]Rasiowa, H. and Sikorski, R., The mathematics of metamathematics, PWN, Warsaw, 1963.Google Scholar