NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic

TL;DR

NM-DEKL$^3_ ty$ is a novel three-layer dependent type system designed to formalize evolving knowledge in dynamic environments, with rigorous semantics and expressiveness analysis.

Contribution

It introduces a new three-layer dependent type system with formal semantics, soundness, completeness, and an embedding into the $$-calculus, advancing formal reasoning about dynamic knowledge.

Findings

Established soundness and equational completeness of NM-DEKL$^3_ty$

Constructed a syntactic model that is initial in the category of models

Demonstrated the system's expressiveness, including non-bisimulation-invariant properties

Abstract

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 $\mu$-calculus and a strict expressiveness inclusion (including the expressibility of non-bisimulation-invariant properties).