Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-24T05:57:32.422Z Has data issue: false hasContentIssue false

Applications of trees to intermediate logics

Published online by Cambridge University Press:  12 March 2014

Dov M. Gabbay*
Affiliation:
Stanford University, Stanford, California 94305

Extract

We investigate extensions of Heyting's predicate calculus (HPC). We relate geometric properties of the trees of Kripke models (see [2]) with schemas of HPC and thus obtain completeness theorems for several intermediate logics defined by schemas. Our main results are:

(a) ∼(∀x ∼ ∼ϕ(x) Λ ∼∀xϕ(x)) is characterized by all Kripke models with trees T with the property that every point is below an endpoint. (From this we shall deduce Glivenko type theorems for this extension.)

(b) The fragment of HPC without ∨ and ∃ is complete for all Kripke models with constant domains.

We assume familiarity with Kripke [2]. Our notation is different from his since we want to stress properties of the trees. A Kripke model will be denoted by (Aα, ≤ 0), αT where (T, ≤, 0) is the tree with the least member 0T and Aα, αT, is the model standing at the node α. The truth value at α of a formula ϕ(a1an) under the indicated assignment at α is denoted by [ϕ(a1an)]α.

A Kripke model is said to be of constant domains if all the models Aα, αT, have the same domain.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1972

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]Görnemann, S., Über eine Verschārfung der intuitionistischen Logik, Dissertation, Hannover, 1969.Google Scholar
[2]Kripke, S. A., Semantical analysis of intuitionistic logic I. Formal systems and recursive functions, Crossley, J.-Dummett, M. Editors, pp. 92130.Google Scholar
[3]Fitting, M., Intuitionistic logic model theory and forcing, North-Holland, Amsterdam, 1969.Google Scholar