Search

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. [ABSTRACT FROM AUTHOR]

The general aim of this article is to study the negation fragment of classical logic within the framework of contemporary (Abstract) Algebraic Logic. More precisely, we shall find the three classes of algebras that are canonically associated with a logic in Algebraic Logic, i.e. we find the classes |$\textrm{Alg}^*$|⁠ , |$\textrm{Alg}$| and the intrinsic variety of the negation fragment of classical logic. In order to achieve this, firstly, we propose a Hilbert-style axiomatization for this fragment. Then, we characterize the reduced matrix models and the full generalized matrix models of this logic. Also, we classify the negation fragment in the Leibniz and Frege hierarchies. [ABSTRACT FROM AUTHOR]

In the present paper, we continue the research in Zhao (2021, Logic J. IGPL) to develop the Sahlqvist completeness theory for hybrid logic with satisfaction operators and downarrow binders |$\mathcal {L}(@, {\downarrow })$|⁠. We define the class of restricted Sahlqvist formulas for |$\mathcal {L}(@, {\downarrow })$| following the ideas in Conradie and Robinson (2017, J. Logic Comput. , 27, 867–900), but we follow a different proof strategy which is purely proof-theoretic, namely showing that for every restricted Sahlqvist formula |$\varphi $| and its hybrid pure correspondence |$\pi $|⁠ , |$\textbf {K}_{\mathcal {H}(@, {\downarrow })}+\varphi $| proves |$\pi $|⁠ ; therefore, |$\textbf {K}_{\mathcal {H}(@, {\downarrow })}+\varphi $| is complete with respect to the class of frames defined by |$\pi $|⁠ , using a modified version |$\textsf {ALBA}^{{\downarrow }}_{\textsf {Modified}}$| of the algorithm |$\textsf {ALBA}^{{\downarrow }}$| defined in Zhao (2021, Logic J. IGPL). [ABSTRACT FROM AUTHOR]

The well-known logic first degree entailment logic (FDE), introduced by Belnap and Dunn, is defined with |$\wedge $|⁠ , |$\vee $| and |$\sim $| as the sole primitive connectives. The aim of this paper is to establish the lattice formed by the class of all 4-valued C-extending implicative expansions of FDE verifying the axioms and rules of Routley and Meyer's basic logic B and its useful disjunctive extension B |$^{\textrm {d}}$|⁠. It is to be noted that Boolean negation (so, classical propositional logic) is definable in the strongest element in the said class. [ABSTRACT FROM AUTHOR]

In this paper, the predicate counterparts, defined both axiomatically and semantically by means of Kripke frames, of the modal propositional logics |$\textbf {GL}$|⁠ , |$\textbf {Grz}$|⁠ , |$\textbf {wGrz}$| and their extensions are considered. It is proved that the set of semantical consequences on Kripke frames of every logic between |$\textbf {QwGrz}$| and |$\textbf {QGL.3}$| or between |$\textbf {QwGrz}$| and |$\textbf {QGrz.3}$| is |$\Pi ^1_1$| -hard even in languages with three (sometimes, two) individual variables, two (sometimes, one) unary predicate letters, and a single proposition letter. As a corollary, it is proved that infinite families of modal predicate axiomatic systems, based on the classical first-order logic and the modal propositional logics |$\textbf {GL}$|⁠ , |$\textbf {Grz}$|⁠ , |$\textbf {wGrz}$| are not Kripke complete. Both |$\Pi ^1_1$| -hardness and Kripke incompleteness results of the paper do not depend on whether the logics contain the Barcan formula. [ABSTRACT FROM AUTHOR]

This article is an editorial announcing a special issue of the Logic Journal of the IGPL in honor of John Newsome Crossley, a British-Australian logician who celebrated his 85th birthday in 2022. The issue includes papers written by Crossley's students and friends, covering a range of topics in logic and related fields. The editorial highlights Crossley's contributions to logic, his impact on the field in both the UK and Australia, and his reputation as a kind and friendly individual. The article also mentions a conference that was held in conjunction with the special issue and provides a link to recordings of the talks. [Extracted from the article]

Since the early days of artificial intelligence (AI), many logics have been explored as tools for knowledge representation and reasoning. In the spirit of the Crossley Festscrift and recognizing John Crossley's diverse interests and his legacy in both mathematical logic and computer science, I discuss examples from my own research that sit in the overlap of logic and AI, with a focus on supporting human–AI interactions. [ABSTRACT FROM AUTHOR]

Each of us has a story which we can think of as a set of beliefs, hopefully consistent. We make our decisions in view of our beliefs which may be probabilistic, in the general case, but simple yes or no as in this paper. Our beliefs are our envelope just as the shell of a tortoise is its envelope. Decision theory—or single agent game theory tells us when to make the best choice in a game of us against nature. But nature has no desire to further or frustrate our efforts. Nature is mysterious but not malign. Things change when there are other agents involved. Then the best thing for us to do will depend on what they do. And they will think the same. And we predict their actions in terms of what we think their beliefs are. But how do we coordinate with others whose beliefs are different? This paper addresses the issue of working together despite different beliefs. [ABSTRACT FROM AUTHOR]

In 2003 Zia Movahed pointed to a passage of Avicenna, written probably in 1022, which Movahed claimed anticipated the modal formula of Barcan (that 'For every |$x$| necessarily |$\phi $| ' entails 'Necessarily for every |$x$| |$\phi $| '), and its converse. Since 2003, examination of early logical writings of Avicenna has clarified how he understood entailments between modal sentences, using his own new temporal language to provide a kind of semantics. In the light of that, Movahed's claim for the Barcan formula needs some tidying up but is basically correct. But by his semantics Avicenna should not have claimed the converse Barcan formula and probably didn't claim it. [ABSTRACT FROM AUTHOR]

The Thousands of Problems for Theorem Provers (TPTP) World is a well-established infrastructure that supports research, development and deployment of automated theorem proving systems. This paper provides an overview of the logic languages of the TPTP World, from classical first-order form (FOF), through typed FOF, up to typed higher-order form, and beyond to non-classical forms. The logic languages are described in a non-technical way and are illustrated with examples using the TPTP language. [ABSTRACT FROM AUTHOR]

John Crossley settled in Australia in 1968 having been a graduate student and later University Lecturer at Oxford. This is a brief account of his logical career. It is a revised version of a webcast talk for World Logic Day on 14 January 2022. [ABSTRACT FROM AUTHOR]

In 2016, Béziau introduces a restricted notion of paraconsistency, the so-called genuine paraconsistency. A logic is genuine paraconsistent if it rejects the laws |$\varphi ,\neg \varphi \vdash \psi $| and |$\vdash \neg (\varphi \land \neg \varphi)$|⁠. In that paper, the author analyzes, among the three-valued logics, which of them satisfy this property. If we consider multiple-conclusion consequence relations, the dual properties of those above-mentioned are |$ \vdash \varphi , \neg \varphi $| and |$\neg (\psi \vee \neg \psi) \vdash $|⁠. We call genuine paracomplete logics those rejecting the mentioned properties. We present here an analysis of the three-valued genuine paracomplete logics. A very natural twist structures semantics for these logics is also found in a systematic way. This semantics produces automatically a simple and elegant Hilbert-style characterization for all these logics. Finally, we introduce the logic LGP which is genuine paracomplete is not genuine paraconsistent, not even paraconsistent and cannot be characterized by a single finite logical matrix. [ABSTRACT FROM AUTHOR]

The basis of the paper is a logic of analytical consequential implication, CI.0, which is known to be equivalent to the well-known modal system KT thanks to the definition A → B = df A ⥽ B ∧ Ξ (Α, Β), Ξ (Α, Β) being a symbol for what is called here Equimodality Property: (□A ≡ □B) ∧ (◊A ≡ ◊B). Extending CI.0 (=KT) with axioms and rules for the so-called circumstantial operator symbolized by *, one obtains a system CI.0*Eq in whose language one can define an operator ↠ suitable to formalize context-dependent conditionals (so to counterfactual conditionals) via the definition (Def ↠) A ↠ B = df *A ⥽ B ∧ Ξ (Α, Β).. The central problem of the paper is to identify inside CI.0*Eq + Def ↠ a set of axioms yielding the fragment consisting of all and only theorems in which only truth-functional operators and the two operators → and ↠ occur. This system, here called CI.0 , is introduced in §3. In view of the intended purpose, it is introduced a complete and tableau-decidable system KT w , which is an extension of KT with axioms for the so-called quasi-variables w (A), w (B)... Three translation functions among the three languages used in the paper are then introduced. The first, Tr, maps every wff of form *A into wffs of form w (A) ∧ A and translates theorems of CI.0*Eq into theorems of KT w. The second, t°, translates theorems of CI.0 into theorems of CI.0*Eq by applying Def↠. A third one, t , translates theorems of CI.0 into theorems of KT w. As a consequence, it follows that t°A = Tr t A. In §4 it is proved that CI.0 is complete w.r.t. the class of CI.0 -models of form  where f is a selection function and R an access relation. It is then proved (i) that CI.0 models may be converted into KT w -models; (ii) that the truth-value of a proposition in a world of a CI.0 -model is preserved in the same world of the derived KT w -model; (iii) that A is a CI.0 -thesis iff its translation t A is KT w -thesis. It follows that, if A is not a CI.0 -thesis, t A is not a KT w -thesis, so also that Tr t A is not a CI.0*Eq-thesis. Since t°A = Tr t A and t°A is a function built on Def↠, this proves that every t°-translation of a CI.0 -wff that is a CI.0*Eq-theorem is a CI.0 -theorem. Since the converse proposition is proved in §2, their conjunction establishes the desired result. In the final section, it is proved that CI.0 is tableau-decidable, that ↠ is not a trivial operator and that ↠ enjoys the positive and negative properties required in §1 for context-dependent conditionals. Some final remarks suggest that studying the relations between CI.0 and systems of classical conditional logic may be a promising line of investigation. [ABSTRACT FROM AUTHOR]

We present a temporal logic of branching time with four primitive operators: |$\exists {\mathcal {C}}$| – it may change whether ; |$\forall {\mathcal {C}} $| – it must change whether ; |$\exists \Box $| – it may be endlessly unchangeable that ; and |$\forall \Box $| – it must be endlessly unchangeable that. Semantically, operator |$\forall {\mathcal {C}}$| expresses a change in the logical value of the given formula in every state that may be an immediate successor of the one considered, while |$\exists {\mathcal {C}}$| expresses a change in the logical value of the given formula in some state that is a possible immediate successor. |$\forall {\mathcal {C}} $| and |$\exists {\mathcal {C}}$| are not normal operators, they are not mutually definable and have unusual properties: |$\forall {\mathcal {C}} A\leftrightarrow \forall {\mathcal {C}} \neg A$| and |$\exists {\mathcal {C}} A \leftrightarrow \exists {\mathcal {C}} \neg A$| are axioms. Operators |$\exists \Box $| and |$\forall \Box $| express endless unchangeability in some and all paths , respectively. Our axiomatization contains two infinitary rules that allow one to obtain |$\exists \Box A$| from infinitely many combinations of formulas with |$A, \neg , \forall {\mathcal {C}}, \land $|⁠ , and to get |$\forall \Box A$| from infinitely many combinations of formulas with |$A, \neg , \exists {\mathcal {C}}, \land $|⁠. We show that our formalism is complete by presenting a bridge between our logic and logic |$\textsf {UB}$|⁠ , which is a fragment of |$\textsf {CTL}$| in which until operators does not occur. [ABSTRACT FROM AUTHOR]

Neural networks are widely used in systems of artificial intelligence, but due to their black box nature, they have so far evaded formal analysis to certify that they satisfy desirable properties, mainly when they perform critical tasks. In this work, we introduce methods for the formal analysis of reachability and robustness of neural networks that are modeled as rational McNaughton functions by, first, stating such properties in the language of Łukasiewicz infinitely-valued logic and, then, using the reasoning techniques of such logical system. We also present a case study where we employ the proposed techniques in an actual neural network that we trained to predict whether it will rain tomorrow in Australia. [ABSTRACT FROM AUTHOR]

We study arbitrary intermediate propositional logics extended with a collection of axioms from (classical) justification logics. For these, we introduce various semantics by combining either Heyting algebras or Kripke frames with the usual semantic machinery used by Mkrtychev's, Fitting's or Lehmann and Studer's models for classical justification logics. We prove unified completeness theorems for all intermediate justification logics and their corresponding semantics using a respective propositional completeness theorem of the underlying intermediate logic. Further, by a modification of a method of Fitting, we prove unified realization theorems for a large class of intermediate justification logics and accompanying intermediate modal logics. [ABSTRACT FROM AUTHOR]

The logic E4 is related to Brady's BN4 in a similar way to which Anderson and Belnap's logic of entailment E is related to their logic of the relevant implication R. In 'A companion to Brady's 4-valued relevant logic: the 4-valued logic of entailment E4', quoted in this paper, three alternatives to BN4 and another three to E4 are summarily introduced in a couple of pages as the only alternatives containing Routley and Meyer's basic logic B, provided some conditions are fulfilled. The aim of this note is to prove (i) BN4 and its three alternatives are the same logic up to some point, since they are functionally equivalent to each other, as it is the case with E4 and its three alternatives, which are also functionally equivalent to each other; (ii) to some extent, E4 is superior to BN4, since the latter is functionally included in the former, but not conversely. [ABSTRACT FROM AUTHOR]

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 (i.e. that contain a finite number of finitary rule schemata). 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. [ABSTRACT FROM AUTHOR]

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 ccHa s and its extension |${\textrm {ILM}}$| - |${\vee }$| for c |$\vee $| cHa s 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 ccHa s 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 }$|⁠. [ABSTRACT FROM AUTHOR]

In the present paper, we obtain a Jónsson-style canonicity proof for the Sahlqvist fragment of distributive modal |$\mu $| -calculus in clopen semantics, alternative to the canonicity-via-correspondence argument in Conradie and Craig (2017, Journal of Logic and Computation , 27, 705–748), generalizing the results in Bezhanishvili and Hodkinson (2012, Theoretical Computer Science , 424, 1–19). The key ingredient of this proof is a characterization result about |$\sigma $| -contracting maps. [ABSTRACT FROM AUTHOR]

The interpretability logic IL P is the interpretability logic of all sufficiently strong |$\varSigma _1$| -sound finitely axiomatised theories, such as the Gödel-Bernays set theory. The interpretability logic IL is a strict subset of the intersection of the interpretability logics of all so-called reasonable theories, IL (All). It is known that both IL P and IL W are decidable, however their complexity has not been resolved previously. In [ 10 ] it was shown that the basic interpretability logic IL is PSPACE -complete. Here we prove the same for IL P and IL W. [ABSTRACT FROM AUTHOR]

Classical logic of formal provability includes Löb's theorem, but not reflection. In contrast, intuitions about the inferential behavior of informal provability (in informal mathematics) seem to invalidate Löb's theorem and validate reflection (after all, the intuition is, whatever mathematicians prove holds!). We employ a non-deterministic many-valued semantics and develop a modal logic T-BAT of an informal provability operator, which indeed does validate reflection and invalidates Löb's theorem. We study its properties and its relation to known provability-related paradoxical arguments. We also argue that T-BAT is a fairly sensible candidate for a formal logic of informal provability. [ABSTRACT FROM AUTHOR]

In this article, I consider the positive logic of Boolean groups (i.e. Abelian groups where every non-identity element has order 2), where these are taken as frames for an operational semantics à la Urquhart. I call this logic BG. It is shown that the logic over the smallest nontrivial Boolean group, taken as a frame, is identical to the positive fragment of a quasi-relevance logic that was developed by Robles and Méndez (an extension of this result where negation is included is also discussed). It is proved that BG satisfies the variable sharing property and is Halldén complete, while failing to satisfy the disjunction property. Sound and complete subscripted tableaux are presented for BG. An axiomatization (in the positive language extended with fusion) is presented, which is sound with respect to BG and, with respect to a related ternary relational semantics, complete; the problem of identifying a complete axiomatization for BG itself is left open. Connections between BG and the quasi-relevance logic KR are also discussed. [ABSTRACT FROM AUTHOR]

In the present paper, we develop the algorithmic correspondence theory for hybrid logic with binder |$\mathcal {H}(@, \downarrow)$|⁠. We define the class of Sahlqvist inequalities for |$\mathcal {H}(@, \downarrow)$|⁠ , and each inequality of which is shown to have a first-order frame correspondent effectively computable by an algorithm |$\textsf {ALBA}^{\downarrow }$|⁠. [ABSTRACT FROM AUTHOR]

This article investigates the connections between the logics of being wrong , introduced in Steinsvold (2011, Notre Dame J. Form. Log. , 52, 245–253), and factive ignorance , presented in Kubyshkina and Petrolo (2021, Synthese , 198, 5917–5928). The first part of the paper provides a sound and complete axiomatization of the logic of factive ignorance that corrects errors in Kubyshkina and Petrolo (2021, Synthese , 198, 5917–5928) and resolves questions about the expressivity of the language. In the second half, it is shown that the relationship between the two logics suggests an alternative axiomatization for the logic of factive ignorance, the adequacy of which is easily proved via straightforward translations. [ABSTRACT FROM AUTHOR]

A version of intuitionistic type theory is extended with opposite types, allowing a different formalization of negation and obtaining a paraconsistent type theory (⁠|$\textsf{PTT} $|⁠). The rules for opposite types in |$\textsf{PTT} $| are based on the rules of the so-called constructible falsity. A propositions-as-types correspondence between the many-sorted paraconsistent logic |$\textsf{PL}_\textsf{S} $| (a many-sorted extension of López-Escobar's refutability calculus presented in natural deduction format) and |$\textsf{PTT} $| is proven. Moreover, a translation of |$\textsf{PTT} $| into intuitionistic type theory is presented and some properties of |$\textsf{PTT} $| are discussed. [ABSTRACT FROM AUTHOR]

The need for a 'many-valued logic' in linguistics has been evident since the 1970s, but there was lack of clarity as to whether it should come from the family of fuzzy logics or from the family of probabilistic logics. In this regard, Fine [ 14 ] and Kamp [ 26 ] pointed out undesirable effects of fuzzy logic (the failure of idempotency and coherence) which kept two generations of linguists and philosophers at arm's length. (Another unwanted feature of fuzzy logic is the property of truth functionality.) While probabilistic logic is not fraught by the same problems, its lack of constructiveness, i.e. its inability to compose complex truth degrees from atomic truth degrees, did not make it more attractive to linguists either. In the absence of a clear perspective in 'many-valued logic', scholars chose to proliferate ontologies grafted atop the classical bivalent logic: ontologies for truth, individuals, events, situations, possible worlds and degrees. The result has been a collection of incompatible classical logics. In this paper, I present sample logic, in particular its semantics (not its axiomatization). Sample logics is a member of the family of probabilistic logics, which is constructive without being truth functional. More specifically, I integrate all the important linguistic data on which the classical logics are predicated. The concepts of (in)dependency and conditional (in)dependency are the cornerstones of sample logic. [ABSTRACT FROM AUTHOR]

In this paper, we study two companions of a logic, viz. the left variable inclusion companion and the restricted rules companion, their nature and interrelations, especially in connection with paraconsistency. A sufficient condition for the two companions to coincide has also been proved. Two new logical systems—intuitionistic paraconsistent weak Kleene logic (IPWK) and paraconsistent pre-rough logic (PPRL)—are presented here as examples of logics of left variable inclusion. IPWK is the left variable inclusion companion of intuitionistic propositional logic and is also the restricted rules companion of it. PPRL, on the other hand, is the left variable inclusion companion of pre-rough logic but differs from the restricted rules companion of it. We have discussed algebraic semantics for these logics in terms of Płonka sums. This amounts to introducing a contaminating truth value, intended to denote a state of indeterminacy. [ABSTRACT FROM AUTHOR]

We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the non-theorem. Therefore, we also obtain an embedding of the classical predicate logic of finite models into the logic of partial quasiary predicates over finite structures. As a consequence, we prove that the logic of partial quasiary predicates is undecidable—more precisely, |$\varSigma ^0_1$| -complete—over arbitrary structures and not recursively enumerable—more precisely, |$\varPi ^0_1$| -complete—over finite structures. [ABSTRACT FROM AUTHOR]

The logic |$G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$| was introduced in Robles and Mendéz (2014, Logic Journal of the IGPL , 22, 515–538) as a paraconsistent logic which is based on Gödel's 3-valued matrix, except that Kleene–Łukasiewicz's negation is added to the language and is used as the main negation connective. We show that |$G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$| is exactly the intersection of |$G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$| and |$G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$|⁠ , the two truth-preserving 3-valued logics which are based on the same truth tables. (In |$G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$| the set |${\cal D}$| of designated elements is |$\{1\}$|⁠ , while in |$G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$|   |${\cal D}=\{1,0.5\}$|⁠.) We then construct a Hilbert-type system which has (MP) for |$\to $| as its sole rule of inference, and is strongly sound and complete for |$G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$|⁠. Then we show how, by adding one axiom (in the case of |$G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$|⁠) or one new rule of inference (in the case of |$G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$|⁠), we get strongly sound and complete systems for |$G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$| and |$G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$|⁠. Finally, we provide quasi-canonical Gentzen-type systems which are sound and complete for those logics and show that they are all analytic, by proving the cut-elimination theorem for them. [ABSTRACT FROM AUTHOR]

We study the topic of realization from classical justification logics in the context of the recently introduced Gödel justification logics. We show that the standard Gödel modal logics of Caicedo and Rodriguez are not realized by the Gödel justification logics and moreover, we study possible extensions of the Gödel justification logics, which are strong enough to realize the standard Gödel modal logics. On the other hand, we study the fragments of the standard Gödel modal logics, which are realized by the usual Gödel justification logics. We prove the corresponding realization theorem by using Fitting's merging of realizations as well as appropriate hypersequent calculi on the modal side, adapting the work by Metcalfe and Olivetti. For these hypersequent calculi, we also show a cut-elimination theorem. We provide natural semantical characterizations for all of these newly introduced logics. [ABSTRACT FROM AUTHOR]

This document is a correction to a previous article titled "A note on functional relations in a certain class of implicative expansions of FDE related to Brady's 4-valued logic BN4." The correction addresses an error in the definition used in the proof of Proposition 3.2. The corrected definition states that A→B is equal to (A k3 B) ∨ (A→B), rather than (A k11 B) ∨ (A→B) as previously stated. The correction is reported by Gemma Robles and José M Méndez. [Extracted from the article]

Dynamic topological logic (⁠|$\textsf{DTL}$|⁠) is a multi-modal logic that was introduced for reasoning about dynamic topological systems , i.e. structures of the form |$\langle{\mathfrak{X}, f}\rangle $|⁠ , where |$\mathfrak{X}$| is a topological space and |$f$| is a continuous function on it. The problem of finding a complete and natural axiomatization for this logic in the original tri-modal language has been open for more than one decade. In this paper, we give a natural axiomatization of |$\textsf{DTL}$| and prove its strong completeness with respect to the class of all dynamic topological systems. Our proof system is infinitary in the sense that it contains an infinitary derivation rule with countably many premises and one conclusion. It should be remarked that |$\textsf{DTL}$| is semantically non-compact, so no finitary proof system for this logic could be strongly complete. Moreover, we provide an infinitary axiomatic system for the logic |${\textsf{DTL}}_{\mathcal{A}}$|⁠ , i.e. the |$\textsf{DTL}$| of Alexandrov spaces, and show that it is strongly complete with respect to the class of all dynamical systems based on Alexandrov spaces. [ABSTRACT FROM AUTHOR]

Inspired by an interesting quotation from the literature, we propose four modalities, called 'sane belief', 'insane belief', 'reliable belief' and 'unreliable belief', and introduce logics with each operator as the modal primitive. We show that the four modalities constitute a square of opposition, which indicates some interesting relationships among them. We compare the relative expressivity of these logics and other related logics, including a logic of false beliefs from the literature. The four main logics are all less expressive than the standard modal logic over various model classes, and the logics of sane and insane beliefs are, respectively, equally expressive as the logics of unreliable and reliable beliefs on any class of models. The logics of reliable and unreliable beliefs are then combined into a bimodal logic, which turns out to be equally expressive as the standard modal logic. Despite this, we cannot obtain a complete axiomatization of the minimal bimodal logic, by simply translating the axioms and rules of the minimal modal logic |$\textbf{K}$| into the bimodal language. We then introduce a schematic modality which unifies reliable and unreliable beliefs and axiomatize it over the class of all frames and also the class of serial frames. This line of research is finally extended to unify sane and insane beliefs and some axiomatizations are given. [ABSTRACT FROM AUTHOR]

Orthomodular posets form an algebraic formalization of the logic of quantum mechanics. A central question is how to introduce implication in such a logic. We give a positive answer whenever the orthomodular poset in question is of finite height. The crucial advantage of our solution is that the corresponding algebra, called implication orthomodular poset, i.e. a poset equipped with a binary operator of implication, corresponds to the original orthomodular poset and that its implication operator is everywhere defined. We present here a complete list of axioms for implication orthomodular posets. This enables us to derive an axiomatization in Gentzen style for the algebraizable logic of orthomodular posets of finite height. [ABSTRACT FROM AUTHOR]

In this work, we propose a variant of so-called informational semantics, a technique elaborated by Voishvillo, for two infectious logics, Deutsch's |${\mathbf{S}_{\mathbf{fde}}}$| and Szmuc's |$\mathbf{dS}_{\mathbf{fde}}$|⁠. We show how the machinery of informational semantics can be effectively used to analyse truth and falsity conditions of disjunction and conjunction. Using this technique, it is possible to claim that disjunction and conjunction can be rightfully regarded as such, a claim which was disputed in the recent literature. Both |${\mathbf{S}_{\mathbf{fde}}}$| and |$\mathbf{dS}_{\mathbf{fde}}$| are formalized in terms of natural deduction. This allows us to solve several problems: to develop a natural deduction calculus for |${\mathbf{S}_{\mathbf{fde}}}$| containing the standard form of disjunction elimination (in contrast to the calculus by Petrukhin), to introduce the first natural deduction calculus for |$\mathbf{dS}_{\mathbf{fde}}$| and to reflect the fundamental symmetry between |${\mathbf{S}_{\mathbf{fde}}}$| and |$\mathbf{dS}_{\mathbf{fde}}$| on proof-theoretical level forming a convenient basis for obtaining their well-known extensions |$\mathbf{K}^{\mathbf{w}}_{\mathbf{3}}$| and |$\mathbf{PWK}$|⁠. [ABSTRACT FROM AUTHOR]

The main result proves Lyndon's and Craig's interpolation properties for the logic of strict implication |${\textsf{F}}$|⁠ , with a purely syntactical method. A cut-free G3 -style sequent calculus |$ {\textsf{GF}} $| and its single-succedent variant |$ \textsf{GF}_{\textsf{s}} $| are introduced. |$ {\textsf{GF}} $| can be extended to a G3 -variant of the sequent calculus GBPC3 for Visser's basic logic. Also a simple syntactic proof of known embedding result of |$ {\textsf{F}} $| into |$ {\textsf{K}} $| is provided. An extension of |$ {\textsf{F}} $|⁠ , namely |$ \textsf{FD}, $| is considered as well. [ABSTRACT FROM AUTHOR]

A classical result by Słupecki states that a logic L is functionally complete for the 3-element set of truth-values THREE if, in addition to functionally including Łukasiewicz's 3-valued logic Ł3, what he names the ' |$T$| -function' is definable in L. By leaning upon this classical result, we prove a general theorem for defining binary expansions (i.e. expansions with a binary connective) of Kleene's strong logic that are functionally complete for THREE. [ABSTRACT FROM AUTHOR]

In this work, we investigate the representation of counterfactual conditionals using the vector logic, a matrix-vector formalism for logical functions and truth values. Inside this formalism, the counterfactuals can be transformed in complex matrices preprocessing an implication matrix with one of the square roots of NOT, a complex matrix. This mathematical approach puts in evidence the virtual character of the counterfactuals. This happens because this representation produces a valuation of a counterfactual that is the superposition of the two opposite truth values weighted, respectively, by two complex conjugated coefficients. This result shows that this procedure gives an uncertain evaluation projected on the complex domain. After this basic representation, the judgement of the plausibility of a given counterfactual allows us to shift the decision towards an acceptance or a refusal. This shift is the result of applying for a second time one of the two square roots of NOT. [ABSTRACT FROM AUTHOR]

Paraconsistent weak Kleene (⁠|$\textrm{PWK}$|⁠) logic is the |$3$| -valued logic based on the weak Kleene matrices and with two designated values. In this paper, we investigate the poset of prevarieties of generalized involutive bisemilattices, focussing in particular on the order ideal generated by Α |$\textrm{lg} (\textrm{PWK})$|⁠. Applying to this poset a general result by Alexej Pynko, we prove that, exactly like Priest's logic of paradox, |$\textrm{PWK}$| has only one proper nontrivial extension apart from classical logic: |$\textrm{PWK}_{\textrm{E}}\textrm{,}$| PWK logic plus explosion. This |$6$| -valued logic, unlike |$\textrm{PWK} $|⁠ , fails to be paraconsistent. We describe its consequence relation via a variable inclusion criterion and identify its Suszko-reduced models. [ABSTRACT FROM AUTHOR]

We offer tableaux systems for logics of essence and accident and logics of non-contingency, showing their soundness and completeness for Kripke semantics. We also show an interesting parallel between these logics based on the semantic insensitivity of the two non-normal operators by which these logics are expressed. [ABSTRACT FROM AUTHOR]

Argument evaluation , one of the central problems in argumentation theory, consists in studying what makes an argument a good one. This paper proposes a formal approach to argument evaluation from the perspective of justification logic. We adopt a multi-agent setting, accepting the intuitive idea that arguments are always evaluated by someone. Two general restrictions are imposed on our analysis: non-deductive arguments are left out and the goal of argument evaluation is fixed: supporting a given proposition. Methodologically, our approach uses several existing tools borrowed from justification logic, awareness logic, doxastic logic and logics for belief dependence. We start by introducing a basic logic for argument evaluation, where a list of argumentative and doxastic notions can be expressed. Later on, we discuss how to capture the mentioned form of argument evaluation by defining a preference operator in the object language. The intuitive picture behind this definition is that, when assessing a couple of arguments, the agent puts them to a test consisting of several criteria (filters). As a result of this process, a preference relation among the evaluated arguments is established by the agent. After showing that this operator suffers a special form of logical omniscience, called preferential omniscience, we discuss how to define an explicit version of it, more suitable to deal with non-ideal agents. The present work exploits the formal notion of awareness in order to model several informal phenomena: awareness of sentences, availability of arguments and communication between agents and external sources (advisers). We discuss several extensions of the basic logic and offer completeness and decidability results for all of them. [ABSTRACT FROM AUTHOR]

The present paper is devoted to present two pragmatic logics and their corresponding intended interpretations according to which an illocutionary act of (scientific) hypothesis-making is justified by a scintilla of evidence. The paper first introduces a general pragmatic frame for assertions, expanded to hypotheses, |${\mathsf{AH}}$| and a hypothetical pragmatic logic for evidence |${\mathsf{HLP}}$|⁠. Both |${\mathsf{AH}}$| and |${\mathsf{HLP}}$| are extensions of the Logic for Pragmatics , |$\mathcal{L}^P$|⁠. We compare |${\mathsf{AH}}$| and |$\mathsf{HLP}$|⁠. Then, we underline the expressive and inferential richness of both systems in dealing with hypothetical judgements, especially when based on different, sometimes conflicting, evidence. [ABSTRACT FROM AUTHOR]

From the technical point of view, philosophically neutral, the duality between a paraconsistent and a paracomplete logic (for example intuitionistic logic) lies in the fact that explosion does not hold in the former and excluded middle does not hold in the latter. From the point of view of the motivations for rejecting explosion and excluded middle, this duality can be interpreted either ontologically or epistemically. An ontological interpretation of intuitionistic logic is Brouwer's idealism; of paraconsistency is dialetheism. The epistemic interpretation of intuitionistic logic is in terms of preservation of constructive proof; of paraconsistency is in terms of preservation of evidence. In this paper, we explain and defend the epistemic approach to paraconsistency. We argue that it is more plausible than dialetheism and allows a peaceful and fruitful coexistence with classical logic. [ABSTRACT FROM AUTHOR]

We first define a language for the dialogical logic and the models that the language generates. This language is thought to capture the structure of the dialogues captured by Lekta—a software framework oriented to the design and implementation of natural language processing-related applications—and its users. These dialogues are defined as cooperative dialogues in which the dialogical logic perspective of a dialogue seen as a competition is shifted into a perspective in which both agents cooperate towards a common goal. Later we define a BDI temporal logic based on a modal framework that we will use to study the beliefs, desires and intentions of both agents based on the model generated by the dialogical logic. [ABSTRACT FROM AUTHOR]

Abductive problems and their solutions are presented by means of justification logic. We introduce additional meta-constructions in order to generate and compare different solutions to the same abductive problem. Our approach has three advantages: (i) it makes structurally explicit the solution to an abductive problem (as it has a syntactic nature); (ii) it gives a precise meaning to the notion of evidence; (iii) it provides clear definitions and procedures for the comparison of solutions that can be adapted to different needs. [ABSTRACT FROM AUTHOR]

Abductive conclusions are drawn in a special, co-hortative mood (Peirce's 'investigand'). Abductive conclusions are representative interpretants that represent abduction (or retroduction) as a form of reasoning that can convey a general conception of the truth. The truth is not asserted; abduction merely delivers the idea of a matter of course, rendering that idea comparatively simple and natural, hence assuring us of its justified assertibility. Hence abductive reasoning is at home in addressing 'How Possible'-questions in science. Abductive reasoning concerns the question of how things might, could or would conceivably be such that they can be plausibly asserted. Peirce took all reasoning to be diagrammatic and representable using the graphical method of logic. Yet no examples have previously been found in his large manuscript corpus of what such non-deductive graphs might look like. This paper proposes a new interpretation of a sole exception, a sketch of two graphs from a rejected page from 1903, which might be the only surviving example of Peirce's abductive graphs. The proposed interpretation takes them to be representative interpretants of this special inverse type of inference. [ABSTRACT FROM AUTHOR]

Most of the standard approaches consider abduction in terms of a backward reasoning and miss some of its fundamental features. Overall, they neglect its pragmatic dimension and the conjectural aspect of the conclusion. In this paper, we approach abduction in terms of strategic adjustment process in the context of dialogical logic. This sheds light on the use of conjectures in argumentative interactions. Although abductive dialogues are sometimes based upon sentential conjectures, they can also involve hypotheses about the context of argumentation itself. Indeed, the underlying logic of an argumentative interaction is not always settled since the beginning. In this context, abduction is not only concerned with the introduction of sentential hypotheses, but also with hypotheses concerning the structural rules governing the dialogue itself. We thus emphasize the instrumental dimension of abduction in dialogues. [ABSTRACT FROM AUTHOR]

It is known that many relevant logics can be conservatively extended by the truth constant known as the Ackermann constant. It is also known that many relevant logics can be conservatively extended by Boolean negation. This essay, however, shows that a range of relevant logics with the Ackermann constant cannot be conservatively extended by a Boolean negation. [ABSTRACT FROM AUTHOR]

Linear temporal logic (LTL) with Since and Until modalities is expressively equivalent, over the class of complete linear orders, to a fragment of first-order logic known as FOMLO (first-order monadic logic of order). It turns out that LTL, under some basic assumptions, is expressively complete if and only if it has the property, called separation, that every formula is equivalent to a Boolean combination of formulas that each refer only to the past, present or future. Herein we present simple algorithms and their implementations to perform separation of the LTL with Since and Until, over discrete and complete linear orders, and translation from FOMLO formulas into equivalent temporal logic formulas. We additionally show that the separation of a certain fragment of LTL results in at most a double exponential size growth. [ABSTRACT FROM AUTHOR]