Nonmonotonic and normative reasoning: a unified proof-theoretic framework

Rational agents are mostly located in dynamic environments, thereby handling incomplete information concerning the world and the rules that should govern their behavior. When elaborating such incomplete information, agents reach defeasible conclusions, that may be withdrawn when further information is available. Nonmonotonic logics are designed with the aim of modeling this mode of reasoning. This dissertation investigates different kinds of nonmonotonic logic through the lens of structural proof-theory. Specifically, the thesis proposes a uniform proof-theoretic platform for monotonic and nonmonotonic extensions of classical propositional logic, based on combinations of sequents and antisequents (i.e., sequents for underivability) framed in suitable Gentzen-style calculi. The first case study is abductive reasoning, defined as the search for the missing premise in a deductively invalid argument. For any given abductive problem, we provide a syntactical procedure to generate an expected solution which does not coincide with the deductively minimal one, and which is a natural candidate for being the result of an inference to the best explanation. Next, we introduce the notion of hybrid hypersequent, where sequents and antisequents are composed in parallel to provide contrary updating on the derivation of the conclusion. We show that hybrid hypersequents are flexible enough to provide (weakly) analytic calculi for a number of logics for nonmonotonic and normative reasoning: default logics, a weak version of preferential logic R corresponding to base-generated belief revision, constrained I/O logics. Crucially, this proof-theoretic approach does not rely on ad hoc extensions of the underlying language to formalize extra-logical rules. Lastly, we present a modified notion of controlled sequent, where the turnstile is annotated with sets of formulas to prescribe what should or should not be entailed by the formulas in the antecedent. We introduce controlled sequent calculi for deontic reasoning grounded in default logic, showing that the introduction of suitable extra-logical rules permits to navigate paradoxical, dilemmatic or dynamic deontic scenarios in accordance with their intuitive assessment.