Kant's logic rules revised to fix completeness flaw in reasoning system
A Counterexample to KL1 Completeness and a Complete Disjunctive Calculus
Logic in Computer Science
Summary
The paper investigates a formal system that turns Kant's philosophical rules into logic about actions. The original system was thought to be complete, meaning it could derive all truths about these rules, but the authors found a specific example where it fails. They fixed the problem by adjusting a key inference rule to allow for more flexible reasoning. This fix makes the system work properly for all finite cases and also applies to an extended version of the logic. The results are formally checked with a proof assistant to ensure correctness.
What this means in practice
- •For automated reasoning developers: Improve rule-based reasoning engines that model conditional permissions and obligations by adopting the corrected inference rule for sound and complete derivations on finite rule sets.
- •For formal methods engineers: Implement formal verification tools relying on Kantian logic frameworks more reliably by using the revised calculus with disjunctive inference to ensure correctness in decision systems.
Authors
Damiano Presa, Fabio Aurelio D'Asaro, Massimiliano Badino
Abstract
The logic KL$_1$ of Evans, Sergot and Stephenson formalizes Kant's rules as conditional imperatives $B \square\to C$ and permissives $B \diamond\to C$ over acts. Its consequence relation is operational: a rule follows from a set of rules when adjoining it leaves the set of outcomes unchanged for every input. The authors proved their calculus sound and conjectured that it is complete. We show that the conjecture fails: for distinct atoms $b,c,d$ the rules $\top \diamond\to b \lor d$, $b \diamond\to c$, $d \diamond\to c$ and $c \square\to b \lor d$ entail $\top \diamond\to c$, which is not derivable. Non-derivability is proved by an invariant that holds at every derivation depth and for arbitrary intermediate atoms. The obstruction is the side condition of may-trans, which requires each new act to bring with it a single intermediary act. Replacing it by a disjunctive side condition yields may-trans-disj, a strict generalization from which the original rule is derivable. Using a local characterization of entailment, we prove the repaired calculus sound for arbitrary sets of rules and complete for finite ones, and we show that, with finite inputs, completeness cannot be extended to infinite sets. The main results on KL$_1$ are formalized in Agda. For KL$_2$ we observe that the published reduction to KL$_1$ passes through infinite rule sets; re-establishing the decomposition for finite rule sets, we prove that KL$_2$ with the disjunctive rule is sound and complete for finite sets of rules. We close with remarks on KL$_3$ and on the significance of completeness for the relation between the operational and the inferential questions of Kant's logic.