Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-16T15:29:23.549Z Has data issue: false hasContentIssue false
  • English
  • Français

The decidability of the Kreisel-Putnam system1

Published online by Cambridge University Press:  12 March 2014

Dov M. Gabbay
Dov M. Gabbay*
Affiliation:
Hebrew University of Jerusalem
Get access Rights & Permissions [Opens in a new window]

Extract

The intuitionistic propositional logic I has the following disjunction property

This property does not characterize intuitionistic logic. For example Kreisel and Putnam [5] showed that the extension of I with the axiom

has the disjunction property. Another known system with this propery is due to Scott [5], and is obtained by adding to I the following axiom:

In the present paper we shall prove, using methods originally introduced by Segerberg [10], that the Kreisel-Putnam logic is decidable. In fact we shall show that it has the finite model property, and since it is finitely axiomatizable, it is decidable by [4]. The decidability of Scott's system was proved by J. G. Anderson in his thesis in 1966.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 35 , Issue 3 , September 1970 , pp. 431 - 437
Copyright
Copyright © Association for Symbolic Logic 1971

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.)

Footnotes

1

This research was sponsored under contract no. N00014–69-G-0192 U.S. Office of Naval Research, Information System Branch.

References

[0]Diego, A., Sur les algebras de Hilbert, Gauthiers-Villars, Paris, 1966.Google Scholar
[1]Gabbay, D., Decidability results in nonclassical logics. I, to appear; Part II, in preparation.Google Scholar
[2]Gabbay, D., Model theory for intuitionistic logic. I, to appear.Google Scholar
[3]Gabbay, D. and de Jongh, D., Sequences of decidable, finitely axiomatizable intermediate logics with the disjunction property, to appear.Google Scholar
[4]Harrop, R., On the existence of finite models and decision procedures, Proceedings of the Cambridge Philosophical Society, vol. 54 (1958), pp. 1–16.CrossRefGoogle Scholar
[5]Kreisel, G. and Putnam, H., Eine Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül, Archiv für Mathematische Logik und Grundlagenforschung, vol. 3 (1957), pp. 74–78.CrossRefGoogle Scholar
[6]Kripke, S., Semantic analysis for intuitionistic logic, Formal systems and recursive functions, Amsterdam, J. Crossley-M. Dummett, Editors, 1965.Google Scholar
[7]McKay, C., Decidability of certain intermediate logics, this Journal, vol. 33 (1968), pp. 258–265.Google Scholar
[8]Medvedev, T., Interpretations of logical formulae by means of finite problems, Doklady, vol. 7 (1966), pp. 857–860.Google Scholar
[9]Rabin, M. O., Decidability of second order theories and automata on trees, Transactions of the American Mathematical Society, vol. 121 (1969), pp. 1–35.Google Scholar
[10]Segerberg, K., Propositional logics related to Heyting and Johansson, Theoria, vol. 34 (1968), pp. 26–61.CrossRefGoogle Scholar