An erotetic calculus for a given logic constitutes a sequent-style proof-theoretical formalization of the logic grounded in Inferential Erotetic Logic ). In this paper, a new erotetic calculus for Classical Propositional Logic ), dual with respect to the existing ones, is given. We modify the calculus to obtain complete proof systems for the propositional part of paraconsistent logic CLuN and its extensions CLuNs and mbC. The method is based on dual resolution. Moreover, the resolution rule is non-clausal. According to the (...) authors knowledge, this is the first account of resolution for mbC. Last but not least, as the method is grounded in IEL, it constitutes an important tool for the so-called question-processing. (shrink)

We define Kripke semantics for propositional intuitionistic logic with Suszko’s identity. We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko’s propositional identity connective.

In this paper we are applying certain strategy described by Negri and Von Plato :418–435, 1998), allowing construction of sequent calculi for axiomatic theories, to Suszko’s Sentential calculus with identity. We describe two calculi obtained in this way, prove that the cut rule, as well as the other structural rules, are admissible in one of them, and we also present an example which suggests that the cut rule is not admissible in the other.

In this paper we are applying certain strategy described by Negri and Von Plato :418–435, 1998), allowing construction of sequent calculi for axiomatic theories, to Suszko’s Sentential calculus with identity. We describe two calculi obtained in this way, prove that the cut rule, as well as the other structural rules, are admissible in one of them, and we also present an example which suggests that the cut rule is not admissible in the other.

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated \(\mathsf {ND}^1_{\mathsf {ISCI}}\) and a semantically motivated \(\mathsf {ND}^2_{\mathsf {ISCI}}\). The formulation of \(\mathsf {ND}^1_{\mathsf {ISCI}}\) is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, but due (...) to the normalization procedure non-subformulas can label only leaves of proofs. In \(\mathsf {ND}^2_{\mathsf {ISCI}}\), we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic. (shrink)

The aim in this paper is to define an Abductive Question-Answer System for the minimal logic of formal inconsistency \. As a proof-theoretical basis we employ the Socratic proofs method. The system produces abductive hypotheses; these are answers to abductive questions concerning derivability of formulas from sets of formulas. We integrated the generation of and the evaluation of hypotheses via constraints of consistency and significance being imposed on the system rules.

This paper presents Rasiowa–Sikorski deduction systems for logics \, \, \ and \. For each of the logics two systems are developed: an R–S system that can be supplemented with admissible cut rule, and a \-version of R–S system in which the non-admissible rule of cut is the only branching rule. The systems are presented in a Smullyan-like uniform notation, extended and adjusted to the aims of this paper. Completeness is proved by the use of abstract refutability properties which are (...) dual to consistency properties used by Fitting. Also the notion of admissibility of a rule in an R–S-system is analysed. (shrink)