This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.

A unified and modular falsification-aware single-succedent Gentzen-style framework is introduced for classical, paradefinite, paraconsistent, and paracomplete logics. This framework is composed of two special inference rules, referred to as the rules of explosion and excluded middle, which correspond to the principle of explosion and the law of excluded middle, respectively. Similar to the cut rule in Gentzen’s LK for classical logic, these rules are admissible in cut-free LK. A falsification-aware single-succedent Gentzen-style sequent calculus fsCL for classical logic is formalized based (...) on the proposed framework. The calculus fsCL is obtained from the existing falsification-aware single-succedent Gentzen-style sequent calculus GN4 for Nelson’s paradefinite (or paraconsistent) four-valued logic N4 by adding the rules of explosion and excluded middle. A falsification-aware single-succedent Gentzen-style sequent calculus GN3 for Nelson’s paracomplete three-valued logic N3 is also obtained from GN4 by adding the rule of explosion. The cut-elimination theorems for fsCL, GN3, and some of their neighbors as well as the Glivenko theorem for fsCL are proved. (shrink)

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. (shrink)

The strong normalization theorem is uniformly proved for typed λ-calculi for a wide range of substructural logics with or without strong negation.