Applications of trees to intermediate logics

1972 ◽  
Vol 37 (1) ◽  
pp. 135-138 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Kripke Model ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Geometric Properties ◽  
Intermediate Logics ◽  
Truth Value ◽  
Constant Domains ◽  
Completeness Theorems

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.

Sufficient conditions for the undecidability of intuitionistic theories with applications

1972 ◽  
Vol 37 (2) ◽  
pp. 375-384 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Decision Problem ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
The Other ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Symmetric Relation ◽  
Undecidable Theory ◽  
Classical Models ◽  
Classical Predicate

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC.Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not.Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

On the interpolation theorem for the logic of constant domains

1981 ◽  
Vol 46 (1) ◽  
pp. 87-88 ◽  
Author(s):  
E. G. K. López-Escobar
Keyword(s):  
Simple Proof ◽  
Open Problem ◽  
Formal System ◽  
Kripke Model ◽  
Interpolation Theorem ◽  
Predicate Calculus ◽  
Weak Consistency ◽  
Simple Matter ◽  
Constant Domains

In Gabbay [1] it is stated as an open problem whether or not Craig's Theorem holds for the logic of constant domains CD, i.e. for the extension of the intuitionistic predicate calculus, IPC, obtained by adding the schema; . Then in the later article, [2], Gabbay gives a proof of it. The proof given in [2] is via Robinson's (weak) consistency theorem and depends on relatively complicated (Kripke-) model-theoretical constructions developed in [1] (see p. 392 of [1] for a brief sketch of the method). The aim of this note is to show that the interpolation theorem for CD can also be obtained, by simple proof-theoretic methods, from §80 of Kleene's Introduction to Metamathematics [3].GI is the classical formal system whose postulates are given on p. 442 of [3]. Let GD be the system obtained from GI by the following modifications: (1) the sequents of GD are to have at most two formulas in their succedents and (2) the intuitionistic restriction that Θ be empty is required for the succedent rules (→ ¬) and (→ ⊃). It is a simple matter to show that: , x not free in . It then follows that, using Theorem 46 of [3], if then .

Equivalence between semantics for intuitionism. I

1981 ◽  
Vol 46 (4) ◽  
pp. 773-780 ◽  
Author(s):  
E. G. K. López-Escobar
Keyword(s):  
Formal Logic ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Axiom Schema ◽  
Formal Systems ◽  
Consistency Results ◽  
Partial List ◽  
Image Position ◽  
Constant Domains

It is probably because intuitionism is founded on the concept of (abstract) proof that it has been possible to develop various kinds of models. The following is but a partial list: Gabbay [5], Beth [2], Kripke [8], Kleene [7], Läuchli [9], McKinsey and Tarski [10], Rasiowa and Sikorski [14], Scott [15], de Swart [16], and Veldman [17].The original purpose for having the models appears to have been for obtaining independence or consistency results for certain formalizations of intuitionism [see Beth [2], Prawitz [13]]; of course, if the models could be also justified as being plausible interpretations of intuitionistic thinking, so much the better. In fact, having some kind of plausible interpretation makes it much easier to work with the models. Occasionally the models were used to suggest possible extensions of the formal systems; for example, the Kripke models with constant domains have motivated interest in the formal logic CD which extends the Intuitionistic Predicate Calculus (IPC) by having the axiom schema

Decidability of some intuitionistic predicate theories

1972 ◽  
Vol 37 (3) ◽  
pp. 579-587 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Reduction Method ◽  
Abelian Groups ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Classical Counterpart ◽  
First Order ◽  
Intuitionistic Theory ◽  
Classical Predicate

Suppose T is a first order intuitionistic theory (more precisely, a theory of Heyting's predicate calculus, e.g., abelian groups, one unary function, dense linear order, etc.) presented to us by a set of axioms (denoted also by) T.Question. Is T decidable?One knows that if the classical counterpart of T (i.e., take the same axioms but with the classical predicate calculus as the underlying logic) is not decidable, then T cannot be decidable. The problem remains for theories whose classical counterpart is decidable. In [8], sufficient conditions for undecidability were given, and several intuitionistic theories such as abelian groups and unary functions (both with decidable equality) were shown to be undecidable. In this note we show decidability results (see Theorems 1 and 2 below), and compare these results with the undecidability results previously obtained. The method we use is the reduction-method, described fully in [12] and widely applied in [3], which is applied here roughly as follows:Let T be a given theory of Heyting's predicate calculus. We know that Heyting's predicate calculus is complete for the Kripke-model type of semantics. We choose a class M of Kripke models for which T is complete, i.e., all axioms of T are valid in any model of the class and whenever φ is not a theorem of T, φ is false in some model of M.

Another intuitionistic completeness proof

1976 ◽  
Vol 41 (3) ◽  
pp. 644-662 ◽  
Author(s):  
H. De Swart
Keyword(s):  
Slight Modification ◽  
Kripke Model ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Single Model ◽  
Completeness Proof ◽  
Definition Of

In March 1973, W. Veldman [1] discovered that, by a slight modification of a Kripke-model, it was possible to give an intuitionistic proof of the completeness-theorem for the intuitionistic predicate calculus (IPC) with respect to modified Kripke models. The modification was the following: Let f represent absurdity, then we allow the possibility that and we agree that, for all sentences ϕ, , if . Just one modified Kripke model is constructed such that validity in implies derivability in IPC. While usually one thinks of as some subset of ⋃nNatn and of as the discrete natural ordering in ⋃nNatn, in Veldman's model , is a spread and , where Γα and Γβ are sets of sentences associated with α, resp. β, is a nondiscrete ordering.In the completeness-proofs, both for Beth and for Kripke models that we present here, we consider only models over ⋃nNatn, with the natural discrete ordering and we need validity in all models, not just in one, to get derivability in IPC. Also we have to modify the definition of a model in a somewhat different way than Veldman did. We agree that if ∨s[M⊨sf], then M⊨sϕ for each s ∈ ⋃nNatn and for each sentence ϕ.One can view a single model of the type constructed in [1] as the result of throwing together all the models of (the type constructed in) this paper into one big model, which has the somewhat strange properties mentioned above.

On the strong semantical completeness of the intuitionistic predicate calculus

1968 ◽  
Vol 33 (1) ◽  
pp. 1-7 ◽  
Author(s):  
Richmond H. Thomason
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
First Order ◽  
Semantic Tableaux ◽  
Weak Completeness ◽  
Skolem Theorem ◽  
Completeness Theorems

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

Finite Kripke models and predicate logics of provability

1990 ◽  
Vol 55 (3) ◽  
pp. 1090-1098 ◽  
Author(s):  
Sergei Artemov ◽  
Giorgie Dzhaparidze
Keyword(s):  
Modal Logic ◽  
Kripke Model ◽  
Finite Model ◽  
Kripke Models ◽  
Model Property ◽  
Logical Formula ◽  
Finite Model Property ◽  
Modal Predicate Logics ◽  
The One ◽  
Arithmetical Interpretation

AbstractThe paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic:If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR.This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.

Adding propositional connectives to countable infinitary logic

1975 ◽  
Vol 77 (1) ◽  
pp. 1-6
Author(s):  
Harvey Friedman
Keyword(s):  
Completeness Theorem ◽  
Predicate Calculus ◽  
Compactness Theorem ◽  
Functional Completeness ◽  
Infinitary Logic ◽  
Completeness Theorems ◽  
Infinite Sequences

AbstractFor countable admissible α, one can add a new infinitary propositional connective to so that the extended language obeys the Barwise compactness theorem, and the set of valid sentences is complete α-r.e.Aside from obeying the compactness theorem and a completeness theorem, ordinary finitary predicate calculus is also truth-functionally complete.In (1), Barwise shows that for countable admissible A, provides a fragment of which obeys a compactness theorem and a completeness theorem. However, we of course lose truth-functional completeness, with respect to infinitary propositional connectives that operate on infinite sequences of propositional variables. This raises the question of studying extensions of the language obtained by adding infinitary propositional connectives, in connexion with the Barwise compactness and completeness theorems, and other metatheorems, proved for Some aspects of this project are proposed in (3). It is the purpose of this paper to answer a few of the more basic questions which arise in this connexion.We have not attempted to study the preservation of interpolation or implicit definability. This could be quite interesting if done systematically.

Kripke models for linear logic

1993 ◽  
Vol 58 (2) ◽  
pp. 514-545 ◽  
Author(s):  
Gerard Allwein ◽  
J. Michael Dunn
Keyword(s):  
Representation Theorem ◽  
Linear Logic ◽  
Kripke Model ◽  
Relevance Logic ◽  
Distributive Lattices ◽  
Kripke Models ◽  
Binary Operations ◽  
Modal Algebras ◽  
Boolean Lattices ◽  
Gaggle Theory

AbstractWe present a Kripke model for Girard's Linear Logic (without exponentials) in a conservative fashion where the logical functors beyond the basic lattice operations may be added one by one without recourse to such things as negation. You can either have some logical functors or not as you choose. Commutativity and associativity are isolated in such a way that the base Kripke model is a model for noncommutative, nonassociative Linear Logic. We also extend the logic by adding a coimplication operator, similar to Curry's subtraction operator, which is residuated with Linear Logic's cotensor product. And we can add contraction to get nondistributive Relevance Logic. The model rests heavily on Urquhart's representation of nondistributive lattices and also on Dunn's Gaggle Theory. Indeed, the paper may be viewed as an investigation into nondistributive Gaggle Theory restricted to binary operations. The valuations on the Kripke model are three valued: true, false, and indifferent. The lattice representation theorem of Urquhart has the nice feature of yielding Priestley's representation theorem for distributive lattices if the original lattice happens to be distributive. Hence the representation is consistent with Stone's representation of distributive and Boolean lattices, and our semantics is consistent with the Lemmon-Scott representation of modal algebras and the Routley-Meyer semantics for Relevance Logic.

Sign in / Sign up

Export Citation Format

Share Document