Applications of trees to intermediate logics

Abstract

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 0 ∈ T and A α , α ∈ T , is the model standing at the node α . The truth value at α of a formula ϕ ( a 1 … a n ) under the indicated assignment at α is denoted by [ ϕ ( a 1 … a n )] α . A Kripke model is said to be of constant domains if all the models A α , α ∈ T , have the same domain.