Analytic Proof Theory for Aqvist's System F

Abstract

The key strength of preference-based logics for conditional obligation is their ability to handle contrary-to-duty paradoxes and account for exceptions. Here we investigate Åqvist’s system F, a well-known logic in this family. F has the notable feature that every satisfiable formula has a “best” element. Thus far, the only proof system for F was a Hilbert calculus, impeding applications and deeper investigations. We fill this gap, constructing the first analytic calculus for F. The calculus possesses good proof-theoretical properties—in particular, cut-elimination, which greatly facilitates proof search. Our calculus is used to provide explanations of logical consequences, as a decision-making tool, and to obtain a preliminary complexity upper bound for F (giving a theoretical limit on its automated behavior).