Recent zbMATH articles in MSC 03B20https://zbmath.org/atom/cc/03B202022-11-17T18:59:28.764376ZWerkzeugA reconstruction of ex falso quodlibet via quasi-multiple-conclusion natural deductionhttps://zbmath.org/1496.030292022-11-17T18:59:28.764376Z"Fukuda, Yosuke"https://zbmath.org/authors/?q=ai:fukuda.yosuke"Igarashi, Ryosuke"https://zbmath.org/authors/?q=ai:igarashi.ryosukeSummary: This paper is intended to offer a philosophical analysis of the propositional intuitionistic logic formulated as NJ. This system has been connected to Prawitz and Dummett's proof-theoretic semantics and its computational counterpart. The problem is, however, there has been no successful justification of ex falso quodlibet (EFQ): ``From the absurdity ``\(\bot\)'', an arbitrary formula follows''. To justify this rule, we propose a novel intuitionistic natural deduction with what we call quasi-multiple conclusion. In our framework, EFQ is no longer an inference deriving everything from ``\(\bot\)'', but rather represents a ``jump'' inference from the absurdity to the other possibility.
For the entire collection see [Zbl 1369.68010].Subatomic negationhttps://zbmath.org/1496.030302022-11-17T18:59:28.764376Z"Więckowski, Bartosz"https://zbmath.org/authors/?q=ai:wieckowski.bartoszSummary: The operators of first-order logic, including negation, operate on whole formulae. This makes it unsuitable as a tool for the formal analysis of reasoning with non-sentential forms of negation such as predicate term negation (e.g., negatively affixed gradable adjectives). We extend its language with negation operators whose scope is more narrow than an atomic formula. Exploiting the usefulness of subatomic proof-theoretic considerations for the study of subatomic inferential structure, we define intuitionistic subatomic natural deduction systems which have several subatomic operators and an additional operator for formula negation at their disposal. We establish normalization and subexpression (resp. subformula) property results for the systems. The normalization results allow us to formulate a proof-theoretic semantics for formulae composed of the subatomic operators. We illustrate the systems with applications to reasoning with combinations of sentential negation, predicate term negation (of adjectives, verbs, and common nouns), subject term negation, and antonymy.A forward unprovability calculus for intuitionistic propositional logichttps://zbmath.org/1496.030432022-11-17T18:59:28.764376Z"Fiorentini, Camillo"https://zbmath.org/authors/?q=ai:fiorentini.camillo"Ferrari, Mauro"https://zbmath.org/authors/?q=ai:ferrari.mauroSummary: The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. This method has been successfully applied to a variety of logics. Here we apply this method to derive the unprovability of a goal formula \(G\) in Intuitionistic Propositional Logic. To this aim we design a forward calculus \(\mathbf {FRJ}(G) \) for Intuitionistic unprovability. From a derivation of \(G\) in \(\mathbf {FRJ}(G) \) we can extract a Kripke countermodel for \(G\). Since in forward methods sequents are not duplicated, the generated countermodels do not contain redundant worlds and are in general very concise.
For the entire collection see [Zbl 1371.68015].Non-clausal connection calculi for non-classical logicshttps://zbmath.org/1496.030492022-11-17T18:59:28.764376Z"Otten, Jens"https://zbmath.org/authors/?q=ai:otten.jensSummary: The paper introduces non-clausal connection calculi for first-order intuitionistic and several first-order modal logics. The notion of a non-clausal matrix together with the non-clausal connection calculus for classical logic are extended to intuitionistic and modal logics by adding prefixes that encode the Kripke semantics of these logics. Details of the required prefix unification and some optimization techniques are described. Furthermore, compact Prolog implementations of the introduced non-classical calculi are presented. An experimental evaluation shows that non-clausal connection calculi are a solid basis for proof search in these logics, in terms of time complexity and proof size.
For the entire collection see [Zbl 1371.68015].On the concept of a notational varianthttps://zbmath.org/1496.030832022-11-17T18:59:28.764376Z"Kocurek, Alexander W."https://zbmath.org/authors/?q=ai:kocurek.alexander-wSummary: In the study of modal and nonclassical logics, translations have frequently been employed as a way of measuring the inferential capabilities of a logic. It is sometimes claimed that two logics are ``notational variants'' if they are translationally equivalent. However, we will show that this cannot be quite right, since first-order logic and propositional logic are translationally equivalent. Others have claimed that for two logics to be notational variants, they must at least be compositionally intertranslatable. The definition of compositionality these accounts use, however, is too strong, as the standard translation from modal logic to first-order logic is not compositional in this sense. In light of this, we will explore a weaker version of this notion that we will call schematicity and show that there is no schematic translation either from first-order logic to propositional logic or from intuitionistic logic to classical logic.
For the entire collection see [Zbl 1369.68010].A basic dual intuitionistic logic and some of its extensions included in \(\mathrm{G}3_{\mathrm{DH}}\)https://zbmath.org/1496.031102022-11-17T18:59:28.764376Z"Robles, Gemma"https://zbmath.org/authors/?q=ai:robles.gemma"Méndez, José M."https://zbmath.org/authors/?q=ai:mendez.jose-manuel|mendez.jose-mSummary: The logic DHb is the result of extending Sylvan and Plumwood's minimal De Morgan logic \(\mathrm{B}_{\mathrm{M}}\) with a dual intuitionistic negation of the type Sylvan defined for the extension \(\mathrm{CC}\omega\) of da Costa's paraconsistent logic \(\mathrm{C}\omega \). We provide Routley-Meyer ternary relational semantics with a set of designated points for DHb and a wealth of its extensions included in \(\mathrm{G3}_{\mathrm{DH}}\), the expansion of \(\mathrm{G3}_+\) with a dual intuitionistic negation of the kind considered by Sylvan \((\mathrm{G3}_+\) is the positive fragment of Gödelian 3-valued logic G3). All logics in the paper are paraconsistent.