NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic
This work addresses a foundational issue in formal logic and type theory for dynamic systems, but it appears incremental as it builds on existing dependent type systems.
The paper tackles the problem of formalizing evolving knowledge in dynamic environments by introducing a new dependent type system, NM-DEKL$^3_\infty$, which uses a three-layer architecture and establishes soundness and equational completeness.
We present a new dependent type system, NM-DEKL$^3_\infty$ (Non-Monotone Dependent Knowledge-Enhanced Logic), for formalising evolving knowledge in dynamic environments. The system uses a three-layer architecture separating a computational layer, a constructive knowledge layer, and a propositional knowledge layer. We define its syntax and semantics and establish Soundness and Equational Completeness; we construct a syntactic model and prove that it is initial in the category of models, from which equational completeness follows. We also give an embedding into the $μ$-calculus and a strict expressiveness inclusion (including the expressibility of non-bisimulation-invariant properties).