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

A terminating sequent calculus for intuitionistic propositional logic is obtained by modifying the R$\supset $ rule of the labelled sequent calculus $\mathbf {G3I}$. This is done by adding a variant of the principle of a fortiori in the left-hand side of the premiss of the rule. In the resulting calculus, called ${\mathbf {G3I}}_{\mathbf {t}}$, derivability of any given sequent is directly decidable by root-first proof search, without any extra device such as loop-checking. In the negative case, the failed proof search gives a finite countermodel to the sequent on a reflexive, transitive, and Noetherian Kripke frame. As a byproduct, a direct proof of faithfulness of the embedding of intuitionistic logic into Grzegorcyk logic is obtained.

We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from [8] that any Grothendieck fibration of the kind being considered can automatically be upgraded to a two-dimensional fibration, after which the invariance property is reduced to an abstract theorem concerning pseudonatural transformations of morphisms into two-dimensional fibrations.

Werner’s set-theoretical model is one of the simplest models of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort “ ${\tt Prop}$ ”. However, this model of ${\tt Prop}$ is so coarse that the principle of excluded middle $P \lor \neg P$ holds. Following our previous work, we interpret ${\tt Prop}$ into a topological space (a special case of Heyting algebra) to make the model more intuitionistic without sacrificing simplicity. We improve on that work by providing a full interpretation of dependent product types, using Alexandroff spaces. We also extend our approach to inductive types by adding support for ${\mathsf{list}}$ s.

Sahlqvist theory is extended to the fragments of the intuitionistic propositional calculus that include the conjunction connective. This allows us to introduce a Sahlqvist theory of intuitionistic character amenable to arbitrary protoalgebraic deductive systems. As an application, we obtain a Sahlqvist theorem for the fragments of the intuitionistic propositional calculus that include the implication connective and for the extensions of the intuitionistic linear logic.

Intuitionistic logic formalises the foundational ideas of L.E.J. Brouwer’s mathematical programme of intuitionism. It is one of the earliest non-classical logics, and the difference between classical and intuitionistic logic may be interpreted to lie in the law of the excluded middle, which asserts that either a proposition is true or its negation is true. This principle is deemed unacceptable from the constructive point of view, in whose understanding the law means that there is an effective procedure to determine the truth of all propositions. This understanding of the distinction between the two logics supports the view that negation plays a vital role in the formulation of intuitionistic logic.

Nonetheless, the formalisation of negation in intuitionistic logic has not been universally accepted, and many alternative accounts of negation have been proposed. Some seek to weaken or strengthen the negation, and others actively supporting negative inferences that are impossible with it.

This thesis follows this tradition and investigates various aspects of negation in intuitionistic logic. Firstly, we look at a problem proposed by H. Ishihara, which asks how effectively one can conserve the deducibility of classical theorems into intuitionistic logic, by assuming atomic classes of non-constructive principles. The classes given in this section improve a previous class given by K. Ishii in two respects: (a) instead of a single class for the law of the excluded middle, two classes are given in terms of weaker principles, allowing a finer analysis and (b) the conservation now extends to a subsystem of intuitionistic logic called Glivenko’s logic. This section also discusses the extension of Ishihara’s problem to minimal logic.

Secondly, we study the relationship between two frameworks for weak constructive negation, the approach of D. Vakarelov on one hand and the framework of subminimal negation by A. Colacito, D. de Jongh, and A. L. Vargas on the other hand. We capture a version of Vakarelov’s logic with the semantics of the latter framework, and clarify the relationship between the two semantics. This also provides proof-theoretic insights, which results in the formulation of a cut-free sequent calculus for the aforementioned system.

Thirdly, we investigate the ways to unify the formalisations of some logics with contra-intuitionistic inferences. The enquiry concerns paraconsistent logics by R. Sylvan and A. B. Gordienko, as well as the logic of co-negation by G. Priest and of empirical negation by M. De and H. Omori. We take Sylvan’s system as basic, and formulate the frame conditions of the defining axioms of the other systems. The conditions are then used to obtain cut-free labelled sequent calculi for the systems.

Finally, we consider L. Humberstone’s actuality operator for intuitionistic logic, which can be seen as the dualisation of a contra-intuitionistic negation. A compete axiomatisation of intuitionistic logic with actuality operator is given, and comparisons are made for some related operators.

Abstract prepared by Satoru Niki.

E-mail: [email protected]

The language of linear temporal logic can be interpreted on the class of dynamic topological systems, giving rise to the intuitionistic temporal logic ${\sf ITL}^{\sf c}_{\Diamond \forall }$ , recently shown to be decidable by Fernández-Duque. In this article we axiomatize this logic, some fragments, and prove completeness for several familiar spaces.

The Gödel translation provides an embedding of the intuitionistic logic $\mathsf {IPC}$ into the modal logic $\mathsf {Grz}$ , which then embeds into the modal logic $\mathsf {GL}$ via the splitting translation. Combined with Solovay’s theorem that $\mathsf {GL}$ is the modal logic of the provability predicate of Peano Arithmetic $\mathsf {PA}$ , both $\mathsf {IPC}$ and $\mathsf {Grz}$ admit provability interpretations. When attempting to ‘lift’ these results to the monadic extensions $\mathsf {MIPC}$ , $\mathsf {MGrz}$ , and $\mathsf {MGL}$ of these logics, the same techniques no longer work. Following a conjecture made by Esakia, we add an appropriate version of Casari’s formula to these monadic extensions (denoted by a ‘+’), obtaining that the Gödel translation embeds $\mathsf {M^{+}IPC}$ into $\mathsf {M^{+}Grz}$ and the splitting translation embeds $\mathsf {M^{+}Grz}$ into $\mathsf {MGL}$ . As proven by Japaridze, Solovay’s result extends to the monadic system $\mathsf {MGL}$ , which leads us to a provability interpretation of both $\mathsf {M^{+}IPC}$ and $\mathsf {M^{+}Grz}$ .

We show that monadic intuitionistic quantifiers admit the following temporal interpretation: “always in the future” (for $\forall $ ) and “sometime in the past” (for $\exists $ ). It is well known that Prior’s intuitionistic modal logic ${\sf MIPC}$ axiomatizes the monadic fragment of the intuitionistic predicate logic, and that ${\sf MIPC}$ is translated fully and faithfully into the monadic fragment ${\sf MS4}$ of the predicate ${\sf S4}$ via the Gödel translation. To realize the temporal interpretation mentioned above, we introduce a new tense extension ${\sf TS4}$ of ${\sf S4}$ and provide a full and faithful translation of ${\sf MIPC}$ into ${\sf TS4}$ . We compare this new translation of ${\sf MIPC}$ with the Gödel translation by showing that both ${\sf TS4}$ and ${\sf MS4}$ can be translated fully and faithfully into a tense extension of ${\sf MS4}$ , which we denote by ${\sf MS4.t}$ . This is done by utilizing the relational semantics for these logics. As a result, we arrive at the diagram of full and faithful translations shown in Figure 1 which is commutative up to logical equivalence. We prove the finite model property (fmp) for ${\sf MS4.t}$ using algebraic semantics, and show that the fmp for the other logics involved can be derived as a consequence of the fullness and faithfulness of the translations considered.

In this work we present some new contributions towards two different directions in the study of modal logic. First we employ tense logics to provide a temporal interpretation of intuitionistic quantifiers as “always in the future” and “sometime in the past.” This is achieved by modifying the Gödel translation and resolves an asymmetry between the standard interpretation of intuitionistic quantifiers.

Then we generalize the classic Gelfand–Naimark–Stone duality between compact Hausdorff spaces and uniformly complete bounded archimedean $\ell $ -algebras to a duality encompassing compact Hausdorff spaces with continuous relations. This leads to the notion of modal operators on bounded archimedean $\ell $ -algebras and in particular on rings of continuous real-valued functions on compact Hausdorff spaces. This new duality is also a generalization of the classic Jónsson-Tarski duality in modal logic.

Abstract taken directly from the thesis.

E-mail: [email protected]

URL: https://www.proquest.com/openview/5d284dbfb954383da9364149fa312b6f/1?pq-origsite=gscholar&cbl=18750&diss=y

Strong negation is a well-known alternative to the standard negation in intuitionistic logic. It is defined virtually by giving falsity conditions to each of the connectives. Among these, the falsity condition for implication appears to unnecessarily deviate from the standard negation. In this paper, we introduce a slight modification to strong negation, and observe its comparative advantages over the original notion. In addition, we consider the paraconsistent variants of our modification, and study their relationship with non-constructive principles and connexivity.

We explore the problems that confront any attempt to explain or explicate exactly what a primitive logical rule of inference is, or consists in. We arrive at a proposed solution that places a surprisingly heavy load on the prospect of being able to understand and deal with specifications of rules that are essentially self-referring. That is, any rule $\rho $ is to be understood via a specification that involves, embedded within it, reference to rule $\rho $ itself. Just how we arrive at this position is explained by reference to familiar rules as well as less familiar ones with unusual features. An inquiry of this kind is surprisingly absent from the foundations of inferentialism—the view that meanings of expressions (especially logical ones) are to be characterized by the rules of inference that govern them.

Here, we present a category ${\mathbf {pEff}}$ which can be considered a predicative variant of Hyland's Effective Topos ${{\mathbf {Eff} }}$ for the following reasons. First, its construction is carried in Feferman’s predicative theory of non-iterative fixpoints ${{\widehat {ID_1}}}$ . Second, ${\mathbf {pEff}}$ is a list-arithmetic locally cartesian closed pretopos with a full subcategory ${{\mathbf {pEff}_{set}}}$ of small objects having the same categorical structure which is preserved by the embedding in ${\mathbf {pEff}}$ ; furthermore subobjects in ${{\mathbf {pEff}_{set}}}$ are classified by a non-small object in ${\mathbf {pEff}}$ . Third ${\mathbf {pEff}}$ happens to coincide with the exact completion of the lex category defined as a predicative rendering in ${{\widehat {ID_1}}}$ of the subcategory of ${{\mathbf {Eff} }}$ of recursive functions and it validates the Formal Church’s thesis. Hence pEff turns out to be itself a predicative rendering of a full subcategory of ${{\mathbf {Eff} }}$ .

Rybakov (1984a) proved that the admissible rules of $\mathsf {IPC}$ are decidable. We give a proof of the same theorem, using the same core idea, but couched in the many notions that have been developed in the mean time. In particular, we illustrate how the argument can be interpreted as using refinements of the notions of exactness and extendibility.

For the Heyting Arithmetic HA, $HA^{\text{*}} $ is defined [14, 15] as the theory $\left\{ {A|HA \vdash A^\square } \right\}$, where $A^\square $ is called the box translation of A (Definition 2.4). We characterize the ${\text{\Sigma }}_1 $-provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $ (Definition 3.17).

We show that the polynomial translation of the classical propositional normal modal logic S4 into the intuitionistic propositional logic Int from Fernández is incorrect. We give a modified translation and prove its correctness, and provide implementations of both translations to allow others to test our results.

This paper consists in the formulation of a novel categorical set theory, MLCat, which is proved to be equiconsistent to New Foundations (NF), and which can be modulated to correspond to intuitionistic (denoted with an “I” on the left) or classical NF, with atoms (denoted with a “U” on the right) or not:

This paper shows that any propositional logic that extends a basic substructural logic BSL (a weak, nondistributive, nonassociative, and noncommutative version of Full Lambek logic with a paraconsistent negation) can be enriched with questions in the style of inquisitive semantics and logic. We introduce a relational semantic framework for substructural logics that enables us to define the notion of an inquisitive extension of λ, denoted as ${\lambda ^?}$, for any logic λ that is at least as strong as BSL. A general theory of these “inquisitive extensions” is worked out. In particular, it is shown how to axiomatize ${\lambda ^?}$, given the axiomatization of λ. Furthermore, the general theory is applied to some prominent logical systems in the class: classical logic Cl, intuitionistic logic Int, and t-norm based fuzzy logics, including for example Łukasiewicz fuzzy logic Ł. For the inquisitive extensions of these logics, axiomatization is provided and a suitable semantics found.