With any structural inference rule A/B, we associate the rule $${(A \lor p)/(B \lor p)}$$, providing that formulas A and B do not contain the variable p. We call the latter rule a join-extension ( $${\lor}$$ -extension, for short) of the former. Obviously, for any intermediate logic with disjunction property, a $${\lor}$$ -extension of any admissible rule is also admissible in this logic. We investigate intermediate logics, in which the $${\lor}$$ -extension of each admissible rule is admissible. (...) We prove that any structural finitary consequence operator (for intermediate logic) can be defined by a set of $${\lor}$$ -extended rules if and only if it can be defined through a set of well-connected Heyting algebras of a corresponding quasivariety. As we exemplify, the latter condition is satisfied for a broad class of algebraizable logics. (shrink)

The goal of this paper is to generalize a notion of characteristic (or Jankov) formula by using finite partial Heyting algebras instead of the finite subdirectly irreducible algebras: with every finite partial Heyting algebra we associate a characteristic formula, and we study the properties of these formulas. We prove that any intermediate logic can be axiomatized by such formulas. We further discuss the correlations between characteristic formulas of finite partial algebras and canonical formulas. Then with every (...) well-connected Heyting algebra we associate a set of characteristic formulas that correspond to each finite relative subalgebra of this algebra. Finally, we demonstrate that in many respects these sets enjoy the same properties as regular characteristic formulas. In the last section we outline an approach how to generalize these obtained results to the broad classes of algebras. (shrink)

This article provides an algebraic study of the propositional system $\mathtt {InqB}$ of inquisitive logic. We also investigate the wider class of $\mathtt {DNA}$ -logics, which are negative variants of intermediate logics, and the corresponding algebraic structures, $\mathtt {DNA}$ -varieties. We prove that the lattice of $\mathtt {DNA}$ -logics is dually isomorphic to the lattice of $\mathtt {DNA}$ -varieties. We characterise maximal and minimal intermediate logics with the same negative variant, and we prove a suitable version (...) of Birkhoff’s classic variety theorems. We also introduce locally finite $\mathtt {DNA}$ -varieties and show that these varieties are axiomatised by the analogues of Jankov formulas. Finally, we prove that the lattice of extensions of $\mathtt {InqB}$ is dually isomorphic to the ordinal $\omega +1$ and give an axiomatisation of these logics via Jankov $\mathtt {DNA}$ -formulas. This shows that these extensions coincide with the so-called inquisitive hierarchy of [9].1. (shrink)

Journal of Mathematical Logic, Volume 22, Issue 03, December 2022. In this paper, we show that there exist (continuum many) varieties of bi-Heyting algebras that are not generated by their complete members. It follows that there exist (continuum many) extensions of the Heyting–Brouwer logic [math] that are topologically incomplete. This result provides further insight into the long-standing open problem of Kuznetsov by yielding a negative solution of the reformulation of the problem from extensions of [math] to extensions (...) of [math]. (shrink)

A partial solution to Ono’s problem P54 is given. Here Ono’s problem P54 is whether Harrop disjunction property is equivalent to disjunction property or not in intermediate predicate logics. As an application of this result it is shown that some intermediate predicate logics satisfy Harrop disjunction property.

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

For intermediate logics, there is obtained in the paper an algebraic equivalent of the disjunction propertyDP. It is proved that the logic of finite binary trees is not maximal among intermediate logics withDP. Introduced is a logicND, which has the only maximal extension withDP, namely, the logicML of finite problems.

The variety of Heyting algebras has two well-behaved locally finite reducts, the variety of bounded distributive lattices and the variety of implicative semilattices. The variety of bounded distributive lattices is generated by the →-free reducts of Heyting algebras, while the variety of implicative semilattices is generated by the ∨-free reducts. Each of these reducts gives rise to canonical formulas that generalize Jankov formulas and provide an axiomatization of all superintuitionistic logics. The ∨-free reducts of Heyting algebras (...) give rise to the -canonical formulas that we studied in an earlier work. Here we introduce the -canonical formulas, which are obtained from the study of the →-free reducts of Heyting algebras. We prove that every si-logic is axiomatizable by -canonical formulas. We also discuss the similarities and differences between these two kinds of canonical formulas. One of the main ingredients of these formulas is a designated subset D of pairs of elements of a finite subdirectly irreducible Heyting algebra A. When D=A2, we show that the -canonical formula of A is equivalent to the Jankov formula of A. On the other hand, when D=∅, the -canonical formulas produce a new class of si-logics we term stable si-logics. We prove that there are continuum many stable si-logics and that all stable si-logics have the finite model property. We also compare stable si-logics to splitting and subframe si-logics. (shrink)

With each superintuitionistic propositional logic L with a disjunction property we associate a set of modal logics the assertoric fragment of which is L . Each formula of these modal logics is interdeducible with a formula representing a set of rules admissible in L . The smallest of these logics contains only formulas representing derivable in L rules while the greatest one contains formulas corresponding to all admissible in L rules. The algebraic semantic for these logics is described.

This paper deals with the varieties of monadic Heyting algebras, algebraic models of intuitionistic modal logic MIPC. We investigate semisimple, locally finite, finitely approximated and splitting varieties of monadic Heyting algebras as well as varieties with the disjunction and the existence properties. The investigation of monadic Heyting algebras clarifies the correspondence between intuitionistic modal logics over MIPC and superintuitionistic predicate logics and provides us with the solutions of several problems raised by Ono [35].

We study axiomatic extensions of the propositional constructive logic with strong negation having the disjunction property in terms of corresponding to them varieties of Nelson algebras. Any such varietyV is characterized by the property: (PQWC) ifA,B V, thenA×B is a homomorphic image of some well-connected algebra ofV.We prove:• each varietyV of Nelson algebras with PQWC lies in the fibre –1(W) for some varietyW of Heyting algebras having PQWC, • for any varietyW of Heyting algebras with PQWC the (...) least and the greatest varieties in –1(W) have PQWC, • there exist varietiesW of Heyting algebras having PQWC such that –1(W) contains infinitely many varieties (of Nelson algebras) with PQWC. (shrink)

The aim of this paper is to look from the point of view of admissibility of inference rules at intermediate logics having the finite model property which extend Heyting's intuitionistic propositional logic H. A semantic description for logics with the finite model property preserving all admissible inference rules for H is given. It is shown that there are continuously many logics of this kind. Three special tabular intermediate logics λ, 1 ≥ i ≥ 3, are given which (...) describe all tabular logics preserving admissibility: a tabular logic λ preserves all admissible rules for H iff 7λ has width not more than 2 and is not included in each λ. MSC: 03B55, 03B20. (shrink)

In this paper we consider the class of truth-functional modal many-valued logics with the complete lattice of truth-values. The conjunction and disjunction logic operators correspond to the meet and join operators of the lattices, while the negation is independently introduced as a hierarchy of antitonic operators which invert bottom and top elements. The non-constructive logic implication will be defined for a subclass of modular lattices, while the constructive implication for distributive lattices (Heyting algebras) is based on relative pseudo-complements (...) as in intuitionistic logic. We show that the complete lattices are intrinsically modal, with banal identity modal operator. We define the autoreferential set-based representation for the class of modal algebras, and show that the autoreferential Kripke-style semantics for this class of modal algebras is based on the set of possible worlds equal to the complete lattice of algebraic truth-values. The philosophical assumption is based on the consideration that each possible world represents a level of credibility, so that only propositions with the right logic value (i.e., level of credibility) can be accepted by this world, then we connect it with paraconsistent properties and LFI logics. The bottom truth value in this complete lattice corresponds to the trivial world in which each formula is satisfied, that is, to the world with explosive inconsistency. The top truth value corresponds to the world with classical logics, while all intermediate possible worlds represent the different levels of paraconsistent logics. (shrink)

We give an example of a variety of Heyting algebras and of a splitting algebra in this variety that is not finitely presentable. Moreover, we show that the corresponding splitting pair cannot be defined by any finitely presentable algebra. Also, using the Gödel-McKinsey-Tarski translation and the Blok-Esakia theorem, we construct a variety of Grzegorczyk algebras with similar properties.

This paper is a survey of results concerning the disjunction property, Halldén-completeness, and other related properties of intermediate prepositional logics and normal modal logics containing S4.

In Coecke (2002) we proposed the intuitionistic or disjunctive representation of quantum logic, i.e., a representation of the property lattice of physical systems as a complete Heyting algebra of logical propositions on these properties, where this complete Heyting algebra goes equipped with an additional operation, the operational resolution, which identifies the properties within the logic of propositions. This representation has an important application towards dynamic quantum logic, namely in describing the temporal indeterministic propagation of actual properties of physical (...) systems. This paper can as such by conceived as an addendum to Quantum Logic in Intuitionistic Perspective that discusses spin-off and thus provides an additional motivation. We derive a quantaloidal semantics for dynamic disjunctive quantum logic and illustrate it for the particular case of a perfect (quantum) measurement. (shrink)

Some of the basic substructural logics are shown by Ono to have the disjunction property (DP) by using cut elimination of sequent calculi for these logics. On the other hand, this syntactic method works only for a limited number of substructural logics. Here we show that Maksimova's criterion on the DP of superintuitionistic logics can be naturally extended to one on the DP of substructural logics over FL. By using this, we show the DP for some of the substructural (...) logics for which syntactic methods don't work well. (shrink)

In this paper, we will study Heyting algebras endowed with tense negative operators, which we call tense H-algebras and we proof that these algebras are the algebraic semantics of the Intuitionistic Propositional Logic with Galois Negations. Finally, we will develop a Priestley-style duality for tense H-algebras.

In classical logic, the proposition expressed by a sentence is construed as a set of possible worlds, capturing the informative content of the sentence. However, sentences in natural language are not only used to provide information, but also to request information. Thus, natural language semantics requires a logical framework whose notion of meaning does not only embody informative content, but also inquisitive content. This paper develops the algebraic foundations for such a framework. We argue that propositions, in order to embody (...) both informative and inquisitive content in a satisfactory way, should be defined as non-empty, downward closed sets of possibilities, where each possibility in turn is a set of possible worlds. We define a natural entailment order over such propositions, capturing when one proposition is at least as informative and inquisitive as another, and we show that this entailment order gives rise to a complete Heyting algebra, with meet, join, and relative pseudo-complement operators. Just as in classical logic, these semantic operators are then associated with the logical constants in a first-order language. We explore the logical properties of the resulting system and discuss its significance for natural language semantics. We show that the system essentially coincides with the simplest and most well-understood existing implementation of inquisitive semantics, and that its treatment of disjunction and existentials also concurs with recent work in alternative semantics. Thus, our algebraic considerations do not lead to a wholly new treatment of the logical constants, but rather provide more solid foundations for some of the existing proposals. (shrink)

In this paper it is shown that there exist a structural complete interme- diate logics with the disjunction property, which was previously conjectured by H. Friedman. The intermedi.

Two algebraic structures, the contrapositionally complemented Heyting algebra (ccHa) and the contrapositionally |$\vee $| complemented Heyting algebra (c|$\vee $|cHa), are studied. The salient feature of these algebras is that there are two negations, one intuitionistic and another minimal in nature, along with a condition connecting the two operators. Properties of these algebras are discussed, examples are given and comparisons are made with relevant algebras. Intuitionistic Logic with Minimal Negation (ILM) corresponding to ccHas and its extension |${\textrm {ILM}}$|-|${\vee }$| (...) for c|$\vee $|cHas are then investigated. Besides its relations with intuitionistic and minimal logics, ILM is observed to be related to Peirce’s logic and Vakarelov’s logic MIN. With a focus on properties of the two negations, relational semantics for ILM and |${\textrm {ILM}}$|-|${\vee }$| are obtained with respect to four classes of frames, and inter-translations between the classes preserving truth and validity are provided. ILM and |${\textrm {ILM}}$|-|${\vee }$| are shown to have the finite model property with respect to these classes of frames and proved to be decidable. Extracting features of the two negations in the algebras, a further investigation is made, following logical studies of negations that define the operators independently of the binary operator of implication. Using Dunn’s logical framework for the purpose, two logics |$K_{im}$| and |$K_{im-{\vee }}$| are discussed, where the language does not include implication. The |$K_{im}$|-algebras are reducts of ccHas and are different from relevant algebraic structures having two negations. The negations in the |$K_{im}$|-algebras and |$K_{im-{\vee }}$|-algebras are shown to occupy distinct positions in an enhanced form of Dunn’s kite of negations. Relational semantics for |$K_{im}$| and |$K_{im-{\vee }}$| is provided by a class of frames that are based on Dunn’s compatibility frames. It is observed that this class coincides with one of the four classes giving the relational semantics for ILM and |${\textrm {ILM}}$|-|${\vee }$|⁠. (shrink)

We introduce the concept of a connected logic (over S4) and show that each connected logic with the finite model property is the logic of a subalgebra of the closure algebra of all subsets of the real line R, thus generalizing the McKinsey-Tarski theorem. As a consequence, we obtain that each intermediate logic with the finite model property is the logic of a subalgebra of the Heyting algebra of all open subsets of R.

We discuss relationships among the existence property, the disjunction property, and their weak variants in the setting of intermediate predicate logics. We deal with the weak and sentential existence properties, and the Z-normality, which is a weak variant of the disjunction property. These weak variants were presented in the author’s previous paper [16]. In the present paper, the Kripke sheaf semantics is used.

We give a systematic method of constructing extensions of the Kuznetsov-Gerčiu logic KG without the finite model property (fmp for short), and show that there are continuum many such. We also introduce a new technique of gluing of cyclic intuitionistic descriptive frames and give a new simple proof of Gerčiu’s result [9, 8] that all extensions of the Rieger-Nishimura logic RN have the fmp. Moreover, we show that each extension of RN has the poly-size model property, thus improving on [9]. (...) Furthermore, for each function f: omega -> omega, we construct an extension Lf of KG such that Lf has the fmp, but does not have the f-size model property. We also give a new simple proof of another result of Gerčiu [9] characterizing the only extension of KG that bounds the fmp for extensions of KG. We conclude the paper by proving that RN.KC = RN + (¬p vee ¬¬p) is the only pre-locally tabular extension of KG, introduce the internal depth of an extension L of RN, and show that L is locally tabular if and only if the internal depth of L is finite. (shrink)

We provide results allowing to state, by the simple inspection of suitable classes of posets , that the corresponding intermediate propositional logics are maximal among the ones which satisfy the disjunction property. Starting from these results, we directly exhibit, without using the axiom of choice, the Kripke frames semantics of 2No maximal intermediate propositional logics with the disjunction property. This improves previous evaluations, giving rise to the same conclusion but made with an essential use of the (...) axiom of choice, of the cardinality of the set of the maximal intermediate propositional logics with the disjunction property. (shrink)

In this paper we shall prove that certain subvarieties of the variety of Salgebras (Heyting algebras with successor) has amalgamation. This result together with an appropriate version of Theorem 1 of [L. L. Maksimova, Craig’s theorem in superintuitionistic logics and amalgamable varieties of pseudo-boolean algebras, Algebra i Logika, 16(6):643-681, 1977] allows us to show interpolation in the calculus IPC S (n), associated with these varieties.We use that every algebra in any of the varieties of S-algebras studied in this work (...) has a canonical extension, to show completeness of the calculus IPC S (n) with respect to appropriate Kripke models. (shrink)

Hamkins and Löwe proved that the modal logic of forcing is S4.2 . In this paper, we consider its modal companion, the intermediate logic KC and relate it to the fatal Heyting algebra H ZFC of forcing persistent sentences. This Heyting algebra is equationally generic for the class of fatal Heyting algebras. Motivated by these results, we further analyse the class of fatal Heyting algebras.

Many intermediate logics, even extremely well-behaved ones such as IPC, lack the finite model property for admissible rules. We give conditions under which this failure holds. We show that frames which validate all admissible rules necessarily satisfy a certain closure condition, and we prove that this condition, in the finite case, ensures that the frame is of width 2. Finally, we indicate how this result is related to some classical results on finite, free Heyting algebras.

The one-variable fragment of a first-order logic may be viewed as an “S5-like” modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases—notably, the modal counterparts $\mathrm {S5}$ and $\mathrm {MIPC}$ of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively—but a general approach, extending beyond first-order intermediate logics, has been lacking. To this end, a sufficient criterion is given (...) in this paper for the one-variable fragment of a semantically defined first-order logic—spanning families of intermediate, substructural, many-valued, and modal logics—to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property. (shrink)

A Q -Heyting algebra is an algebra of type such that is a Heyting algebra and the unary operation ∇ satisfies the conditions ∇0=0, a ∧∇ a = a , ∇=∇ a ∧∇ b and ∇=∇ a ∨∇ b , for any a , b ∈ H . This paper is devoted to the study of the subvariety QH L of linear Q -Heyting algebras. Using Priestley duality we investigate the subdirectly irreducible linear Q -Heyting algebras (...) and, as consequences, we derive some properties of the lattice of subvarieties of QH L and find equational bases for some of these subvarieties. (shrink)

Infinitely many intermediate propositional logics with the disjunction property are defined, each logic being characterized both in terms of a finite axiomatization and in terms of a Kripke semantics with the finite model property. The completeness theorems are used to prove that any two logics are constructively incompatible. As a consequence, one deduces that there are infinitely many maximal intermediate propositional logics with the disjunction property.

A Heyting algebra is supplemented if each element a has a dual pseudo-complement \, and a Heyting algebra is centrally supplement if it is supplemented and each supplement is central. We show that each Heyting algebra has a centrally supplemented extension in the same variety of Heyting algebras as the original. We use this tool to investigate a new type of completion of Heyting algebras arising in the context of algebraic proof theory, the so-called hyper-MacNeille (...) completion. We show that the hyper-MacNeille completion of a Heyting algebra is the MacNeille completion of its centrally supplemented extension. This provides an algebraic description of the hyper-MacNeille completion of a Heyting algebra, allows development of further properties of the hyper-MacNeille completion, and provides new examples of varieties of Heyting algebras that are closed under hyper-MacNeille completions. In particular, connections between the centrally supplemented extension and Boolean products allow us to show that any finitely generated variety of Heyting algebras is closed under hyper-MacNeille completions. (shrink)

We study some operations that may be defined using the minimum operator in the context of a Heyting algebra. Our motivation comes from the fact that 1) already known compatible operations, such as the successor by Kuznetsov, the minimum dense by Smetanich and the operation G by Gabbay may be defined in this way, though almost never explicitly noted in the literature; 2) defining operations in this way is equivalent, from a logical point of view, to two clauses, one (...) corresponding to an introduction rule and the other to an elimination rule, thus providing a manageable way to deal with these operations. Our main result is negative: all operations that arise turn out to be Heyting terms or the mentioned already known operations or operations interdefinable with them. However, it should be noted that some of the operations that arise may exist even if the known operations do not. We also study the extension of Priestley duality to Heyting algebras enriched with the new operations. (shrink)

\(\nabla \) -algebra is a natural generalization of Heyting algebra, unifying many algebraic structures including bounded lattices, Heyting algebras, temporal Heyting algebras and the algebraic presentation of the dynamic topological systems. In a series of two papers, we will systematically study the algebro-topological properties of different varieties of \(\nabla \) -algebras. In the present paper, we start with investigating the structure of these varieties by characterizing their subdirectly irreducible and simple elements. Then, we prove the closure of (...) these varieties under the Dedekind-MacNeille completion and provide the canonical construction and the Kripke representation for \(\nabla \) -algebras by which we establish the amalgamation property for some varieties of \(\nabla \) -algebras. In the sequel of the present paper, we will complete the study by covering the logics of these varieties and their corresponding Priestley-Esakia and spectral duality theories. (shrink)

We use the left self‐distributive axiom to introduce and study a special class of weak Heyting algebras, called self‐distributive weak Heyting algebras (SDWH‐algebras). We present some useful properties of SDWH‐algebras and obtain some equivalent conditions of them. A characteristic of SDWH‐algebras of orders 3 and 4 is given. Finally, we study the relation between the variety of SDWH‐algebras and some of the known subvarieties of weak Heyting algebras such as the variety of Heyting algebras, the variety (...) of basic algebras, the variety of subresiduated lattices, the variety of reflexive WH‐algebras (RWH‐algebras), and the variety of transitive WH‐algebras (TWH‐algebras). (shrink)

The aim of this paper is to give, using the Kripke semantics for intuitionism, a representation of finitely generated free Heyting algebras. By means of the representation we determine in a constructive way some set of "special elements" of such algebras. Furthermore, we show that many algebraic properties which are satisfied by the free algebra on one generator are not satisfied by free algebras on more than one generator.

We investigate degree of satisfiability questions in the context of Heyting algebras and intuitionistic logic. We classify all equations in one free variable with respect to finite satisfiability gap, and determine which common principles of classical logic in multiple free variables have finite satisfiability gap. In particular we prove that, in a finite non-Boolean Heyting algebra, the probability that a randomly chosen element satisfies $x \vee \neg x = \top $ is no larger than $\frac {2}{3}$. Finally, we (...) generalize our results to infinite Heyting algebras, and present their applications to point-set topology, black-box algebras, and the philosophy of logic. (shrink)

We investigate a recently devised polyhedral semantics for intermediate logics, in which formulas are interpreted in n-dimensional polyhedra. An intermediate logic is polyhedrally complete if it is complete with respect to some class of polyhedra. The first main result of this paper is a necessary and sufficient condition for the polyhedral completeness of a logic. This condition, which we call the Nerve Criterion, is expressed in terms of Alexandrov’s notion of the nerve of a poset. It affords a (...) purely combinatorial characterisation of polyhedrally complete logics. Using the Nerve Criterion we show, easily, that there are continuum many intermediate logics that are not polyhedrally complete but which have the finite model property. We also provide, at considerable combinatorial labour, a countably infinite class of logics axiomatised by the Jankov–Fine formulas of ‘starlike trees’ all of which are polyhedrally complete. The polyhedral completeness theorem for these ‘starlike logics’ is the second main result of this paper. (shrink)

We characterise the intermediate logics which admit a cut-free hypersequent calculus of the form \, where \ is the hypersequent counterpart of the sequent calculus \ for propositional intuitionistic logic, and \ is a set of so-called structural hypersequent rules, i.e., rules not involving any logical connectives. The characterisation of this class of intermediate logics is presented both in terms of the algebraic and the relational semantics for intermediate logics. We discuss various—positive as well as negative—consequences (...) of this characterisation. (shrink)

Roelcke non-precompactness, simplicity, and non-amenability of the automorphism group of the Fraïssé limit of finite Heyting algebras are proved among others.

This is the first part of a paper concerning intermediate propositional logics with the disjunction property which cannot be properly extended into logics of the same kind, and are therefore called maximal. To deal with these logics, we use a method based on the search of suitable nonstandard logics, which has an heuristic content and has allowed us to discover a wide family of logics, as well as to get their maximality proofs in a uniform way. The present (...) part illustrates infinitely many maximal logics with the disjunction property extending the well-known logic of Scott, and aims to provide a first picture of the method, sufficient for the reader who wish to achieve an overall understanding of it without entering into the further aspects developed in the second part. From this point of view, the latter will not be self-standing, but will be seen as a prosecution and a complement of the former, with the aim that the material presented in the whole paper can be used as a starting point for a classification of the subject. (shrink)

We study finitely generated free Heyting algebras from a topological and from a model theoretic point of view. We review Bellissima’s representation of the finitely generated free Heyting algebra; we prove that it yields an embedding in the profinite completion, which is also the completion with respect to a naturally defined metric. We give an algebraic interpretation of the Kripke model used by Bellissima as the principal ideal spectrum and show it to be first order interpretable in the (...) Heyting algebra, from which several model theoretic and algebraic properties are derived. In particular, we prove that a free finitely generated Heyting algebra has only one set of free generators, which is definable in it. As a consequence its automorphism group is the permutation group over its generators. (shrink)

We study some operations that may be defined using the minimum operator in the context of a Heyting algebra. Our motivation comes from the fact that 1) already known compatible operations, such as the successor by Kuznetsov, the minimum dense by Smetanich and the operation G by Gabbay may be defined in this way, though almost never explicitly noted in the literature; 2) defining operations in this way is equivalent, from a logical point of view, to two clauses, one (...) corresponding to an introduction rule and the other to an elimination rule, thus providing a manageable way to deal with these operations. Our main result is negative: all operations that arise turn out to be Heyting terms or the mentioned already known operations or operations interdefinable with them. However, it should be noted that some of the operations that arise may exist even if the known operations do not. We also study the extension of Priestley duality to Heyting algebras enriched with the new operations. (shrink)

It was shown recently that epimorphisms need not be surjective in a variety K of Heyting algebras, but only one counter-example was exhibited in the literature until now. Here, a continuum of such examples is identified, viz. the variety generated by the Rieger-Nishimura lattice, and all of its (locally finite) subvarieties that contain the original counter-example K . It is known that, whenever a variety of Heyting algebras has finite depth, then it has surjective epimorphisms. In contrast, we (...) show that for every integer $n \geq 2$ , the variety of all Heyting algebras of width at most n has a non-surjective epimorphism. Within the so-called Kuznetsov-Gerčiu variety (i.e., the variety generated by finite linear sums of one-generated Heyting algebras), we describe exactly the subvarieties that have surjective epimorphisms. This yields new positive examples, and an alternative proof of epimorphism surjectivity for all varieties of Gödel algebras. The results settle natural questions about Beth-style definability for a range of intermediate logics. (shrink)

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such (...) that for all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

This paper presents an algebraic framework for investigating proposed translations of classical logic into intuitionistic logic, such as the four negative translations introduced by Kolmogorov, Gödel, Gentzen and Glivenko. We view these asvariant semanticsand present a semantic formulation of Troelstra’s syntactic criteria for a satisfactory negative translation. We consider how each of the above-mentioned translation schemes behaves on two generalisations of Heyting algebras: bounded pocrims and bounded hoops. When a translation fails for a particular class of algebras, (...) we demonstrate that failure via specific finite examples. Using these, we prove that the syntactic version of these translations will fail to satisfy Troelstra’s criteria in the corresponding substructural logical setting. (shrink)

This is the second part of a paper devoted to the study of the maximal intermediate propositional logics with the disjunction property , whose first part has appeared in this journal with the title “A method to single out maximal propositional logics with the disjunction property I”. In the first part we have explained the general results upon which a method to single out maximal constructive logics is based and have illustrated such a method by exhibiting the (...) Kripke semantics of maximal constructive logics extending the logic ST of Scott, for which, in turn, a semantical characterization in terms of Kripke frames has been given. In the present part we complete the illustration of the method of the first part, having in mind some aspects which might be interesting for a classification of the maximal constructive logics, and an application of the heuristic content of the method to detect the nonmaximality of apparently maximal constructive logics. Thus, on the one hand we introduce the logic AST , which is compared with ST and is seen as a logic “alternative” to it, in a sense which will be precisely explained. We provide a Kripke semantics for AST and show that there are maximal constructive logics which neither are extensions of ST nor are extensions of AST. Finally, we give a further application of the results of the first part by exhibiting the Kripke semantics of a maximal constructive logic extending AST. On the other hand, we compare the maximal constructive logics presented in both parts of the paper with a constructive logic introduced by Maksimova , which has been conjectured to be maximal by Chagrov and Zacharyashchev ; from this comparison a disproof of the conjecture arises. (shrink)