Axiom Dynamics 3: Conservativeness and Invariance Rigidity—Dual Conditions for the Legitimacy of Axiom Transitions

Changes of the rule set of an axiom system—expansion, contraction, and revision—change the theorem set in the closure, but “what a change must preserve and whatit must gain” has previously lacked a machine-checkable compositional criterion.This paper establishes, on a finite Horn deductive system, an object-level three-waydecomposition ledger for transitions: any rule-set change induces a theorem set T toT′, and the difference is decomposed into the object-level gain set Gainobj = T′,the loss set Loss = T \ T′, and the invariant set Inv = T ∩ T′. The three-waydecomposition is complete and pairwise disjoint. Legitimacy is decided by a dualcondition: the protection core Core ⊆ Inv (Condition 1, losslessness), and Gainobjor meta-level gain Gainmeta is nonempty (Condition 2, gainfulness). Failure ofCondition 1 is an immediate veto and is not compensated by Condition 2 or bysyntactic-level gains; after Condition 1 holds, Condition 2 can fail independently.The criterion for meta-level gain is based on the carrier function Car(P,S): aproperty P constitutes meta-level gain if and only if P holds in the post-changesystem, its carrier is nonempty, and it belongs to Type A genuine acquisition (Phad a carrier before the change but did not hold) or Type B level addition (P hadno applicable carrier before the change and acquires a carrier after the change).Type B must be marked “level addition.” The termination of closure computationhas carriers and holds at both ends of the change and is not counted as meta-levelgain; savings in derivation depth and description length belong to the syntactic-levelledger and are also not counted.On the finite Horn fragment, universal conservativeness (closure equality for every fact set) is equivalent to redundancy (the conclusion of a rule is already derivablefrom its premises via existing rules). This equivalence is proved by syntactic induction and recomputed by full enumeration with seven atoms, a six-rule baseline, 448candidate rules, and 128 fact sets, with zero counterexamples. Universal conservativeness is the syntactic counterpart of deductive conservativeness at the level of ruleredundancy, not an equivalent of the model-expansion property; model expansionimplies deductive conservativeness, but the converse generally fails. Fixed-fact-setconservativeness for rule incorporation holds automatically by monotonicity andprovides no detection power; the two readings are distinguished by qualifiers andare not conflated.Membership rigidity resides in the layer of theorem-set membership, not in thesyntactic layer. Chain–star rewiring, with the empty fact input as baseline, keepsthe theorem set pointwise invariant; the syntactic ledger is the same, 15, the sumsof shortest derivation depths are 28 and 7 respectively, and the two-stage totalledgers are 43 and 22 respectively. This case displays the separation between themembership layer and the syntactic layer, and does not by itself constitute a positiveverdict of legitimacy: its object-level gain is empty, and the depth saving does notsatisfy Condition 2. The condition for membership rigidity is closure preservation;if a rule transition causes some atom to fall into Loss, rigidity does not apply, andthe dual-condition verdict must be entered. If a falsifiable prediction is registeredas a member of the theorem set, a closure-preserving rule reorganization does notchange its membership; changes of the fact set are not within the jurisdiction ofthe three-way decomposition, and under forward-chaining Horn semantics fact-setexpansion is monotonically nondecreasing, so empirical-level elimination must beborne by fact-set contraction, fact replacement, or rule change.The four types of verdicts show the logical independence of the two branches:an uncompensated contraction dies by Condition 1 because Loss touches the protection core; a compensated revision keeps the theorem set unchanged but hasno object-level gain and no meta-level gain satisfying the carrier condition, anddies by Condition 2; an object-level genuine expansion bears Condition 2 throughnew theorems; the incorporation of a meta-rule bears Condition 2 through Type Blevel-addition meta-level gain, and its legitimacy depends on the meta-rule indeedintroducing a candidate-selection operator in the rule-application semantics. Whatis determinately established is the completeness of the three-way decomposition, theconjunctive structure of the dual condition, the logical independence of Condition 1and Condition 2, the equivalence of universal conservativeness and redundancy onthe finite Horn fragment, and the above stratified readings; what is open or to beverified is the membership of the list of meta-level properties, the boundary of thecarrier function in real theories, the theory of choice of Core, and the interactionbetween the dual condition and derivation-cycle theorems. The legitimacy criterion and the timing criterion apply independently: legitimate does not equal worthmaking, and worth making does not equal legitimate.