Search

It will be shown that propositional tense logic (with the Kripke relational semantics) may be regarded as a fragment of propositional modal logic (again with the Kripke semantics). This paper deals only with model theory. The interpretation of formal systems of tense logic as formal systems of modal logic will be discussed in [6].The languages M and T, of modal and tense logic respectively, each have a countable infinity of propositional variables and the Boolean connectives; in addition, M has the unary operator ⋄ and T has the unary operators F and P. A structure is a pair . If Γ is a set of formulas of M [T] and α is a formula of M [T], then α is a logical consequence of Γ, or Γ ⊩ α,if α is valid in every model of Γ i.e., in every structure in which all γ ∈ Γ are valid.

In classical logic a collection of sets of statements (or equivalently, a property of sets of statements) is called a consistency property if it meets certain simple closure conditions (a definition is given in §2). The simplest example of a consistency property is the collection of all consistent sets in some formal system for classical logic. The Model Existence Theorem then says that any member of a consistency property is satisfiable in a countable domain. From this theorem many basic results of classical logic follow rather simply: completeness theorems, the compactness theorem, the Lowenheim-Skolem theorem, and the Craig interpolation lemma among others. The central position of the theorem in classical logic is obvious. For the infinitary logic the Model Existence Theorem is even more basic as the compactness theorem is not available; [8] is largely based on it.In this paper we define appropriate notions of consistency properties for the first-order modal logics S4, T and K (without the Barcan formula) and for intuitionistic logic. Indeed we define two versions for intuitionistic logic, one deriving from the work of Gentzen, one from Beth; both have their uses. Model Existence Theorems are proved, from which the usual known basic results follow. We remark that Craig interpolation lemmas have been proved model theoretically for these logics by Gabbay ([5], [6]) using ultraproducts. The existence of both ultra-product and consistency property proofs of the same result is a common phenomena in classical and infinitary logic. We also present extremely simple tableau proof systems for S4, T, K and intuitionistic logics, systems whose completeness is an easy consequence of the Model Existence Theorems.

In [10], Kripke gave a definition of the semantics of the intuitionistic logic. Fitting [2] showed that Kripke's models are equivalent to algebraic models (i.e., pseudo-Boolean models) in a certain sense. As a corollary of this result, we can show that any partially ordered set is regarded as a (characteristic) model of a intermediate logic ^ We shall study the relations between intermediate logics and partially ordered sets as models of them, in this paper. We call a partially ordered set, a Kripke model.2^ At present we don't know whether any intermediate logic 'has a Kripke model. But Kripke models have some interesting properties and are useful when we study the models of intermediate logics. In §2, we shall study general properties of Kripke models. In §3, we shall define the height of a Kripke model and show the close connection between the height and the slice, which is introduced in [7]. In §4, we shall give a model of LP» which is the least element in n-ih slice Sn (see [7]).

In what follows there is presented a unified semantic treatment of certain “paradox-free” systems of entailment, including Church's weak theory of implication (Church [7]) and logics akin to the systems E and R of Anderson and Belnap (Anderson [3], Belnap [6]). We shall refer to these systems generally as relevant logics.The leading idea of the semantics is that just as in modal logic validity may be defined in terms of certain valuations on a binary relational structure so in relevant logics validity may be defined in terms of certain valuations on a semilattice—interpreted informally as the semilattice of possible pieces of information. Completeness theorems can be given relative to these semantics for the implicational fragments of relevant logics. The semantical viewpoint affords some insights into the structure of the systems—in particular light is thrown upon admissible modes of negation and on the assumptions underlying rejection of the “paradoxes of material implication”.The systems discussed are formulated in fragments of a first-order language with → (entailment), &, ⋁, ¬,(x) and (∃x) primitive, omitting identity but including a denumerable list of propositional variables (p, q, r, p1,…etc.), and (for each n > 0), a denumerable list of n-ary predicate letters. The schematic letters A, B, C, D, A1,… are used on the meta-level as variables ranging over formulas. The conventions of Church [9] are followed in abbreviating formulas. The semantics of the systems are given in informal terms; it is an easy matter to turn the informal descriptions into formal set-theoretical definitions.

Publisher Summary This chapter discusses the semantics of entailment. Earlier, modal logics had no semantics. Bearing a real world G, a set of worlds K, and a relation R of relative possibility between worlds, Saul Kripke beheld this situation and saw that it was formally explicable and made model structures. It came to pass that soon everyone was making model structures, and some were deontic, some were temporal, and some were epistemic, according to the conditions on the binary relation R. The models made by Kripke, Hintikka, and Thomason were, however, not relevant. Central to the semantics being developed is a ternary relation R that takes the place for the relevant logics of the Kripke binary relation for standard modal and intuitionistic logics.

This work is a sequel to Q4]. The familiarity with the results and terminology of T4] is presupposed. It is a well-known fact that the intuitionistic prepositional logic (abbreviated as LJ) has not a finite characteristic model. But, Jaskowski proved that there is a monotonic descending sequence of finite models which converges to LJ. Using the notation in Q4], we can restate this result as follows; there are finite (pseudo-Boolean) models Pi(i € /) such that LJ^Cr\ieIPi. Now, let's consider the following problem. Let L be any intermediate logic. Are there finite pseudo-Boolean models Pi(i €E /) such that ZOCAie/ Pi? If this problem is solved affirmatively for a logic Z,, we say L has the finite model property, following Harrop's terminology Ql]. In Ql], it is proved that if a logic L is finitely axiomatizable and has the finite model property then L is decidable. It is an interesting problem whether all intermediate logics are decidable. But we don't know even whether all intermediate logics have the finite model property. In this paper, we show that this problem can be reduced to the following problem presented in \j£}: Has any intermediate logic a characteristic Kripke model ? We extend the result to that for logics between Johansson's minimal logic and the classical prepositional logic, and show that the logics whobe decidability are not known in £5] are decidable. Now, we state our main theorem.

This paper is a sequel to [7], and the terminology of [7] is largely presupposed here. In [7], the algebraic methods of McKinsey-Tarski were employed and extended to yield semantic results of a Kripke kind for a class of relatively weak modal logics, the strongest of which was the Feysvon Wright system T. Deontic versions of both T and E2, called T(D) and D2, and even weaker systems, were handled. The main aim of the present paper is to extend these results to stronger systems of modal logic. Thus the Lewis systems S2–S5, the Brouwersche system B of Kripke [4], the systems E3–E5 of [5], and Łukasiewicz's modal logic, as well as certain new systems, are considered.Certain modifications of the method of [7] have proved convenient. Thus in Section I, some further results concerning model structures are proved in order that the relationship between S2 and E2, S3 and E3, can be properly stated; in particular, the notions of a refined and connected model structure play a pervasive role throughout.

In ClOj, we developed the method of Kripke models and gave some applications of it to the study of the intermediate logics. We found that the use of Kripke models is very efficient, since in many cases the algebraic structure of Kripke models reflects well the properties of the logics characterized by them. In dll]], we proved that a certain relation holds between the logics characterized by some Kripke models and the logics having the finite model property. As we stated in the correction at the end of CllH, the original proof contained an error. So, we emphasize here that the following problem remains open: Has any intermediate logic a characteristic Kripke model? In this paper, we will proceed in the same direction as Hi OH anc* Ell]. At present, we have at hand many particular intermediate logics. But we have very little knowledge about the general properties common to many logics. For instance, though many logics having the disjunction property have been known, we don't know what conditions make a logic have the disjunction property. We think that the central aim of the study of intermedate logics is to construct the theory about the general properties of them. The notion of the slice introduced by Hosoi Q4] gave us the first clue to our purpose. We will introduce in §1 other classifications of intermediate logics. In §2, we will characterize them by Kripke models, just as the slice was characterized by the height of Kripke models in [110]. In §3, we will investigate about the disjunction property in connection with these classifications. We assume familiarity with the terminologies and the notions of ^10]. In ^10], we consider a

In [1] and [2] I investigated logics intermediate between intuitionistic and classical propositional logic. In the present paper I shall study inclusion and non-inclusion between certain intermediate predicate logics. All the logics considered result from intuitionistic predicate logic by addition of classically valid axiom schemes.

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 ϕ(a1 … an) under the indicated assignment at α is denoted by [ϕ(a1 … an)]α.A Kripke model is said to be of constant domains if all the models Aα, α ∈ T, have the same domain.

1 This paper is a continuation of the investigations reported in Corcoran and Weaver [1] where two logics j£Π and -CDD, having natural deduction systems based on Lewis's S5, are shown to have the usually desired properties (strong soundness, strong completeness, compactness). As in [1], we desire to treat modal logic as a "clean" natural deduction system with a conceptually meaningful semantics. Here, our investigations are carried out for several S4 based logics. These logics, when regarded as logistic systems (cf. Corcoran [2], p. 154), are seen to be equivalent; but, when regarded as consequence systems (ibid., p. 157), one diverges from the others in a fashion which suggests that two standard measures of semantic complexity may not be linked. Some of the results of [l] are presupposed here and the more obvious definitions will not be repeated in detail. We consider the logics -Cl, -C2, and -£3. These logics share the same language (^DD) and deductive system (Δ'DD) but each has its own semantics system (Σl, Σ2, Σ3). Σl is an extension of the Kripke [3] semantics for S5 as modified in [l], Σ2 is largely due to Makinson [5], and Σ3 is due to Kripke [4]. -C DD is the usual modal sentential language with D, ~ and 3 as logical constants (see 2 below). Δ'DD (see 3 below), a modification of the natural deduction system given in [l], permits proofs from arbitrary sets of premises. For S a set of sentences and A & sentence, Sv-A means that A is provable from S, i.e., there is a proof (in Δ'DD) of A whose premises are among the members of S. ([-A means S\-A where S is empty.) If S\-A, we sometimes say that the argument (S, A) is demonstrable and when, in addition, S is empty we say that A is provable.

Kripke's model structure for D2 is a quadruple (G, K, R, N) where N is the set of normal elements, i.e., the subset of K such that for every H in N, HRH. (See [1, p. 220, p. 211].) In fact, however, this structure provides a model for E2, as the work of Lemmon shows ([2, pp. 58–62]).To show the inadequacy of Kripke's model structure, we show that the E2 thesis □B ⊃ B, not a thesis of D2, is valid under Kripke's modelling for D2. Suppose, for a reductio argument, that □ B ⊃ B is false for some valuation ϕ in some D2 model structure. Thenyϕ(□B ⊃ B, G) = F; so by truth-functional assignments