In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication $\phi \rightarrow \psi $ with no interpolant. Importantly, this result does not contradict the unfortunately named ‘Craig interpolation’ theorem established by Rauszer in [24] since that article is about the property (...) more correctly named ‘deductive interpolation’ (see Galatos, Jipsen, Kowalski and Ono’s use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent. (shrink)

In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can (...) be regarded as a bi-intuitionistic variant of the original classical multilattice logic determined by the algebraic structure of multilattices. Similar completeness and embedding results are also shown for another logic called bi-intuitionistic connexive multilattice logic, obtained by replacing the connectives of intuitionistic implication and co-implication with their connexive variants. (shrink)

We define notions of homomorphism, submodel, and sandwich of Kripke models, and we define two syntactic operators analogous to universal and existential closure. Then we prove an intuitionistic analogue of the generalized (dual of the) Lyndon-Łoś-Tarski Theorem, which characterizes the sentences preserved under inverse images of homomorphisms of Kripke models, an intuitionistic analogue of the generalized Łoś-Tarski Theorem, which characterizes the sentences preserved under submodels of Kripke models, and an intuitionistic analogue of the generalized Keisler Sandwich Theorem, (...) which characterizes the sentences preserved under sandwiches of Kripke models. We also define several intuitionistic formula hierarchies analogous to the classical formula hierarchies $\forall_n (= \Pi^0_n)$ and $\exists_n (=\Sigma^0_n)$ , and we show how our generalized syntactic preservation theorems specialize to these hierarchies. Each of these theorems implies the corresponding classical theorem in the case where the Kripke models force classical logic. (shrink)

Craig interpolation theorem implies that the derivability of X,X′ Y′ implies existence of an interpolant I in the common language of X and X′ Y′ such that both X I and I,X′ Y′ are derivable. For classical logic this extends to X,X′ Y,Y′, but for intuitionistic logic there are counterexamples. We present a version true for intuitionistic propositional logic, and more complicated version for the predicate case.

Basic Predicate Logic, BQC, is a proper subsystem of Intuitionistic Predicate Logic, IQC. For every formula in the language {, , , , , , }, we associate two sequences of formulas 0,1,... and 0,1,... in the same language. We prove that for every sequent , there are natural numbers m, n, such that IQC , iff BQC n m. Some applications of this translation are mentioned.

One criterion of constructive logics is the disjunction, property (DP). The Halldén-completeness is a weak DP, and is related to the relevance principle and variable separation. This concept is well-understood in the case of propositional logics. We extend this notion to predicate logics. Then three counterparts naturally arise. We discuss relationships between these properties and meet-irreducibility in the lattice of logics.

The main part of the proof of Kripke's completeness theorem for intuitionistic logic is Henkin's construction. We introduce a new Kripke-type semantics with semilattice structures for intuitionistic logic. The completeness theorem for this semantics can he proved without Henkin's construction.

One criterion of constructive logics is the disjunction, property (DP). The Halldén-completeness is a weak DP, and is related to the relevance principle and variable separation. This concept is well-understood in the case of propositional logics. We extend this notion to predicate logics. Then three counterparts naturally arise. We discuss relationships between these properties and meet-irreducibility in the lattice of logics.

Some properties of Kripke-sheaf semantics for super-intuitionistic predicate logics are shown. The concept ofp-morphisms between Kripke sheaves is introduced. It is shown that if there exists ap-morphism from a Kripke sheaf 1 into 2 then the logic characterized by 1 is contained in the logic characterized by 2. Examples of Kripke-sheaf complete and finitely axiomatizable super-intuitionistic (and intermediate) predicate logics each of which is Kripke-frame incomplete are given. A correction to the author's previous paper (...) Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics (Studia Logica, 49(1990), pp. 289–306 ) is stated. (shrink)

In this paper, we introduce the notions of connexive and bi-intuitionistic multilattices and develop on their base the algebraic semantics for Kamide, Shramko, and Wansing’s connexive and bi-intuitionistic multilattice logics which were previously known in the form of sequent calculi and Kripke semantics. We prove that these logics are sound and complete with respect to the presented algebraic structures.

Using the framework of categorical logic, this paper analyzes and streamlines Gabbay's semantical proof of the Craig interpolation theorem for intuitionistic predicate logic. In the process, an apparently new and interesting fact about the relation of coherent and intuitionistic logic is found.

Bi-intuitionistic logic is the result of adding the dual of intuitionistic implication to intuitionistic logic. In this note, we characterize the expressive power of this logic by showing that the first order formulas equivalent to translations of bi-intuitionistic propositional formulas are exactly those preserved under bi-intuitionistic directed bisimulations. The proof technique is originally due to Lindstrom and, in contrast to the most common proofs of this kind of result, it does not use (...) the machinery of neither saturated models nor elementary chains. (shrink)

In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.

The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of (...) bilateralist reasoning, since they do not only internalize processes of verifcation or provability but also the dual processes in terms of falsifcation or what is called dual provability. In [Wansing, 2017] a normal form theorem for N2Int is stated, here, I want to prove a cut-elimination theorem for SC2Int, i.e., if successful, this would extend the results existing so far. (shrink)

The well-known algebraic semantics and topological semantics for intuitionistic logic (Int) is here extended to Wansing's bi-intuitionistic logic (2Int). The logic 2Int is also characterised by a quasi-twist structure semantics, which leads to an alternative topological characterisation of 2Int. Later, notions of Fregean negation and of unilateralisation are proposed. The logic 2Int is extended with a ‘Fregean negation’ connective ∼, obtaining 2Int∼, and it is showed that the logic N4⋆ (an extension of Nelson's (...) paraconsistent logic) results to be the unilateralisation of 2Int∼ via ∼. The logic 2Int∼ is also characterised by a Kripke-style semantics, a twist structure semantics and a topological semantics. (shrink)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, (...) without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)

In this contribution, we will present some results concerning the connectives of bi-intuitionistic logic in the setting of Arnold Koslow’s implication structures. Furthermore, we will present soundness and completeness results of Koslow’s implication structures with respect to bi-intuitionistic logic.

We present a multiple-assumption multiple-conclusion system for bi-intuitionistic logic. Derivations in the systems are graphs whose edges are labelled by formulas and whose nodes are labelled by rules. We show how to embed both the standard intuitionistic and dual-intuitionistic natural deduction systems into the proposed system. Soundness and completeness are established using translations with more traditional sequent calculi for bi-intuitionistic logic.

Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual (...) class='Hi'>intuitionistic exclusion, similarly to future and past modalities in tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose. (shrink)

Intuitionistic propositional logic with Galois negations ( \(\mathsf {IGN}\) ) is introduced. Heyting algebras with Galois negations are obtained from Heyting algebras by adding the Galois pair \((\lnot,{\sim })\) and dual Galois pair \((\dot{\lnot },\dot{\sim })\) of negations. Discrete duality between GN-frames and algebras as well as the relational semantics for \(\mathsf {IGN}\) are developed. A Hilbert-style axiomatic system \(\mathsf {HN}\) is given for \(\mathsf {IGN}\), and Galois negation logics are defined as extensions of \(\mathsf {IGN}\). We give (...) the bi-tense logic \(\mathsf {S4N}_t\) which is obtained from the minimal tense extension of the modal logic \(\mathsf {S4}\) by adding tense operators. We give a new extended Gödel translation \(\tau \) and prove that \(\mathsf {IGN}\) is embedded into \(\mathsf {S4N}_t\) by \(\tau \). Moreover, every Kripke-complete Galois negation logic _L_ is embedded into its tense companion \(\tau (L)\). (shrink)

We prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present (...) a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search. (shrink)

Modal counterparts of intermediate predicate logics will be studied by means of algebraic devise. Our main tool will be a construction of algebraic semantics for modal logics from algebraic frames for predicate logics. Uncountably many examples of modal counterparts of intermediate predicate logics will be given.

We develop a predicate logical extension of a subintuitionistic propositional logic. Therefore a Hilbert type calculus and a Kripke type model are given. The propositional logic is formulated to axiomatize the idea of strategic weakening of Kripke''s semantic for intuitionistic logic: dropping the semantical condition of heredity or persistence leads to a nonmonotonic model. On the syntactic side this leads to a certain restriction imposed on the deduction theorem. By means of a Henkin argument strong (...) completeness is proved making use of predicate logical principles, which are only classically acceptable. (shrink)

We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely (...) combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers ∀ new and ∃ new which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels. (shrink)

This paper presents an intuitionistic proof of a statement which under a classical reading is logically equivalent to Gödel's completeness theorem for classical predicate logic.

We provide a sucient frame-theoretic condition for a super bi-intuitionistic logic to have Maksimova's variable separation property. We conclude that bi-intuitionistic logic enjoys the property. Furthermore, we offer an algebraic characterization of the super-bi-intuitionistic logics with Maksimova's property.

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by (...) the semantics is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle. (shrink)

The paper presents predicate logical extensions of some subintuitionistic logics. Subintuitionistic logics result if conditions of the accessibility relation in Kripke models for intuitionistic logic are dropped. The accessibility relation which interprets implication in models for the propositional base subintuitionistic logic considered here is neither persistent on atoms, nor reflexive, nor transitive. Strongly complete predicate logical extensions are modeled with a second accessibility relation, which is a partial order, for the interpretation of the universal quantifier.

We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call "intuitionistic path axioms". We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.

A notion of strictly primitive recursive realizability is introduced by Damnjanovic in 1994. It is a kind of constructive semantics of the arithmetical sentences using primitive recursive functions. It is of interest to study the corresponding predicate logic. It was argued by Park in 2003 that the predicate logic of strictly primitive recursive realizability is not arithmetical. Park’s argument is essentially based on a claim of Damnjanovic that intuitionistic logic is sound with respect to (...) strictly primitive recursive realizability, but that claim was disproved by the author of this article in 2006. The aim of this paper is to present a correct proof of the result of Park. (shrink)

We give a syntactic translation from first-order intuitionistic predicate logic into second-order intuitionistic propositional logic IPC2. The translation covers the full set of logical connectives ∧, ∨, →, ⊥, ∀, and ∃, extending our previous work, which studied the significantly simpler case of the universal-implicational fragment of predicate logic. As corollaries of our approach, we obtain simple proofs of nondefinability of ∃ from the propositional connectives and nondefinability of ∀ from ∃ in the (...) second-order intuitionistic propositional logic. We also show that the ∀-free fragment of IPC2 is undecidable. (shrink)