Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-25T04:42:03.710Z Has data issue: false hasContentIssue false
  • English
  • Français

A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property1

Published online by Cambridge University Press:  12 March 2014

D. M. Gabbay  and
D. H. J. De Jongh
D. M. Gabbay
Affiliation:
Stanford University, Stanford, California 94305
D. H. J. De Jongh
Affiliation:
Suny at Buffalo, Amherst, New York 14226
Get access Rights & Permissions [Opens in a new window]

Extract

The intuitionistic propositional logic I has the following (disjunction) property

.

We are interested in extensions of the intuitionistic logic which are both decidable and have the disjunction property. Systems with the disjunction property are known, for example the Kreisel-Putnam system [1] which is I + (∼ϕ → (ψ ∨ α))→ ((∼ϕ→ψ) ∨ (∼ϕ→α)) and Scott's system I + ((∼ ∼ϕ→ϕ)→(ϕ ∨ ∼ϕ))→ (∼∼ϕ ∨ ∼ϕ). It was shown in [3c] that the first system has the finite-model property.

In this note we shall construct a sequence of intermediate logics Dn with the following properties:

These systems are presented both semantically and syntactically, using the remarkable correspondence between properties of partially ordered sets and axiom schemata of intuitionistic logic. This correspondence, apart from being interesting in itself (for giving geometric meaning to intuitionistic axioms), is also useful in giving independence proofs and obtaining proof theoretic results for intuitionistic systems (see for example, C. Smorynski, Thesis, University of Illinois, 1972, for independence and proof theoretic results in Heyting arithmetic).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 39 , Issue 1 , March 1974 , pp. 67 - 78
Copyright
Copyright © Association for Symbolic Logic 1974

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

Earlier version appeared in Technical Report, Jerusalem, 1969.

References

REFERENCES

[1]Kreisel, G. and Putnam, H., Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül, Archiv für mathematische Logic und Grundlagenforschung, vol. 3 (1957), pp. 74–78.CrossRefGoogle Scholar
[2]Kripke, S., Semantic analysis for intuitionistic logic, Formal system and recursive functions (Crossley, J. and Dummett, M., Editors), North-Holland, Amsterdam, 1965.Google Scholar
[3]Gabbay, D. M., Decidability results in nonclassical logics. I, Annals of Mathematical Logic (to appear).Google Scholar
[3a]Gabbay, D. M., On decidable, finitely axiomatizable, modal and tense systems without the finite model properly, Israel Journal of Mathematics, vol. 10 (1971), pp. 478–503.CrossRefGoogle Scholar
[3b]Gabbay, D. M., Decidability of the Kreisel-Putnam system, this Journal, vol. 35 (1970), pp. 431–437.Google Scholar
[3c]Gabbay, D. M., Model theory for intuitionistic logic, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 18 (1971), pp. 49–54.CrossRefGoogle Scholar
[4]Rabin, M. O., Decidability of second order theories and automata on trees, Transactions of the American Mathematical Society, vol. 141 (1969), pp. 1–35.Google Scholar
[5]Troelstra, A. S., Intermediate logics, Indagationes Mathematicae, vol. 27 (1965), pp. 141–152.CrossRefGoogle Scholar
[6]Segerberg, K., Propositional logics related to Heyting's and Johansson's, Theoria, vol. 34 (1968), pp. 26–61.CrossRefGoogle Scholar
[7]Gabbay, D. M., Semantical methods in non-classical logics, North-Holland, Amsterdam (to appear).Google Scholar