Intuitionistic Logic

In this paper we explore the following question: how weak can a logic be for Rosser’s essential undecidability result to be provable for a weak arithmetical theory? It is well known that Robinson’s Q is essentially undecidable in intuitionistic logic, and P. Hájek proved it in the fuzzy logic BL for Grzegorczyk’s variant of Q which interprets the arithmetic operations as nontotal nonfunctional relations. We present a proof of essential undecidability in a much weaker substructural logic and for a much (...) weaker arithmetic theory, a version of Robinson’s R (with arithmetic operations also interpreted as mere relations). Our result is based on a structural version of the undecidability argument introduced by Kleene and we show that it goes well beyond the scope of the Boolean, intuitionistic, or fuzzy logic. (shrink)

I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms a : A and a = b : A are analytic is unfounded. As I shall show, when A evaluates to a dependent function type (x : (...) B) → C, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-Löf's original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic-synthetic distinction reworked here is capable of accommodating judgments of the forms A type and A = B type as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-Löf's position on the analytic grounding of synthetic judgments. (shrink)

Errett Bishop's work in constructive mathematics is overwhelmingly regarded as a turning point for mathematics based on intuitionistic logic. It brought new life to this form of mathematics and prompted the development of new areas of research that witness today's depth and breadth of constructive mathematics. Surprisingly, notwithstanding the extensive mathematical progress since the publication in 1967 of Errett Bishop's Foundations of Constructive Analysis, there has been no corresponding advances in the philosophy of constructive mathematics Bishop style. The aim of (...) this paper is to foster the philosophical debate about this form of mathematics. I begin by considering key elements of philosophical remarks by Bishop, especially focusing on Bishop's assessment of Brouwer. I then compare these remarks with ``traditional'' philosophical arguments for intuitionistic logic and argue that the latter are in tension with Bishop's views. ``Traditional'' arguments for intuitionistic logic turn out to be also in conflict with significant recent developments in constructive mathematics. This rises pressing questions for the philosopher of mathematics, especially with regard to the possibility of offering alternative philosophical arguments for constructive mathematics. I conclude with the suggestion to look anew at Bishop's own remarks for inspiration. (shrink)

Fine (2017) proposes a new logic of vagueness, CL, that promises to provide both a solution to the sorites paradox and a way to avoid the impossibility result from Fine (2008). The present paper presents a challenge to his new theory of vagueness. I argue that the possibility theorem stated in Fine (2017), as well as his solution to the sorites paradox, fail in certain reasonable extensions of the language of CL. More specifically, I show that if we extend the (...) language with any negation operator that obeys reductio ad absurdum, we can prove a new impossibility result that makes the kind of indeterminacy that Fine takes to be a hallmark of vagueness impossible. I show that such negation operators can be conservatively added to CL and examine some of the philosophical consequences of this result. Moreover, I demonstrate that we can define a particular negation operator that behaves exactly like intuitionistic negation in a natural and unobjectionable propositionally quantified extension of CL. Since intuitionistic negation obeys reductio, the new impossibility result holds in this propositionally quantified extension of CL. In addition, the sorites paradox resurfaces for the new negation. (shrink)

In this paper, we show (among other things) that the conditional in Frege's Begriffsschrift is ambiguous.

In an anonymous referee report written in 1945, Church suggested a sweeping argument against verificiationism, the thesis that every truth is knowable. The argument, which was published with due acknowledgement by Fitch almost two decades later, has generated significant attention as well as some interesting successor arguments. In this paper, we present the most important episodes in this intellectual history using the logic that Church himself favoured, and we give reasons for thinking that the arguments are less than decisive. However, (...) we present some new arguments against verificationism that we believe to be dialectically effective. (shrink)

Two new propositional non-classical logics, referred to as symmetric intuitionistic logic (SIL) and conflated intuitionistic logic (CIL), are introduced as indexed and non-indexed Gentzen-style sequent calculi. SIL is regarded as a natural hybrid logic combining intuitionistic and dual-intuitionistic logics, whereas CIL is regarded as a variant of intuitionistic paraconsistent logic with conflation and without paraconsistent negation. The cut-elimination theorems for SIL and CIL are proved. CIL is shown to be conservative over SIL.

Negation often reinforces problematic habits of othering, but rethinking negation can make good on feminist hopes for logic as a transformative space for inclusion. As Plumwood argues in her 1993 paper, not all uses of negation in the context of social identity are inherently problematic, but the widespread implicit use of classical negation has limited our options with respect to representing difference, ultimately reinforcing dualisms that essentialize social differences in problematic ways. In response to these limitations, I take inspiration from (...) Dembroff’s recent work on the metaphysics of genderqueer identity to build models of social identity using the Heyting-Brouwer logic developed by Rauszer in her 1974 paper. Ultimately, I argue that these models demonstrate both how classical negation reinforces problematic habits of othering and how alternative forms of negation can transform our treatment of social identity altogether. (shrink)

This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas additional to those familiar from standard intuitionist and classical logic. When $\invertediota$ is added it must be ensured that reduction procedures involving replacements of parameters by terms do not introduce new maximal formulas of higher degree than the ones removed. The problem is solved by a rule (...) that permits restricting these terms in the rules for $\forall$, $\exists$ and $\invertediota$ to parameters or constants. A restricted subformula property for deductions in systems without $\invertediota$ is considered. It is improved upon by an alternative formalisation of free logic building on an idea of Ja\'skowski's. In the classical system the rules for $\invertediota$ require treatment known from normalisation for classical logic with $\lor$ or $\exists$. The philosophical significance of the results is also indicated. (shrink)

In this paper we first introduce a new neighbourhood semantics for propositional intuitionistic logic. We then naturally extend this semantics to first-order intuitionistic logic. We also study bisimulation between neighbourhood models and prove some of their basic properties for both propositional and first-order intuitionistic logic.

In this paper, we propose a computational interpretation of the generalized Kreisel–Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry–Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding (...) computational content of the typed Split rule. Our investigation can also be reframed as an effort to answer the following question: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed general version called the S rule. (shrink)

In this paper, we consider the ex falso quodlibet rule (EFQ) as a derived rule and propose a new justification for it based on a rule we call the collapse rule. The collapse rule is a mix between EFQ and disjunctive syllogism (DS). Informally, it says that a choice between a proposition A and ⊥, which is understood as nullary disjunction, is no choice at all and it defaults to A. Thus, we can regard it as capturing the idea of (...) an implosion principle in contrast to EFQ’s explosion principle. Furthermore, we show that the collapse rule can also be used to justify DS and that all these three rules have the same deductive strength: they are all interderivable. Thus, the discussions about the justification of EFQ or DS be reduced to a discussion about the justification of the collapse rule. (shrink)

In his essay ‘“Wang’s Paradox”’, Crispin Wright proposes a solution to the Sorites Paradox (in particular, the form of it he calls the ‘Paradox of Sharp Boundaries’) that involves adopting intuitionistic logic when reasoning with vague predicates. He does not give a semantic theory which accounts for the validity of intuitionistic logic (and the invalidity of stronger logics) in that area. The present essay tentatively makes good the deficiency. By applying a theorem of Tarski, it shows that intuitionistic logic is (...) the strongest logic that may be applied, given certain semantic assumptions about vague predicates. The essay ends with an inconclusive discussion of whether those semantic assumptions should be accepted. (shrink)

It has long been known that (classical) Peano arithmetic is, in some strong sense, “equivalent” to the variant of (classical) Zermelo–Fraenkel set theory (including choice) in which the axiom of infinity is replaced by its negation. The intended model of the latter is the set of hereditarily finite sets. The connection between the theories is so tight that they may be taken as notational variants of each other. Our purpose here is to develop and establish a constructive version of this. (...) We present an intuitionistic theory of the hereditarily finite sets, and show that it is definitionally equivalent to Heyting Arithmetic, in a sense to be made precise. Our main target theory, the intuitionistic small set theory is remarkably simple, and intuitive. It has just one non-logical primitive, for membership, and three straightforward axioms plus one axiom scheme. We locate our theory within intuitionistic mathematics generally. (shrink)

It is widely accepted that there is a clear sense in which the first-order paraconsistent constructive logic with strong negation of Almukdad and Nelson, QN4, is more constructive than intuitionistic first-order logic, QInt. While QInt and QN4 both possess the disjunction property and the existence property as characteristics of constructiveness (or constructivity), QInt lacks certain features of constructiveness enjoyed by QN4, namely the constructible falsity property and the dual of the existence property. This paper deals with the constructiveness of the (...) contra-classical, connexive, paraconsistent, and contradictory non-trivial first-order logic QC, which is a connexive variant of QN4. It is shown that there is a sense in which QC is even more constructive than QN4. The argument focuses on a problem that is mirror-inverted to Raymond Smullyan’s drinker paradox, namely the invalidity of what will be called the drinker truism and its dual in QN4 (and QInt), and on a version of the Brouwer-Heyting-Kolmogorov interpretation of the logical operations that treats proofs and disproofs on a par. The validity of the drinker truism and its dual together with the greater constructiveness of QC in comparison to QN4 may serve as further motivation for the study of connexive logics and suggests that constructive logic is connexive and contradictory (the latter understood as being negation inconsistent). (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...) expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (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)

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)

The principle motivation of this work is to display the sense in which the epistemic reading of a Kripke model tacitly requires common knowledge of the model, CKM. This requirement significantly restricts the amount of epistemic situations we are able to consider. We explore possible worlds epistemic models in a general setting without CKM assumptions and show that such models can be identified with observable substructures of Kripke models. We argue that such observable models offer a new level of generality (...) and conceptual clarity in epistemic modeling. Similar analysis applies to intuitionistic models. (shrink)

The constructive mathematics developed by Bishop in Foundations of Constructive Analysis succeeded in gaining the attention of mathematicians, but discussions of its underlying philosophy are still rare in the literature. Commentators seem to conclude, from Bishop’s rejection of choice sequences and his severe criticism of Brouwerian intuitionism, that he is not an intuitionist–broadly understood as someone who maintains that mathematics is a mental creation, mathematics is meaningful and eludes formalization, mathematical objects are mind-dependent constructions given in intuition, and mathematical truths (...) are experienceable. This paper develops and defends an intuitionistic interpretation of Bishop’s philosophical views. (shrink)

The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication (∃,→) is proved to be undecidable in presence of free type variables (constants). This contrasts with the result that inutitionistic propositional second-order logic with existential quantifier, conjunction and negation is decidable.

We introduce a basic intuitionistic conditional logic \(\textsf{IntCK}\) that we show to be complete both relative to a special type of Kripke models and relative to a standard translation into first-order intuitionistic logic. We show that \(\textsf{IntCK}\) stands in a very natural relation to other similar logics, like the basic classical conditional logic \(\textsf{CK}\) and the basic intuitionistic modal logic \(\textsf{IK}\). As for the basic intuitionistic conditional logic \(\textsf{ICK}\) proposed in Weiss (_Journal of Philosophical Logic_, _48_, 447–469, 2019 ), \(\textsf{IntCK}\) (...) extends its language with a diamond-like conditional modality \(\Diamond \hspace{-4.0pt}\rightarrow \), but its ( \(\Diamond \hspace{-4.0pt}\rightarrow \) )-free fragment is also a proper extension of \(\textsf{ICK}\). We briefly discuss the resulting gap between the two candidate systems of basic intuitionistic conditional logic and the possible pros and cons of both candidates. (shrink)

In this Dissertation, we examine a handful of related themes in the philosophy of logic and mathematics. We take as a starting point the deeply philosophical, and—as we argue, deeply Kantian—views of L.E.J. Brouwer, the founder of intuitionism. We examine his famous first act of intuitionism. Therein, he put forth both a critical and a constructive idea. This critical idea involved digging a philosophical rift between what he thought of himself as doing and what he thought of his contemporaries, specifically (...) Hilbert, as doing. He sought to completely separate mathematics from mathematical language, and thereby logic. In chapter 3, we examine the philosophical foundations for this separation. Artemov Artemov (2001) articulates what we might think of as constructive propositional reasoning in a formal system that augments classical propositional logic with a theory of proofs. In doing this, instead of using just one type of object to characterize constructive reasoning, he uses two; propositions and proofs. In chapter 4, we explore the extent to which it might make sense to think of classical propositional reasoning as instead a theory that has two types of objects in the Artemov style. In chapters 5 and 6, we examine two specific case studies; we look at two philosophical phenomena that admit of formal characterizations and then propose those. In both cases, we focus on predicate style treatments of modality. (shrink)

Without directly addressing the Demarcation Problem for logic—the problem of distinguishing logical vocabulary from others—we focus on distinctive aspects of logical vocabulary in pursuit of a second goal in the philosophy of logic, namely, proposing criteria for the justification of logical rules. Our preferred approach has three components. Two of these are effectively Belnap’s, but with a twist. We agree with Belnap’s response to Prior’s challenge to inferentialist characterisations of the meanings of logical constants. Belnap argued that for a logical (...) constant to exist, its rules must be conservative over a previously given consequence relation and guarantee the uniqueness of the constant. The twist is that we require logical vocabulary to be provably conservative, not over a previously given formal consequence relation, but over a previously given meaningful vocabulary of a language. Uniqueness is also a feature defined in terms of provability: if two syntactically distinguished expressions are governed by the same rules, then formulas with them as main operators are interderivable. Belnap’s criteria are not only those for the existence of a logical constant, but more: they are what distinguishes logical vocabulary from all other expressions. It is the defining mark of a logical constant that it is provably conservative over the fragment of the language which excludes it and that its rules guarantee its uniqueness. The third component is the topic neutrality of logic. The provable conservativeness of logic over a previously given vocabulary of a language is motivated, in part, by appeal to molecularism in the theory of meaning. Molecularity is a feature endorsed by the theory of meaning as a whole, so it does not distinguish logical constants from other expressions. The same is true for conservativeness. We argue that molecularity, and hence conservativeness, are implicit presuppositions of speakers’ use of language: the addition of new vocabulary to a language is presupposed to be conservative. But this presupposition is one that we should be able reflectively to endorse (such as when attempting a rational reconstruction of the use of the vocabulary). Thus, where conservativeness is found to fail, this defect should be remedied and the use of the vocabulary corrected (as in classical negation) or excised altogether (as in pejoratives). We go on to characterise a notion of topic neutrality, which we argue applies to logical vocabulary. We then note that reflective endorsement of the conservativeness of a topic neutral vocabulary requires a proof that the vocabulary is conservative relative to any base vocabulary. Thus we require that logical vocabulary be demonstrably conservative. Allying this requirement, distinctive of logic, to a general consideration about the commitments of assertion yields a mode of justification for logical constants akin to some conceptions of Harmony, i.e., to the idea that the consequences of assertion of a logical complex need to be warranted by the grounds and ought to be the strongest consequences warranted by the grounds. Intuitionistic logic acquires a somewhat familiar justification but emanating from a new motivation. (shrink)

Brouwer’s intuitionism was a far-reaching attempt to reform the foundations of mathematics. While the mathematical community was reluctant to accept Brouwer’s work, its response to later-developed brands of intuitionism, such as those presented by Hermann Weyl and Arend Heyting, was different. The paper accounts for this difference by analyzing the intuitionistic versions of Brouwer, Weyl, and Heyting in light of a two-tiered model of the body and image of mathematical knowledge. Such a perspective provides a richer account of each story (...) and points to a possible connection between the community’s reaction and the changes each mathematician had proposed. (shrink)

I argue against the interpretation of propositions as intentions and proof-objects as fulfillments proposed by Heyting and defended by Tieszen and van Atten. The idea is already a frequent target of criticisms regarding the incompatibility of Brouwer’s and Husserl’s positions, mainly by Rosado Haddock and Hill. I raise a stronger objection in this paper. My claim is that even if we grant that the incompatibility can be properly dealt with, as van Atten believes it can, two fundamental issues indicate that (...) the interpretation is unsustainable regardless: (1) it is hard to determine, without appealing to propositional intentions on pain of circularity, what intention a proof-object should be understood as a fulfillment of; (2) due to a difficult fulfillment dilemma, it is unclear, at best, what the object of an intention corresponding to a proposition is. (shrink)

Chapter 1 constitutes an introduction to Gentzen calculi from two perspectives, logical and philosophical. It introduces the notion of generalisations of Gentzen sequent calculus and the discussion on properties that characterize good inferential systems. Among the variety of Gentzen-style sequent calculi, I divide them in two groups: syntactic and semantic generalisations. In the context of such a discussion, the inferentialist philosophy of the meaning of logical constants is introduced, and some potential objections – mainly concerning the choice of working with (...) semantic generalizations – are addressed. Finally, I’ll introduce the case studies that I’ll be dealing with in part II. Chapter 2 is concerned with the origins and development of Jaśkowski’s discussive logic. The main idea of this chapter is to systematize the various stages of the development of discussive logic related researches from two different angles, i.e., its connections to modal logics and its proof theory, by highlighting virtues and vices. Chapter 3 focuses on the Gentzen-style proof theory of discussive logic, by providing a characterization of it in terms of labelled sequent calculi. Chapter 4 deals with the Gentzen-style proof theory of relevant logics, again by employing the methodology of labelled sequent calculi. This time, instead of working with a single logic, I’ll deal with a whole family of them. More precisely, I’ll study in terms of proof systems those relevant logics that can be characterised, at the semantic level, by reduced Routley-Meyer models, i.e., relational structures with a ternary relation between states and a unique base element. Chapter 5 investigates the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an ‘actuality’ operator to the connectives. This logic was introduced also using Gentzen sequents. Unfortunately, the original proof system is not cut-free. This chapter shows how to solve this problem by moving to hypersequents. Chapter 6 concludes the investigations and discusses the future of the research presented throughout the dissertation. (shrink)

In his paper ‘The possibility of vagueness’ (Fine in Synthese 194(10):3699–3725, 2017), Kit Fine proposes a new logic of vagueness, CL, that promises to provide both a solution to the sorites paradox and a way to avoid the impossibility result from Fine (Philos Perspect 22(1):111–136, 2008). The present paper presents a challenge to his new theory of vagueness. I argue that the possibility theorem stated in Fine (Synthese 194(10):3699–3725, 2017), as well as his solution to the sorites paradox, fail in (...) certain reasonable extensions of the language of CL. More specifically, I show that if we extend the language with any negation operator that obeys reductio ad absurdum, we can prove a new impossibility result that makes the kind of indeterminacy that Fine takes to be a hallmark of vagueness impossible. I show that such negation operators can be conservatively added to CL and examine some of the philosophical consequences of this result. Moreover, I demonstrate that we can define a particular negation operator that behaves exactly like intuitionistic negation in a natural and unobjectionable propositionally quantified extension of CL. Since intuitionistic negation obeys reductio, the new impossibility result holds in this propositionally quantified extension of CL. In addition, the sorites paradox resurfaces for the new negation. (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 presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...) implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in the given signature; (...) if instead of adding Reiteration, one adds the rule of Reductio ad Absurdum, one obtains a proof system for orthologic; by adding both Reiteration and Reductio, one obtains a proof system for classical logic. Arguably neither Reiteration nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rules are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logic, orthologic, and classical logic. The algebraic semantics for the logic we motivate proof-theoretically is based on bounded lattices equipped with what has been called a weak pseudocomplementation. We show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semantics for the logic. This builds on our previous study of representations of lattices with negations, which we extend and specialize for several types of negation in addition to weak pseudocomplementation; in an appendix, we further extend this representation to lattices with implications. Finally, we discuss adding to our logic a conditional obeying only introduction and elimination rules, interpreted as a modality using a family of accessibility relations. (shrink)

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)

The main research goal of the work is to study the notion of co-topos, its correctness, properties and relations with toposes. In particular, the dualization process proposed by proponents of co-toposes has been analyzed, which transforms certain Heyting algebras of toposes into co-Heyting ones, by which a kind of paraconsistent logic may appear in place of intuitionistic logic. It has been shown that if certain two definitions of topos are to be equivalent, then in one of them, in the context (...) of a subobject classifier, there should be a neutral label for the generic subobject, or if the label "true" appears instead, it carries no additional properties or assumptions. It has been shown that a natural isomorphism occurring in one of the definitions of topos need not be an isomorphism of the corresponding algebraic structures on the sets, so that a co-Heyting algebraic structure can be defined on the set of characteristic morphisms, which moreover will also be natural. The analyzes suggest that the notion of co-topos may be considered correct. However, it should be strongly emphasized that although the possibility of defining the notion of co-topos has been shown, its further full consequences should be very carefully examined, which can severely limit its logical applications. (shrink)

Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon $ - (...) and $\tau $ -formulas and using the translation of quantifiers into $\varepsilon $ - and $\tau $ -terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate ${\varepsilon \tau }$ -calculi. The “extended” first $\varepsilon $ -theorem holds if the base logic is finite-valued Gödel–Dummett logic, and fails otherwise, but holds for certain provable formulas in infinite-valued Gödel logic. The second $\varepsilon $ -theorem also holds for finite-valued first-order Gödel logics. The methods used to prove the extended first $\varepsilon $ -theorem for infinite-valued Gödel logic suggest applications to theories of arithmetic. (shrink)

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated \(\mathsf {ND}^1_{\mathsf {ISCI}}\) and a semantically motivated \(\mathsf {ND}^2_{\mathsf {ISCI}}\). The formulation of \(\mathsf {ND}^1_{\mathsf {ISCI}}\) is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, but due (...) to the normalization procedure non-subformulas can label only leaves of proofs. In \(\mathsf {ND}^2_{\mathsf {ISCI}}\), we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic. (shrink)

In 2001, W. Carnielli and Marcos considered a 3-valued logic in order to prove that the schema ϕ ∨ (ϕ → ψ) is not a theorem of da Costa’s logic Cω. In 2006, this logic was studied (and baptized) as G'3 by Osorio et al. as a tool to define semantics of logic programming. It is known that the truth-tables of G'3 have the same expressive power than the one of Łukasiewicz 3-valued logic as well as the one of Gödel (...) 3-valued logic G3. From this, the three logics coincide up-to language, taking into acccount that 1 is the only designated truth-value in these logics. -/- From the algebraic point of view, Canals-Frau and Figallo have studied the 3-valued modal implicative semilattices, where the modal operator is the well-known Moisil-Monteiro-Baaz Δ operator, and the supremum is definable from this. We prove that the subvariety obtained from this by adding a bottom element 0 is term-equivalent to the variety generated by the 3-valued algebra of G'3. The algebras of that variety are called G'3-algebras. From this result, we obtain the equations which axiomatize the variety of G'3-algebras. Moreover, we prove that this variety is semisimple, and the 3-element and the 2-element chains are the unique simple algebras of the variety. Finally an extension of G'3 to first-order languages is presented, with an algebraic semantics based on complete G'3-algebras. The corresponding soundness and completeness theorems are obtained. (shrink)

In this paper, we study three representations of lattices by means of a set with a binary relation of compatibility in the tradition of Ploščica. The standard representations of complete ortholattices and complete perfect Heyting algebras drop out as special cases of the first representation, while the second covers arbitrary complete lattices, as well as complete lattices equipped with a negation we call a protocomplementation. The third topological representation is a variant of that of Craig, Haviar, and Priestley. We then (...) extend each of the three representations to lattices with a multiplicative unary modality; the representing structures, like so-called graph-based frames, add a second relation of accessibility interacting with compatibility. The three representations generalize possibility semantics for classical modal logics to non-classical modal logics, motivated by a recent application of modal orthologic to natural language semantics. (shrink)

This book is dedicated to V.A. Yankov’s seminal contributions to the theory of propositional logics. His papers, published in the 1960s, are highly cited even today. The Yankov characteristic formulas have become a very useful tool in propositional, modal and algebraic logic. The papers contributed to this book provide the new results on different generalizations and applications of characteristic formulas in propositional, modal and algebraic logics. In particular, an exposition of Yankov’s results and their applications in algebraic logic, the theory (...) of admissible rules and refutation systems is included in the book. In addition, the reader can find the studies on splitting and join-splitting in intermediate propositional logics that are based on Yankov-type formulas which are closely related to canonical formulas, and the study of properties of predicate extensions of non-classical propositional logics. The book also contains an exposition of Yankov’s revolutionary approach to constructive proof theory. The editors also include Yankov’s contributions to history and philosophy of mathematics and foundations of mathematics, as well as an examination of his original interpretation of history of Greek philosophy and mathematics. (shrink)

Cet ouvrage offre une introduction accessible à la théorie de la démonstration : il donne les détails des preuves et comporte de nombreux exemples et exercices pour faciliter la compréhension des lecteurs. Il est également conçu pour servir d’aide à la lecture des articles fondateurs de Gerhard Gentzen. L’ouvrage introduit également aux trois principaux formalismes en usage : l’approche axiomatique des preuves, la déduction naturelle et le calcul des séquents. Il donne une démonstration claire et détaillée des résultats fondamentaux du (...) domaine : traduction de l’arithmétique classique vers l’arithmétique intuitionniste, élimination des coupures, théorème de normalisation et conduit ensuite pas à pas le lecteur vers l’exposé de la célèbre preuve de cohérence de Gentzen pour l’arithmétique de Peano du premier ordre. Il comble ainsi une importante lacune éditoriale en présentant à la fois la théorie structurelle et la théorie ordinale de la démonstration. (shrink)

Frame semantics for negation on the Australian Plan accommodates many different negations, but it falls short on accommodating subminimal negation when the language contains conjunction and disjunction. In this paper, I will present a multi-relational frame semantics –multi-incompatibility frame semantics– that can accommodate subminimal negation. I will first argue that multi-incompatibility frames are in accordance with the philosophical motivations behind negation on the Australian Plan, namely its modal and exclusion-expressing nature. Then, I will prove the soundness and completeness results of (...) a subminimal logic that consists of the multi-incompatibility semantics and a proof system with operational rules that characterize subminimal negation, conjunction and disjunction. Lastly, I will prove some key correspondence theorems that relate frame conditions to certain principles that are associated with stronger negations, which will give rise to a new kite of negations that includes subminimal negation. (shrink)

Among Dunn’s many important contributions to relevance logic was his work on the system RM (R-mingle). Although RM is an interesting system in its own right, it is widely considered to be too strong. In this chapter, I revisit a closely related system, RM0 (sometimes known as ‘constructive mingle’), which includes the mingle axiom while not degenerating in the way that RM itself does. My main interest will be in examining this logic from two related semantical perspectives. First, I give (...) a purely operational bisemilattice semantics for it by adapting previous work of Humberstone. Second, I examine a more conventional algebraic semantics for it and discuss how this relates to the operational semantics. A novel operational semantics for J (intuitionistic logic) as well as its conventional Heyting algebraic semantics emerge as special cases of the corresponding semantics for RM0. The results of this chapter suggest that RM0 is a more interesting logic than has been appreciated and that Humberstone’s operational semantic framework similarly deserves more attention than it has received. (shrink)

In this paper we analyse logic of false belief in the intuitionistic setting. This logic, studied in its classical version by Steinsvold, Fan, Gilbert and Venturi, describes the following situation: a formula $\varphi$ is not satisfied in a given world, but we still believe in it. Another interpretations are also possible: e.g. that we do not accept $\varphi$ but it is imposed on us by a kind of council or advisory board. From the mathematical point of view, the idea is (...) expressed by an adequate form of modal operator $\mathsf{W}$ which is interpreted in relational frames with neighborhoods. We discuss monotonicity of forcing, soundness, completeness and several other issues. Finally, we mention the fact that it is possible to investigate intuitionistic logics of unknown truths. (shrink)

This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation (...) to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman–Hilton duality. (shrink)

We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how (...) extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray code from a proof of inclusion of the corresponding coinductive predicates. (shrink)

In this book set theory INC# based on intuitionistic logic with restricted modus ponens rule is proposed. It proved that intuitionistic logic with restricted modus ponens rule can to safe Cantor naive set theory from a triviality.