We study an extension of first-degree entailment (FDE) by Dunn and Belnap with a non-contingency operator |$\blacktriangle \phi $| which is construed as ‘|$\phi $| has the same value in all accessible states’ or ‘all sources give the same information on the truth value of |$\phi $|’. We equip this logic dubbed |$\textbf {K}^\blacktriangle _{\textbf {FDE}}$| with frame semantics and show how the bi-valued models can be interpreted as interconnected networks of Belnapian databases with the |$\blacktriangle $| operator modelling search (...) for inconsistencies in the provided information. We construct an analytic cut system for the logic and show its soundness and completeness. We prove that |$\blacktriangle $| is not definable via the necessity modality |$\Box $| of |$\textbf {K}_{\textbf{FDE}}$|⁠. Furthermore, we prove that in contrast to the classical non-contingency logic, reflexive, |$\textbf {S4}$| and |$\textbf {S5}$| (among others) frames are definable. (shrink)

We discuss two-layered logics formalising reasoning with paraconsistent probabilities that combine the Łukasiewicz [0, 1]-valued logic with Baaz ▵\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\triangle $$\end{document} operator and the Belnap–Dunn logic. The first logic (introduced in [7]) formalises a ‘two-valued’ approach where each event ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi $$\end{document} has independent positive and negative measures that stand for, respectively, the likelihoods of ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi (...) $$\end{document} and ¬ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\lnot \phi $$\end{document}. The second logic that we introduce here corresponds to ‘four-valued’ probabilities. There, ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi $$\end{document} is equipped with four measures standing for pure belief, pure disbelief, conflict and uncertainty of an agent in ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi $$\end{document}.We construct faithful embeddings of and into one another and axiomatise using a Hilbert-style calculus. We also establish the decidability of both logics and provide complexity evaluations for them using an expansion of the constraint tableaux calculus for. (shrink)

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)

ABSTRACTIn this paper, we present a generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems and which augment Avron's Frege system HŁuk with nested and general versions of the disjunction elimination rule, respectively. For these systems, we provide upper bounds on speed-ups w.r.t. both the number of steps in proofs (...) and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus GŁuk for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. (shrink)

In this paper we devise non-distributive relatives of Exactly true logic by Pietz and Riveccio and its dual Non-falsity logic by Shramko, Zaitsev and Belikov. We consider two pre-orders which are algebraic counterparts of the ETL’s and NFL’s entailment relations on the de Morgan lattice 4. We generalise these pre-orders and determine which distributive properties that hold on 4 are not forced by either of the pre-orders. We then construct relatives of ETL and NFL but lack such distributive properties. For (...) these logics we also devise a truth table semantics which uses non-distributive lattice M3 as their lattice of truth values. We also provide analytic tableaux systems which work with sequents of the form \. We then prove correctness and completeness results for these proof systems and provide a neat generalisation for non-distributive ETL- and NFL-like logics built over a certain family of non-distributive modular lattices. (shrink)

We consider four natural deduction systems: Fitch-style systems, Gentzen-style systems (in the form of dags), general deduction Frege systems and nested deduction Frege systems, as well as dag-like Gentzen-style sequent calculi. All these calculi soundly and completely formalize classical propositional logic. -/- We show that general deduction Frege systems and Gentzen-style natural calculi provide at most quadratic speedup over nested deduction Frege systems and Fitch-style natural calculi and at most cubic speedup over Gentzen-style sequent calculi.