The disjunction property of intermediate propositional logics

Alexander Chagrov; Michael Zakharyashchev

doi:10.1007/bf00370182

Some properties of epistemic set theory with collection

Journal of Symbolic Logic ◽

10.2307/2274028 ◽

1986 ◽

Vol 51 (3) ◽

pp. 748-754 ◽

Cited By ~ 1

Author(s):

Andre Scedrov

Keyword(s):

Set Theory ◽

Intuitionistic Logic ◽

Existential Quantifier ◽

Modal Interpretation ◽

Conservative Extension ◽

Disjunction Property ◽

First Order ◽

Slight Extension ◽

Order Arithmetic ◽

Epistemic Systems

Myhill [12] extended the ideas of Shapiro [15], and proposed a system of epistemic set theory IST (based on modal S4 logic) in which the meaning of the necessity operator is taken to be the intuitive provability, as formalized in the system itself. In this setting one works in classical logic, and yet it is possible to make distinctions usually associated with intuitionism, e.g. a constructive existential quantifier can be expressed as (∃x) □ …. This was first confirmed when Goodman [7] proved that Shapiro's epistemic first order arithmetic is conservative over intuitionistic first order arithmetic via an extension of Gödel's modal interpretation [6] of intuitionistic logic.Myhill showed that whenever a sentence □A ∨ □B is provable in IST, then A is provable in IST or B is provable in IST (the disjunction property), and that whenever a sentence ∃x.□A(x) is provable in IST, then so is A(t) for some closed term t (the existence property). He adapted the Friedman slash [4] to epistemic systems.Goodman [8] used Epistemic Replacement to formulate a ZF-like strengthening of IST, and proved that it was a conservative extension of ZF and that it had the disjunction and existence properties. It was then shown in [13] that a slight extension of Goodman's system with the Epistemic Foundation (ZFER, cf. §1) suffices to interpret intuitionistic ZF set theory with Replacement (ZFIR, [10]). This is obtained by extending Gödel's modal interpretation [6] of intuitionistic logic. ZFER still had the properties of Goodman's system mentioned above.

Download Full-text

The decidability of the Kreisel-Putnam system

Journal of Symbolic Logic ◽

10.2307/2270700 ◽

1970 ◽

Vol 35 (3) ◽

pp. 431-437 ◽

Cited By ~ 22

Author(s):

Dov M. Gabbay

Keyword(s):

Intuitionistic Logic ◽

Propositional Logic ◽

Finite Model ◽

Model Property ◽

Intuitionistic Propositional Logic ◽

Disjunction Property ◽

Finite Model Property ◽

Image Position

The intuitionistic propositional logic I has the following disjunction property This property does not characterize intuitionistic logic. For example Kreisel and Putnam [5] showed that the extension of I with the axiomhas the disjunction property. Another known system with this propery is due to Scott [5], and is obtained by adding to I the following axiom:In the present paper we shall prove, using methods originally introduced by Segerberg [10], that the Kreisel-Putnam logic is decidable. In fact we shall show that it has the finite model property, and since it is finitely axiomatizable, it is decidable by [4]. The decidability of Scott's system was proved by J. G. Anderson in his thesis in 1966.

Download Full-text

The disjunction and related properties for constructive Zermelo-Fraenkel set theory

Journal of Symbolic Logic ◽

10.2178/jsl/1129642124 ◽

2005 ◽

Vol 70 (4) ◽

pp. 1233-1254 ◽

Cited By ~ 16

Author(s):

Michael Rathjen

Keyword(s):

Set Theory ◽

Proof Technique ◽

Disjunction Property ◽

Regular Extension ◽

Existence Property ◽

Extension Axiom

AbstractThis paper proves that the disjunction property, the numerical existence property. Church's rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory, CZF, and also for the theory CZF augmented by the Regular Extension Axiom.As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.

Download Full-text

Finitely Presented Heyting Algebras

BRICS Report Series ◽

10.7146/brics.v5i30.19436 ◽

1998 ◽

Vol 5 (30) ◽

Cited By ~ 6

Author(s):

Carsten Butz

Keyword(s):

Simple Proof ◽

Heyting Algebra ◽

Distributive Lattices ◽

Heyting Algebras ◽

Model Property ◽

Disjunction Property ◽

Irreducible Elements ◽

Finite Set ◽

Finite Distributive Lattices ◽

Finitely Presented

In this paper we study the structure of finitely presented Heyting algebras. Using algebraic techniques (as opposed to techniques from proof-theory) we show that every such Heyting algebra is in fact co- Heyting, improving on a result of Ghilardi who showed that Heyting algebras free on a finite set of generators are co-Heyting. Along the way we give a new and simple proof of the finite model property. Our main technical tool is a representation of finitely presented Heyting algebras in terms of a colimit of finite distributive lattices. As applications we construct explicitly the minimal join-irreducible elements (the atoms) and the maximal join-irreducible elements of a finitely presented Heyting algebra in terms of a given presentation. This gives as well a new proof of the disjunction property for intuitionistic propositional logic. Unfortunately not very much is known about the structure of Heyting algebras, although it is understood that implication causes the complex structure of Heyting algebras. Just to name an example, the free Boolean algebra on one generator has four elements, the free Heyting algebra on one generator is infinite. Our research was motivated a simple application of Pitts' uniform interpolation theorem [11]. Combining it with the old analysis of Heyting algebras free on a finite set of generators by Urquhart [13] we get a faithful functor J : HAop f:p: ! PoSet; sending a finitely presented Heyting algebra to the partially ordered set of its join-irreducible elements, and a map between Heyting algebras to its leftadjoint restricted to join-irreducible elements. We will explore on the induced duality more detailed in [5]. Let us briefly browse through the contents of this paper: The first section recapitulates the basic notions, mainly that of the implicational degree of an element in a Heyting algebra. This is a notion relative to a given set of generators. In the next section we study nite Heyting algebras. Our contribution is a simple proof of the nite model property which names in particular a canonical family of nite Heyting algebras into which we can embed a given finitely presented one. In Section 3 we recapitulate the standard duality between nite distributive lattices and nite posets. The `new' feature here is a strict categorical formulation which helps simplifying some proofs and avoiding calculations. In the following section we recapitulate the description given by Ghilardi [8] on how to adjoin implications to a nite distributive lattice, thereby not destroying a given set of implications. This construction will be our major technical ingredient in Section 5 where we show that every nitely presented Heyting algebra is co-Heyting, i.e., that the operation (−) n (−) dual to implication is dened. This result improves on Ghilardi's [8] that this is true for Heyting algebras free on a finite set of generators. Then we go on analysing the structure of finitely presented Heyting algebras in Section 6. We show that every element can be expressed as a finite join of join-irreducibles, and calculate explicitly the maximal join-irreducible elements in such a Heyting algebra (in terms of a given presentation). As a consequence we give a new proof of the disjunction property for propositional intuitionistic logic. As well, we calculate the minimal join-irreducible elements, which are nothing but the atoms of the Heyting algebra. Finally, we show how all this material can be used to express the category of finitely presented Heyting algebras as a category of fractions of a certain category with objects morphism between finite distributive lattices.

Download Full-text

First steps in intuitionistic model theory

Journal of Symbolic Logic ◽

10.2307/2271944 ◽

1978 ◽

Vol 43 (1) ◽

pp. 3-12 ◽

Cited By ~ 3

Author(s):

H. de Swart

Keyword(s):

Model Theory ◽

Infinite Sequence ◽

Finite Sequence ◽

Kripke Models ◽

Disjunction Property ◽

Completeness Proof ◽

New Model ◽

Continuity Principle ◽

Countably Infinite

In this paper we will do some model theory with respect to the models, defined in [7] and, as in [7], we will work again in intuitionistic metamathematics.In this paper we will only consider models M = ‹S, TM›, where S is one fixed spreadlaw for all models M, namely the universal spreadlaw. That we can restrict ourselves to this class of models is a consequence of the completeness proof, which is sketched in [7, §3].The main tools in this paper will be two model-constructions:(i) In §1 we will consider, under a certain condition C(M0, M, s), the construction of a model R(M0, M, s) from two models M0 and M with respect to the finite sequence s.(ii) In §2 we will construct from an infinite sequence M0, M1, M2, … of models a new model Σi∈INMi.Syntactic proofs of the disjunction property and the explicit definability theorem are well known.C. Smorynski [8] gave semantic proofs of these theorems with respect to Kripke models, however using classical metamathematics. In §1 we will give intuitionistically correct, semantic proofs with respect to the models, defined in [7] using Brouwer's continuity principle.Let W be the fan of all models (see [7, Theorem 2.7]) and let Γ be a countably infinite sequence of sentences.

Download Full-text