Analytic Proof Theory for Aqvist's System F

The key strength of preference-based logics for conditional obligation is their abilityto handle contrary-to-duty paradoxes and account for exceptions. Here we investigate˚Aqvist’s system F, a well-known logic in this family. F has the notable feature thatevery satisfiable formula has a “best” element. Thus far, the only proof system forF was a Hilbert calculus, impeding applications and deeper investigations. We fillthis gap, constructing the first analytic calculus for F. The calculus possesses goodproof-theoretical properties—in particular, cut-elimination, which greatly facilitatesproof 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).