An Intrinsic Additive Quotient for Classical Propositional Logic

We isolate a canonical additive quotient associated with classical propositional logic. The construction starts from canonical proof decomposition in fractional semantics: to each formula A we associate the pair Ev(A)=(Id(A),Def(A)) Ev ( A ) = ( Id ( A ) , Def ( A ) ) , where Id(A) Id ( A ) and Def(A) Def ( A ) count, respectively, identity and complementary top-sequents in its canonical decomposition. Equality of these pairs, A≡ EvB A ≡ Ev B iff Ev(A)=Ev(B) Ev ( A ) = Ev ( B ) , induces an equivalence relation on formulas, and conjunction descends to the resulting quotient, yielding a commutative semigroup. The semigroup turns out to be free commutative on two generators. After adjoining an identity element, it becomes isomorphic to (N²,+) ( N 2 , + ) ; in particular, every nonzero pair of natural numbers occurs as (Id(A),Def(A)) ( Id ( A ) , Def ( A ) ) for some classical formula. This gives a canonical normal form for each equivalence class. Along the way, the defect coordinate yields a new single-clause route to Post-completeness. At the metatheoretic level, the first-order theory of the resulting monoid reduces effectively to Presburger arithmetic, and universal affine inequalities in the two coordinates admit an explicit validity criterion. The usual fractional value is recovered by normalizing these two counts. Although the quotient is intrinsically conjunctive, its disjunctive boundary can be characterized exactly by the reduced clause spectrum. Unlike the Lindenbaum–Tarski quotient, the evidence quotient retains multiplicity information while forgetting some literal information. The defect coordinate induces a discrete Lawvere cost semantics and the associated Lawvere quasi-metric geometry.