The purpose of this paper is to define a new logic $${\mathcal {SI}}$$ called semi-intuitionistic logic such that the semi-Heyting algebras introduced in [ 4 ] by Sankappanavar are the semantics for $${\mathcal {SI}}$$ . Besides, the intuitionistic logic will be an axiomatic extension of $${\mathcal {SI}}$$.

Motivated by the definition of semi-Nelson algebras, a propositional calculus called semi-intuitionistic logic with strong negation is introduced and proved to be complete with respect to that class of algebras. An axiomatic extension is proved to have as algebraic semantics the class of Nelson algebras.

Semi-intuitionistic logic is the logic counterpart to semi-Heyting algebras, which were defined by H. P. Sankappanavar as a generalization of Heyting algebras. We present a new, more streamlined set of axioms for semi-intuitionistic logic, which we prove translationally equivalent to the original one. We then study some formulas that define a semi-Heyting implication, and specialize this study to the case in which the formulas use only the lattice operators and the (...) class='Hi'>intuitionistic implication. We prove then that all the logics thus obtained are equivalent to intuitionistic logic, and give their Kripke semantics. (shrink)

The variety \ of semi-Heyting algebras was introduced by H. P. Sankappanavar [13] as an abstraction of the variety of Heyting algebras. Semi-Heyting algebras are the algebraic models for a logic HsH, known as semi-intuitionistic logic, which is equivalent to the one defined by a Hilbert style calculus in Cornejo :9–25, 2011) [6]. In this article we introduce a Gentzen style sequent calculus GsH for the semi-intuitionistic logic whose associated logic (...) GsH is the same as HsH. The advantage of this presentation of the logic is that we can prove a cut-elimination theorem for GsH that allows us to prove the decidability of the logic. As a direct consequence, we also obtain the decidability of the equational theory of semi-Heyting algebras. (shrink)

The paper proves a conjecture of Solomon Feferman concerning the indefiniteness of the continuum hypothesis relative to a semi-intuitionistic set theory.

We study the problem of finding a basis for all rules admissible in the intuitionistic propositional logic IPC. The main result is Theorem 3.1 which gives a basis consisting of all rules in semi-reduced form satisfying certain specific additional requirements. Using developed technique we also find a basis for rules admissible in the logic of excluded middle law KC.

The variety \(\mathbb{DHMSH}\) of dually hemimorphic semi-Heyting algebras was introduced in 2011 by the second author as an expansion of semi-Heyting algebras by a dual hemimorphism. In this paper, we focus on the variety \(\mathbb{DHMSH}\) from a logical point of view. The paper presents an extensive investigation of the logic corresponding to the variety of dually hemimorphic semi-Heyting algebras and of its axiomatic extensions, along with an equally extensive universal algebraic study of their corresponding algebraic semantics. (...) Firstly, we present a Hilbert-style axiomatization of a new logic called "Dually hemimorphic semi-Heyting logic" (\(\mathcal{DHMSH}\), for short), as an expansion of semi-intuitionistic logic \(\mathcal{SI}\) (also called \(\mathcal{SH}\)) introduced by the first author by adding a weak negation (to be interpreted as a dual hemimorphism). We then prove that it is implicative in the sense of Rasiowa and that it is complete with respect to the variety \(\mathbb{DHMSH}\). It is deduced that the logic \(\mathcal{DHMSH}\) is algebraizable in the sense of Blok and Pigozzi, with the variety \(\mathbb{DHMSH}\) as its equivalent algebraic semantics and that the lattice of axiomatic extensions of \(\mathcal{DHMSH}\) is dually isomorphic to the lattice of subvarieties of \(\mathbb{DHMSH}\). A new axiomatization for Moisil's logic is also obtained. Secondly, we characterize the axiomatic extensions of \(\mathcal{DHMSH}\) in which the "Deduction Theorem" holds. Thirdly, we present several new logics, extending the logic \(\mathcal{DHMSH}\), corresponding to several important subvarieties of the variety \(\mathbb{DHMSH}\). These include logics corresponding to the varieties generated by two-element, three-element and some four-element dually quasi-De Morgan semi-Heyting algebras, as well as a new axiomatization for the 3-valued Łukasiewicz logic. Surprisingly, many of these logics turn out to be connexive logics, only a few of which are presented in this paper. Fourthly, we present axiomatizations for two infinite sequences of logics namely, De Morgan Gödel logics and dually pseudocomplemented Gödel logics. Fifthly, axiomatizations are also provided for logics corresponding to many subvarieties of regular dually quasi-De Morgan Stone semi-Heyting algebras, of regular De Morgan semi-Heyting algebras of level 1, and of JI-distributive semi-Heyting algebras of level 1. We conclude the paper with some open problems. Most of the logics considered in this paper are discriminator logics in the sense that they correspond to discriminator varieties. Some of them, just like the classical logic, are even primal in the sense that their corresponding varieties are generated by primal algebras. (shrink)

In this paper we introduce a logic that we name semi Heyting–Brouwer logic, \, in such a way that the variety of double semi-Heyting algebras is its algebraic counterpart. We prove that, up to equivalences by translations, the Heyting–Brouwer logic \ is an axiomatic extension of \ and that the propositional calculi of intuitionistic logic \ and semi-intuitionistic logic \ turn out to be fragments of \.

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, (...) and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics. (shrink)

Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic in a finite types together with various forms of the axiom of choice and a numerical omniscience schema which implies classical logic for arithmetical formulas. Feferman subsequently observed that the proof theoretic strength of such systems can be determined by functional interpretation based on a non-constructive μ-operator and his well-known results on the strength of this operator from the 70's. In this note we consider a weaker form LNOS of (...) NOS which suffices to derive the strong form of binary König's lemma studied by Coquand/Palmgren and gives rise to a new and mathematically strong semi-classical system which, nevertheless, can proof theoretically be reduced to primitive recursive arithmetic PRA. The proof of this fact relies on functional interpretation and a majorization technique developed in a previous paper. (shrink)

In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these metatheorems which (...) allow one to prove similar uniformities even for unbounded spaces as long as certain local boundedness conditions are satisfied. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proof. Finally, we illustrate our main metatheorem by an example from metric fixed point theory. (shrink)

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$. Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$. In addition, we show that this conservation theorem is optimal (...) in the sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. (shrink)

Most axiomatizations of set theory that have been treated metamathematically have been based either entirely on classical logic or entirely on intuitionistic logic. But a natural conception of the settheoretic universe is as an indefinite (or “potential”) totality, to which intuitionistic logic is more appropriately applied, while each set is taken to be a definite (or “completed”) totality, for which classical logic is appropriate; so on that view, set theory should be axiomatized on some (...) correspondingly mixed basis. Similarly, in the case of predicative analysis, the natural numbers are considered to form a definite totality, while the universe of sets (or functions) of natural numbers are viewed as an indefinite totality, so that, again, a mixed semi-constructive logic should be the appropriate one to treat the two together. Various such semiconstructive systems of analysis and set theory are formulated here and their proof-theoretic strength is characterized. Interestingly, though the logic is weakened, one can in compensation strengthen certain principles in a way that could be advantageous for mathematical applications. (shrink)

A contraction-free and cut-free sequent calculus \ for semi-De Morgan algebras, and a structural-rule-free and single-succedent sequent calculus \ for De Morgan algebras are developed. The cut rule is admissible in both sequent calculi. Both calculi enjoy the decidability and Craig interpolation. The sequent calculi are applied to prove some embedding theorems: \ is embedded into \ via Gödel–Gentzen translation. \ is embedded into a sequent calculus for classical propositional logic. \ is embedded into the sequent calculus \ (...) for intuitionistic propositional logic. (shrink)

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which still (...) serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic. (shrink)

This paper is devoted to the reconstruction of the implicit logic of Plato’s Par-menides. The reconstructed logic, F, makes it possible to form a new semi-intuitionistic system of logic of predicates, FN. The axioms of Peano Arithmetic (PA) and an axiom of infinity follow from FN. Therefore, FN can be seen as a new attempt at the realization of Frege’s logicist program. Some very strong systems can be seen as other variants of FN, e.g. Leśniewski’s (...) ontology. The hypothesis from Parmenides II contains proof of the existence of the two highest principles, i.e. the One and the Dyad, their mutual relationship, their relations to other things, and the reasoning regarding the mutual relationship follows some exact formal rules. Six types of Plato’s negation of a predicate are defined. The system is a first-order logic with non-classical negation of a predicate (local negation) that is non-definable by classical sentential negation. Therefore, the implicit logic of Plato’s Parmenides differs from classical syllogistics (formed in the Łukasiewicz’s style) as well as from the classical predicate calculus. (shrink)

This paper focuses on order-preserving logics defined from varieties of distributive lattices with negation, and in particular on the problem of whether these can be axiomatized by means Hilbert-style calculi that are finite. On the negative side, we provide a syntactic condition on the equational presentation of a variety that entails failure of finite axiomatizability for the corresponding logic. An application of this result is that the logic of all distributive lattices with negation is not finitely axiomatizable; we (...) likewise establish that the order-preserving logic of the variety of all Ockham algebras is also not finitely axiomatizable. On the positive side, we show that an arbitrary subvariety of semi-De Morgan algebras is axiomatized by a finite number of equations if and only if the corresponding order-preserving logic is axiomatized by a finite Hilbert-style calculus. This equivalence also holds for every subvariety of a Berman variety of Ockham algebras. We obtain, as a corollary, a new proof that the implication-free fragment of intuitionistic logic is finitely axiomatizable, as well as a new corresponding Hilbert-style calculus. Our proofs are constructive in that they allow us to effectively convert an equational presentation of a variety of algebras into a Hilbert-style calculus for the corresponding order-preserving logic, and vice versa. We also consider the assertional logics associated to the above-mentioned varieties, showing in particular that the assertional logics of finitely axiomatizable subvarieties of semi-De Morgan algebras are finitely axiomatizable as well. (shrink)

Along the line of Hirst‐Mummert and Dorais, we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2‐statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2‐statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong (...) class='Hi'>semi‐intuitionistic systems including bar induction in all finite types but also nonconstructive principles such as Kőnig's lemma and uniform weak Kőnig's lemma. Our result is applicable to many mathematical principles whose sequential versions imply. (shrink)

Although the theory of definability had many important antecedents—such as the descriptive set theory initiated by the French semi-intuitionists in the early 1900s—the main ideas were first laid out in precise mathematical terms by Alfred Tarski beginning in 1929. We review here the basic notions of languages, explicit definability, and grammatical complexity, and emphasize common themes in the theories of definability for four important languages underlying, respectively, descriptive set theory, recursive function theory, classical pure logic, and finite-universe (...) class='Hi'>logic. We review the history of previous studies of the similarities and differences in the theories of definability of the first three of these four languages. A seminal role leading toward unification of the theories has been played by the separation principles introduced by Nikolai Luzin in 1927. Emphasizing analogies and driving toward further unification embracing finite-universe logic we concentrate on a simple example—the first and second separation principles for existential-universal first-order sentences . Using this as a test case for the fundamental problem of how to “finitize” arguments in classical pure logic to the finite-universe case, we are led to the analogous negative solution by using the theory of certain special graphs: a graph is - special for any positive integers m , n , p , q iff it is bipartite with m red points and n blue points and for every p -tuple of red points there is a blue point to which they are all connected . As an aside we introduce for further study a natural “Ramseyesque” increasing sequence A of positive integers, where A is the least positive integer n for which an -special graph exists. (shrink)

In this paper we study an alternative approach to the concept of abstract logic and to connectives in abstract logics. The notion of abstract logic was introduced by Brown and Suszko —nevertheless, similar concepts have been investigated by various authors. Considering abstract logics as intersection structures we extend several notions to their κ -versions, introduce a hierarchy of κ -prime theories, which is important for our treatment of infinite connectives, and study different concepts of κ -compactness. We are (...) particularly interested in non-topped intersection structures viewed as semi-lattices with a minimal meet-dense subset, i.e., with a minimal generator set. We study a chain condition which is sufficient for a minimal generator set, implies compactness of the logic, and in regular logics is equivalent to compactness of the consequence relation together with the existence of a inconsistent set, where κ is the cofinality of the cardinality of the logic. Some of these results are known in a similar form in the context of closure spaces, we give extensions to intersection structures and to big cardinals presenting new proofs based on set-theoretical tools. The existence of a minimal generator set is crucial for our way to define connectives. Although our method can be extended to further non-classical connectives we concentrate here on intuitionistic and infinite ones. Our approach leads us to the concept of the set of complete theories which is stable under all considered connectives and gives rise to the definition of the topological space of the logic. Topological representations of abstract logics by means of this space remain to be further investigated. (shrink)

Brouwer's views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing (...) generality: from the least general Kripke semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy. (shrink)

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)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED (Calculus of Equational Deduction). This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations (in Dijkstra's words, "letting the symbols (...) do the work") have led to the "calculational style," an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system (I-CED), we prove Leibniz's principle for intuitionistic logic and also prove that any (intuitionistic) valid formula of predicate logic can be proved in I-CED. (shrink)

We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic ($$\textrm{CHL}$$ CHL ), hereby introduced as an example of a strongly connexive logic with an intuitive semantics. We use the reverse algebraisation paradigm: $$\textrm{CHL}$$ CHL is presented as the assertional logic of a point regular variety (whose structure theory is examined in detail) that turns out to be term equivalent to the variety of Heyting algebras. We provide Hilbert-style and Gentzen-style proof systems for (...) $$\textrm{CHL}$$ CHL ; moreover, we suggest a possible computational interpretation of its connexive conditional, and we revisit Kapsner’s idea of superconnexivity. (shrink)

This paper is a reaction to the following remark by grzegorczyk: "the compound sentences are not a product of experiment. they arise from reasoning. this concerns also negations; we see that the lemon is yellow, we do not see that it is not blue." generally, in science the truth is ascertained as indirectly as falsehood. an example: a litmus-paper is used to verify the sentence "the solution is acid." this approach gives rise to a (very intuitionistic indeed) conservative extension (...) of the heyting logic satisfying natural duality laws. (shrink)

We consider a logic which is semantically dual (in some precise sense of the term) to intuitionistic. This logic can be labeled as “falsification logic”: it embodies the Popperian methodology of scientific discovery. Whereas intuitionistic logic deals with constructive truth and non-constructive falsity, and Nelson's logic takes both truth and falsity as constructive notions, in the falsification logic truth is essentially non-constructive as opposed to falsity that is conceived constructively. We also briefly (...) clarify the relationships of our falsification logic to some other logical systems. (shrink)

We reconsider the pragmatic interpretation of intuitionistic logic [21] regarded as a logic of assertions and their justi cations and its relations with classical logic. We recall an extension of this approach to a logic dealing with assertions and obligations, related by a notion of causal implication [14, 45]. We focus on the extension to co-intuitionistic logic, seen as a logic of hypotheses [8, 9, 13] and on polarized bi-intuitionistic logic (...) as a logic of assertions and conjectures: looking at the S4 modal translation, we give a de nition of a system AHL of bi-intuitionistic logic that correctly represents the duality between intuitionistic and co-intuitionistic logic, correcting a mistake in previous work [7, 10]. A computational interpretation of cointuitionism as a distributed calculus of coroutines is then used to give an operational interpretation of subtraction.Work on linear co-intuitionism is then recalled, a linear calculus of co-intuitionistic coroutines is de ned and a probabilistic interpretation of linear co-intuitionism is given as in [9]. Also we remark that by extending the language of intuitionistic logic we can express the notion of expectation, an assertion that in all situations the truth of p is possible and that in a logic of expectations the law of double negation holds. Similarly, extending co-intuitionistic logic, we can express the notion of conjecture that p, de ned as a hypothesis that in some situation the truth of p is epistemically necessary. (shrink)

In the pioneering article and two papers, written jointly with McKinsey, Tarski developed the so-called algebraic and topological frameworks for the Intuitionistic Logic and the Lewis modal system. In this paper, we present an outline of modern systems with a topological tinge. We consider topological interpretation of basic systems GL and G of the provability logic in terms of the Cantor derivative and the Hausdorff residue.

Inquisitive logic is a research program seeking to expand the purview of logic beyond declarative sentences to include the logic of questions. To this end, inquisitive propositional logic extends classical propositional logic for declarative sentences with principles governing a new binary connective of inquisitive disjunction, which allows the formation of questions. Recently inquisitive logicians have considered what happens if the logic of declarative sentences is assumed to be intuitionistic rather than classical. In short, (...) what should inquisitive logic be on an intuitionistic base? In this paper, we provide an answer to this question from the perspective of nuclear semantics, an approach to classical and intuitionistic semantics pursued in our previous work. In particular, we show how Beth semantics for intuitionistic logic naturally extends to a semantics for inquisitive intuitionistic logic. In addition, we show how an explicit view of inquisitive intuitionistic logic comes via a translation into propositional lax logic, whose completeness we prove with respect to Beth semantics. (shrink)

I propose a new semantics for intuitionistic logic, which is a cross between the construction-oriented semantics of Brouwer-Heyting-Kolmogorov and the condition-oriented semantics of Kripke. The new semantics shows how there might be a common semantical underpinning for intuitionistic and classical logic and how intuitionistic logic might thereby be tied to a realist conception of the relationship between language and the world.

The sequent system LDJ is formulated using the same connectives as Gentzen's intuitionistic sequent system LJ, but is dual in the following sense: (i) whereas LJ is singular in the consequent, LDJ is singular in the antecedent; (ii) whereas LJ has the same sentential counter-theorems as classical LK but not the same theorems, LDJ has the same sentential theorems as LK but not the same counter-theorems. In particular, LDJ does not reject all contradictions and is accordingly paraconsistent. To obtain (...) a more precise mapping, both LJ and LDJ are extended by adding a "pseudo-difference" operator which is the dual of intuitionistic implication. Cut-elimination and decidability are proved for the extended systems and , and a simply consistent but -inconsistent Set Theory with Unrestricted Comprehension Schema based on LDJ is sketched. (shrink)

The interplay of introduction and elimination rules for propositional connectives is often seen as suggesting a distinguished role for intuitionistic logic. We prove three formal results about intuitionistic propositional logic that bear on that perspective, and discuss their significance.

There are basically two ways to view intuitionistic logic: as a philosophical‐foundational issue in mathematics; or as a technical discipline within mathematical logic. Considering first the philosophical aspects, for they will provide the motivation for the subject, this chapter follows L. E. J. Brouwer, the founding father of intuitionism. Although Brouwer himself contributed little to intuitionistic logic as seen from textbooks and papers, he did point the way for his successors.

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED . This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations have led to the "calculational style," an impressive array (...) of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system , we prove Leibniz's principle for intuitionistic logic and also prove that any valid formula of predicate logic can be proved in I-CED. (shrink)

Semantics connected to some information based metaphor are well-known in logic literature: a paradigmatic example is Kripke semantic for Intuitionistic Logic. In this paper we start from the concrete problem of providing suitable logic-algebraic models for the calculus of attribute dependencies in Formal Contexts with information gaps and we obtain an intuitive model based on the notion of passage of information showing that Kleene algebras, semi-simple Nelson algebras, three-valued ukasiewicz algebras and Post algebras of order (...) three are, in a sense, naturally and directly connected to partially defined information systems. In this way wecan provide for these logic-algebraic structures a raison dêetre different from the original motivations concerning, for instance, computability theory. (shrink)

In recent years, the logic of questions and dependencies has been investigated in the closely related frameworks of inquisitive logic and dependence logic. These investigations have assumed classical logic as the background logic of statements, and added formulas expressing questions and dependencies to this classical core. In this paper, we broaden the scope of these investigations by studying questions and dependency in the context of intuitionistic logic. We propose an intuitionistic team semantics, (...) where teams are embedded within intuitionistic Kripke models. The associated logic is a conservative extension of intuitionistic logic with questions and dependence formulas. We establish a number of results about this logic, including a normal form result, a completeness result, and translations to classical inquisitive logic and modal dependence logic. (shrink)

The interplay of introduction and elimination rules for propositional connectives is often seen as suggesting a distinguished role for intuitionistic logic. We prove three formal results concerning intuitionistic propositional logic that bear on that perspective, and discuss their significance. First, for a range of connectives including both negation and the falsum, there are no classically or intuitionistically correct introduction rules. Second, irrespective of the choice of negation or the falsum as a primitive connective, classical and (...) class='Hi'>intuitionistic consequence satisfy exactly the same structural, introduction, and elimination (briefly, elementary) rules. Third, for falsum as primitive only, intuitionistic consequence is the least consequence relation that satisfies all classically correct elementary rules. (shrink)

It is proved that there are exactly 16 superintuitionistic propositional logics with the projective Beth property. These logics are finitely axiomatizable and have the finite model property. Simultaneously, all varieties of Heyting algebras with strong epimorphisms surjectivity are found.

Extending the language of the intuitionistic propositional logic Int with additional logical constants, we construct a wide family of extensions of Int with the following properties: (a) every member of this family is a maximal conservative extension of Int; (b) additional constants are independent in each of them.

In the present day and age, it seems that every constructivist philosopher of mathematics and her brother wants to be known as an intuitionist. In this paper, It will be shown that such a self-identification is in most cases mistaken. For one thing, not any old (or new) constructivism is intuitionism because not any old relevant construction is carried out mentally in intuition, as Brouwer envisaged. (edited).

Research within the operational approach to the logical foundations of physics has recently pointed out a new perspective in which quantum logic can be viewed as an intuitionistic logic with an additional operator to capture its essential, i.e., non-distributive, properties. In this paper we will offer an introduction to this approach. We will focus further on why quantum logic has an inherent dynamic nature which is captured in the meaning of "orthomodularity" and on how it motivates (...) physically the introduction of dynamic implication operators, each for which a deduction theorem holds with respect to a dynamic conjunction. As such we can offer a positive answer to the many who pondered about whether quantum logic should really be called a logic. Doubts to answer the question positively were in first instance due to the former lack of an implication connective which satisfies the deduction theorem within quantum logic. (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 study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II.

In this paper we present two calculi for intuitionistic logic. The first one, IG, is characterized by the fact that every proof-search terminates and termination is reached without jeopardizing the subformula property. As to the second one, SIC, proof-search terminates, the subformula property is preserved and moreover proof-search is performed without any recourse to metarules, in particular there is no need to back-track. As a consequence, proof-search in the calculus SIC is accomplished by a single tree as in (...) classical logic. (shrink)