Title: ZX-Calculus: Trace-Indexed Dependent Types and Epistemic Semantics

Abstract:

This paper introduces ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Löf Dependent Type Theory (MLTT). This framework synthesizes trace-indexed types, presheaf-based non-monotone semantics, and constructive AGM belief revision. The work is supported by a Coq mechanization featuring 34 fully completed proofs, with no admitted statements regarding the two central results.

(I) Trace Types. We define FinTrace(s0,sn) as an inductive family of typed execution traces. While FinTrace and Star(Step) are isomorphic as path types, they are not judgementally equal. The TraceElim constructor explicitly exposes the event label e:Event, providing a more ergonomic interface for event-driven induction. We establish the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework utilizing reducibility candidates and a Transport Lemma. Note that RC-elim is deferred; however, all other Core results are verified in Coq.

(II) Sheaf Semantics. Propositions indexed by traces are modeled as contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem, supported by an explicit countermodel, differentiates proof-theoretic monotonicity from semantic non-monotonicity. The term model serves as an initial CwF, characterized by a syntactic universal property rather than classical completeness.

(III) AGM Belief Revision. We present a constructive partial meet contraction algorithm, verified against conditions (C1)-(C4). All eight AGM postulates (R1)-(R8) are proven as theorems. Specifically, the proofs for R7 and R8 rely on the Disjunctive Entrenchment Lemma, which is derived constructively and self-containedly within this work.

(IV) Integration. We demonstrate that B^AGM fails the sheaf composition law BP-comp for sequential revision, a fact confirmed by an explicit countermodel and Coq verification. To address this, we introduce Single-Step Revision Systems (SSRS), proving that B^AGM constitutes a valid SSRS (also Coq-verified). This validity is sufficient to support trace morphisms, retraction characterization, and revision witnesses. The failure of BP-comp highlights a fundamental, previously unidentified tension between path-dependent belief revision and functor consistency.

Source: arXiv Generated at: 2026-06-03 00:00:00 UTC