PaperlayerView exact revision on arXiv

Source-linked AI summary

A Counterexample to KL1 Completeness and a Complete Disjunctive Calculus

Damiano Presa, Fabio Aurelio D'Asaro, Massimiliano Badino

arXiv:2610.37107v1cs.LO

TL;DR

KL1’s completeness was conjectured after its soundness had been established, but a four-rule counterexample shows that the original calculus misses an entailed permissive. The paper replaces may-trans’s single-intermediary condition with a disjunctive one and proves soundness for arbitrary rule sets and completeness for finite ones; it also establishes finite-set results for KL2.

  • Problem

    KL1’s calculus was proved sound, but its conjectured completeness—whether every rule entailed by unchanged outcomes is derivable—remained unproved.

    Source: §1 · p. 2

  • Method

    The paper proves non-derivability with an invariant, replaces may-trans’s single-intermediary condition with a disjunctive one, and uses a local characterization of entailment to establish the repaired calculus’s properties.

    Source: §1 · p. 2, §3 · p. 4, §4 · pp. 6–7

  • Results

    KL1’s conjecture fails: four rules entail a permissive absent from derivations, while the repaired calculus is sound for arbitrary sets and complete for finite ones.

    Source: §1 · p. 2, §10 · p. 15

  • Takeaways & Limitations

    For finite rule sets, KL2 with the disjunctive rule is sound and complete after its decomposition into KL1 is re-established.

    Source: §10 · p. 15

    The least-model characterization used in the completeness argument fails for some infinite rule sets, and the KL2 proofs are not mechanized and require independent review.

    Source: §6 · p. 11, §7 · p. 11

Abstract

from arXiv · show

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.

1 Introduction

KL1 treats Kant’s rules as imperatives and permissives over acts, with entailment defined by unchanged outcomes after adjoining a rule. The paper refutes the conjectured completeness of the original calculus and presents a disjunctive repair with soundness and finite-set completeness results.

1 Introduction

  • KL1 represents rules as conditional imperatives and permissives over acts, and answers operational questions through outcome sets.The inferential question is whether further rules may or must be adopted.Source: §1 · pp. 1–2
  • The original calculus was proved sound, but its completeness was only conjectured.The conjecture was supported by randomized testing.Source: §1 · p. 2
  • Four rules over three atoms entail a permissive that has no derivation, refuting the KL1 completeness conjecture.The non-derivability proof uses an invariant over arbitrary derivations.Source: §1 · p. 2
  • Replacing may-trans’s single-intermediary condition with a disjunctive condition yields a strict generalization from which the original rule is derivable.The repaired calculus is sound for arbitrary rule sets and complete for finite ones.Source: §1 · p. 2
  • The paper mechanizes its main KL1 results in Agda and proves finite-set soundness and completeness for KL2 with the disjunctive rule.The published KL2 reduction passes through infinite rule sets; the finite-set proofs are not mechanized and require independent review.Source: §1 · p. 2

2 Preliminaries

The preliminaries define KL1’s rules and outcome-based semantics, then specify entailment and the calculus whose completeness is at issue.

2.1 Syntax

  • Rules are imperatives or permissives with conjunctive bodies and disjunctive heads; rule sets may be infinite.Bodies and heads are finite sets of atoms, with ⊤ and ⊥ denoting the empty body and head.Source: §2.1 · p. 2

2.2 Operational semantics

  • The operational semantics builds candidate outcomes by adding rule-head acts from enabled rules, then retains those satisfying every imperative.Permissives and imperatives both generate acts, but only imperatives constrain outcomes.Source: §2.2 · p. 3

2.3 Entailment

  • A rule is entailed when adjoining it leaves the outcome set unchanged for every finite input.This is not ordinary model-theoretic consequence: adding a permissive can create a new outcome even if every set satisfies it.Source: §2.3 · p. 3

2.4 The inference rules

  • The calculus defines derivable rules as the least set containing the premises and closed under its inference rules.Derivations are finite trees, and may-trans requires a single intermediary imperative for each new act.Source: §2.4 · pp. 3–4
  • KL1’s completeness is stated as the conjecture that every semantically entailed rule is derivable.The displayed rules are reproduced from [2, Fig. 2].Source: §2.4 · p. 4, Figure 1 · p. 4

3 A Counterexample to the Completeness of KL1

A four-rule KL1 set entails a permissive that the original calculus cannot derive. An invariant proves non-derivability, pinpointing the single-intermediary side condition of may-trans.

3 A Counterexample to the Completeness of KL1

  • The four rules permit b or d, permit c after either, and require b or d whenever c is present; together they entail the permissive for c outright.The two rule sets have identical outcome sets for every input.Source: §3 · p. 4
  • The invariant constrains any derivable rule whose head contains c, including derivations using atoms beyond b, c, and d.It is proved by induction on derivations, not by restricting the search to the counterexample’s three atoms.Source: §3 · p. 5
  • The entailed permissive has no derivation, disproving KL1’s completeness conjecture with four rules over three atoms.The non-derivability proof uses an invariant over derivations.Source: §3 · pp. 5–6
  • The obstruction is may-trans’s demand for one intermediary: c is licensed alongside b or d, but neither is common to all models containing c.The disjunctive imperative c → b ∨ d holds, but the singleton side condition cannot use it.Source: §3 · p. 6

4 The Disjunctive Transitivity Rule

The section replaces may-trans’s single-intermediary side condition with a disjunctive one, allowing different outcomes to supply different intermediaries. The revised rule preserves the original rule and resolves the counterexample without changing the semantics.

4 The Disjunctive Transitivity Rule

  • may-trans-disj requires one imperative whose head is the disjunction of all intermediaries, rather than a separate single-intermediary condition.For each c in C, the side condition requires A ∧ c to imply that disjunction.Source: §4 · p. 6
  • In Example 12, the rules in R0 derive ⊤ ◇→ c by may-trans-disj, using c □→ b ∨ d as its side condition.The instance uses ⊤ ◇→ b ∨ d, b ◇→ c, and d ◇→ c.Source: §4 · p. 6
  • The original may-trans rule is derivable in the repaired calculus, while may-trans-disj is not admissible in the original calculus.The disjunctive rule therefore strictly extends the original proof system.Source: §4 · pp. 6–7
  • The repair changes only the proof system: it leaves the operational semantics unchanged, and the disjunctive rule is valid for that semantics.The authors note that the rule’s extra fan-out is redundant under the original single-intermediary side condition, but does genuine work with the disjunctive condition.Source: §4 · p. 7
  • The disjunctive side condition accommodates cases where c is accompanied by b in some models and d in others.The models {b, c} and {c, d} contain no single intermediary in common.Source: §4 · p. 7
  • The repair retains a protective condition: inferring a permission still requires an imperative linking the new act to the intermediary disjunction.For example, p ◇→ q and q ◇→ r alone do not meet the required condition for inferring p ◇→ r.Source: §4 · p. 7

5 Soundness

The section characterizes entailment using two local conditions on outcome sets, then uses that characterization to establish soundness of the repaired calculus. Soundness and closure hold for arbitrary rule sets.

5.1 A local characterization of entailment

  • For every rule set, permissive entailment is equivalent to PermR, while imperative entailment is equivalent to both ValidR and PermR.PermR requires that adding a head atom at a stage containing the body cannot produce a new outcome; ValidR requires every model containing the body to meet the head.Source: §5.1 · p. 8
  • The characterization shows that entailment depends only on the outcome function A ↦ out1(R, A), and adjoining an entailed rule leaves kl1(R) unchanged.The section’s local conditions are defined from that outcome function.Source: §5.1 · pp. 7–8

5.2 Soundness of the repaired calculus

  • The repaired calculus is sound for arbitrary rule sets, and its semantic consequences are closed under the inference rules.Theorem 17 establishes soundness when Q is a subset of kl1(R).Source: §5.2 · p. 8
  • The may-trans-disj soundness argument uses the side-condition imperative to find an intermediary in the outcome, then applies the premises to preserve the outcome inclusion.The proof does not require R to be finite or use definite-program semantics; it relies on positive bodies to assume an intermediary from the final outcome at the start.Source: §5.2 · p. 9
  • The least-model route does not extend to arbitrary rule sets because its least-model characterization fails for some infinite sets.Theorem 17 avoids this limitation.Source: §5.2 · p. 9

6 Completeness

For finite rule sets, the repaired calculus derives every semantically entailed rule, using finite successor sets and induction. The finite-set boundary is substantive: completeness fails for infinite sets under the finite-input reading.

6 Completeness

  • The completeness proof uses the finite set of one-step successors of A, which lies among the heads of R, to organize its induction.Adding a successor decreases the measure µ(S) used in the inductions.Source: §6 · p. 9
  • For finite R, semantic entailment implies derivability in the repaired calculus, and kl1(R) equals deriv∨1(R).The proof reduces permissives to singleton heads, derives those cases by induction, and combines them with may-union.Source: §6 · p. 10
  • The proof is constructive, uses only atoms in R or the target rule, and yields a model-existence equivalence for finite R.For finite R, having a model is equivalent to having a nonempty outcome set from the empty input.Source: §6 · p. 10
  • Completeness cannot extend to infinite rule sets under finite inputs: R∞ entails ⊤ □→ ⊥, but no finite derivation can establish it.Each finite subset of R∞ has an outcome from the empty input, whereas out1(R∞, A) is empty for every finite A.Source: §6 · p. 10
  • For finite R, entailment gives the same relation whether inputs range over finite or arbitrary atom sets.The passage states that Theorems 17 and 23 hold under either reading.Source: §6 · p. 11
  • The alternative least-model proof strategy relies on facts not established in the cited earlier work, including a characterization that fails for some infinite R.The paper also identifies the need to establish transfer of semantic entailment along inference rules.Source: §6 · p. 11

7 Mechanization

The paper formalizes its main KL1 results in Agda, but the mechanization covers statements rather than the informal proofs and does not include Section 8 or Appendix A.

7 Mechanization

  • The main KL1 results in Sections 2–6 are formalized in Agda 2.8.0, using safe mode and no postulates, holes, or disabled termination and positivity checks.The main file type-checks in about five seconds; a supplementary file covers arbitrary inputs and the rule set R∞.Source: §7 · p. 11
  • The formalization represents atoms as natural numbers and rule sets as membership predicates, with finiteness given by an explicit enumeration.Finite sets are represented canonically, and the original calculus is transcribed with may-trans side conditions as derivations of singleton imperatives.Source: §7 · p. 11
  • The mechanization covers theorem statements, not the informal arguments, and Corollary 24 is not itself stated in Agda.Remarks 10 and 26 and the non-derivability half of Remark 25 are also not mechanized.Source: §7 · p. 11
  • The guarantee depends on Agda's correctness and on the formal definitions faithfully matching those of; Section 8 and Appendix A are not mechanized.The paper's proofs follow the formal ones in outline but differ in some details.Source: §7 · pp. 11–12

8 Consequences for KL2 and KL3

The published KL2 reduction to KL1 passes through infinite rule sets, so the paper re-establishes the decomposition for finite sets and proves finite-set soundness and completeness for KL2 with the disjunctive rule. It leaves completeness of the original KL2 calculus and KL3 open.

8 Consequences for KL2 and KL3

  • The published KL2-to-KL1 reduction passes through infinite rule sets, so finite-set KL1 completeness cannot be applied directly to its intermediate set.The intermediate KL1 rule set includes a constraint for every atom.Source: §8.1 · pp. 12–13
  • The finite decomposition works with finitely many auxiliary rules whose members contain only literals over atoms occurring in the original KL2 rules.The paper establishes finiteness of the closure under resolution and of the resulting auxiliary rules.Source: §8.1 · p. 13
  • For every finite KL2 rule set, the calculus with the disjunctive rule is sound and complete.The finite-set decomposition into KL1 is re-established using only operational semantics.Source: §8.1 · p. 13
  • Theorem 31 is proved on paper only, and its proof still requires independent mathematical review.The proof uses the finite-set decomposition and the KL1 results; it is not mechanized.Source: §8.1 · pp. 13–14
  • The original KL2 calculus is sound for finite rule sets, but whether it is complete remains undetermined.The counterexample does not transfer immediately because the cited conservativity result's syntactic half relies on KL1 completeness.Source: §8.1 · p. 14
  • KL3 completeness remains open because existential witnesses remove the finiteness bounds used in the KL1 completeness proof.The relevant ground atoms can be unbounded, successor sets may be infinite, and the construction need not terminate.Source: §8.2 · p. 14

9 Philosophical Significance

The paper connects inferential reasoning about rules to the operational procedures they govern, arguing that completeness keeps those questions aligned within the results' scope. It also shows that finite-set model existence does not extend by compactness to arbitrary rule sets under the finite-outcome semantics.

9 Philosophical Significance

  • The counterexample concerns alternative grounds: every performance of c has a licensing act, but the act may be b or d.The disjunctive side condition preserves the requirement that c be grounded in a rule, while the original may-trans misses this pattern.Source: §9 · pp. 14–15
  • A sound and complete calculus makes reasoning about rules a faithful proxy for reasoning about the acts their procedures govern, within the theorems' scope.The operational question concerns acts permitted or required from a starting point; the inferential question concerns which rules follow.Source: §9 · pp. 14–15
  • For finite rule sets, consistency is equivalent to having an outcome, but a countable set may lack an outcome even when each finite subset has one.The compactness step fails because outcomes are finite packages of acts; these observations do not by themselves bear on transcendental idealism or a mind-independent world.Source: §9 · p. 15

10 Conclusion

The original KL1 calculus is incomplete because of may-trans’s singleton side condition; making it disjunctive yields a calculus sound for arbitrary rule sets and complete for finite ones. For KL2, the disjunctive calculus is sound and complete for finite rule sets.

10 Conclusion

  • The original KL1 calculus’s incompleteness comes from may-trans’s singleton side condition, which the disjunctive condition removes.The repaired calculus contains the original calculus and is sound for arbitrary rule sets and complete for finite ones.Source: §10 · p. 15
  • With finite inputs, completeness cannot extend to infinite rule sets under the operational semantics.The paper gives an example showing that no sound calculus with finite derivations can be complete for infinite rule sets.Source: §10 · p. 15
  • For finite rule sets, KL2’s decomposition into KL1 can be re-established, yielding a sound and complete KL2 calculus with the disjunctive rule.These KL2 proofs are not mechanized and require independent review.Source: §10 · p. 15

A Proofs for Section 8

The appendix proves semantic characterizations used in the finite-set KL2-to-KL1 decomposition. Its lemmas connect violating sets, outcomes, and resolution, then establish equivalence between the auxiliary rule sets used in the decomposition.

A Proofs for Section 8

  • Every maximal consistent set satisfying R also satisfies consistency rules C and the auxiliary rules aux(R).The flipping lemma supports the argument that auxiliary rules are satisfied by maximal consistent models.Source: A Proofs for Section 8 · p. 16
  • If a finite literal set is not violating, the augmented KL1 rule set reaches an outcome within the literals over the rule and input atoms.Consequently, if no augmented-rule model includes the input set, that set is violating.Source: A Proofs for Section 8 · pp. 16–17
  • For every finite literal set, KL2 has no outcomes exactly when the set is violating for the rule set.This characterization is used to relate entailment and violation in the finite-set decomposition.Source: A Proofs for Section 8 · p. 17
  • Resolution characterizes finite consistent violations: each such set includes a member of the resolved violation family, and every member of that family is violating.The result also implies that the extended auxiliary rules are included among the auxiliary rules.Source: A Proofs for Section 8 · p. 17
  • For finite KL2 rule sets, the appendix establishes both directions of the KL2-to-KL1 decomposition using the augmented rule set.The proof reduces the relevant entailment checks to finite violating sets.Source: A Proofs for Section 8 · p. 17
  • The auxiliary rule sets Ra and Re have the same outcomes, although Re is a subset of Ra.The proof derives the additional rules from Re and uses the finite trace of each outcome to establish equality.Source: A Proofs for Section 8 · pp. 17–18
Loading 2610.37107v1…