This work is motivated by the problem of finding the limit of the applicability of the first incompleteness theorem ($\textsf{G1}$). A natural question is, can we find a minimal theory for which $\textsf{G1}$ holds? We examine the Turing degree structure of recursively enumerable (RE) theories for which $\textsf{G1}$ holds and the interpretation degree structure of RE theories weaker than the theory $\textbf{R}$ with respect to interpretation for which $\textsf{G1}$ holds. We answer all questions that we posed in [2], and prove (...) more results about them. It is known that there are no minimal essentially undecidable theories with respect to interpretation. We generalize this result and give some general characterizations, which tell us under what conditions there are no minimal RE theories having some property with respect to interpretation. (shrink)

We consider two computability notions for functions mapping all left-c.e. reals to left-c.e. reals, namely functions computable in the Banach–Mazur and Markov senses. We show that any total Banach–Mazur computable function is also Markov computable, but this is no longer true for partial functions. We also prove a sufficient condition for the almost continuity on the left of Banach–Mazur computable functions, from which it follows that Markov computable functions that are total or whose domains are sets of left-c.e. reals common (...) in the literature (such as Martin-Löf random, regainingly approximable, and speedable left-c.e. reals) are almost continuous on the left. Finally, we construct a Markov computable function that is not pseudocontinuous on the left. (shrink)

Proof theorists have long been struggling to provide simple accounts of various modal logics. Drawing on the recent literature on metainferences, I develop in the present paper a novel approach to this challenge: regular sequent systems augmented with natural deduction-like rules for assuming and discharging sequents. Based on this approach, I introduce an elegant calculus for the modal logic S4⁠. Various discharging conditions on assumptions are shown to yield the weaker logics K⁠, D, and ⁠T. The rules in these calculi (...) have attractive proof-theoretic properties: they are explicit, symmetrical, and non-circular, and they enjoy the subformula property. (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.

The product of two $\textbf {Alt}$ logics possesses the polynomial product finite model property and its membership problem is $\textbf {coNP}$-complete. Using a reduction from an undecidable domino-tiling problem, we prove that its admissibility problem is undecidable.

We show that both the $n$-density and the bounded $n$-width of Kripke frames can be modally defined not only with natural and well-known Sahlqvist formulae containing a linear number of different propositional variables but also with formulae of polynomial length with a logarithmic number of different propositional variables and then we prove that this exponential decrease in the number of variables leads us outside the class of Sahlqvist formulae.

In this paper, we argue that the usual approach to modelling knowledge and belief with the necessity modality $\Box $ does not produce intuitive outcomes in the framework of the Belnap–Dunn logic ($\textsf{BD}$, alias $\textbf{FDE}$—first-degree entailment). We then motivate and introduce a nonstandard modality $\blacksquare $ that formalizes knowledge and belief in $\textsf{BD}$ and use $\blacksquare $ to define $\bullet $ and $\blacktriangledown $ that formalize the unknown truth and ignorance as not knowing whether, respectively. Moreover, we introduce another modality (...) $\textbf{I}$ that stands for factive ignorance and show its connection with $\blacksquare $. We equip these modalities with Kripke-frame-based semantics and construct a sound and complete analytic cut system for $\textsf{BD}^{\blacksquare }$ and $\textsf{BD}^{\textbf{I}}$—the expansions of $\textsf{BD}$ with $\blacksquare $ and $\textbf{I}$. In addition, we show that $\Box $ as it is customarily defined in $\textsf{BD}$ cannot define any of the introduced modalities, nor, conversely, neither $\blacksquare $ nor $\textbf{I}$ can define $\Box $. We also demonstrate that $\blacksquare $ and $\textbf{I}$ are not interdefinable and establish the definability of several important classes of frames using $\blacksquare $. (shrink)

In this paper, we introduce the variety of $I$-modal ririgs. We characterize the congruence lattice of its members by means of $I$-filters, and we provide a description of $I$-filter generation. We also provide an axiomatic presentation for the variety generated by chains of the subvariety of contractive $I$-modal ririgs. Finally, we introduce a Hilbert-style calculus for a logic with $I$-modal ririgs as an equivalent algebraic semantics and we prove that such a logic has the parametrized local deduction-detachment theorem.

Usually in logic, proof systems are defined having in mind proving properties like validity and semantic consequence. It seems worthwhile to address the problem of having proof systems where satisfiability is a primitive notion in the sense that a formal derivation means that a finite set of formulas is satisfiable. Moreover, it would be useful to cover within the same framework as many logics as possible. We consider Kripke semantics where the properties of the constructors are provided by valuation constraints (...) as the common ground of those logics. This includes for instance intuitionistic logic, paraconsistent Nelson’s logic ${\textsf{N4}}$, paraconsistent logic ${\textsf{imbC}}$ and modal logics among others. After specifying a logic by those valuation constraints, we show how to induce automatically and from scratch an existential proof system for that logic. The rules of the proof system are shown to be invertible. General results of soundness and completeness are proved and then applied to the logics at hand. (shrink)

We present a uniform proof-theoretic proof of the Gödel–McKinsey–Tarski embedding for a class of first-order intuitionistic theories. This is achieved by adapting to the case of modal logic the methods of proof analysis in order to convert axioms into rules of inference of a suitable sequent calculus. The soundness and the faithfulness of the embedding are proved by induction on the height of the derivations in the augmented calculi. Finally, we define an extension of the modal system for which the (...) result holds with respect to geometric intuitionistic. (shrink)