KM Construction–Temporal Logic: Finite Stages, Suspension, and Proposition-Specific Proof Methods
We introduce KM construction–temporal logic, a finite-stage proof framework defined relative to an ambient model \(\mathcal M\models\mathrm{ZFC}\). A KM system is not a finite model of ZFC. It is a directed family \[ \mathfrak K= \langle K_r,\iota_{rs},\operatorname{Born},\operatorname{Dep}, \Vdash_r\rangle_{r\le s<\omega}, \] where every \(K_r\) is a finite coded structure and \[ K_\infty=\varinjlim K_r \] represents potential infinity. Stage evaluation is three-valued: \[ \operatorname{Val}_r(\varphi)\in \{\mathbf T,\mathbf F,\mathbf U\}, \] where \(\mathbf U\) denotes undefinedness or suspension and is distinct from falsity. Every admitted derivation has a finite labelled dependency graph, and every genuine construction object has a birth stage. An indispensable occurrence of an object before its birth is suspended. Historical non-retroactivity prevents a later construction from repairing such an occurrence, while dependency-local propagation confines invalidity to genuine dependency paths. The central result, the fundamental theorem of construction, states that \[ \operatorname{Valid}(D)\Longrightarrow \forall r\forall u\, \bigl( \operatorname{IndOcc}_D(r,u) \Rightarrow \operatorname{Born}(u)\le r \bigr). \] Consequently, one indispensable future call suffices to invalidate a finite derivation; no infinite illegal chain is required. The associated proposition-specific method consists of an enterability test, constructivization, a suspension test, extraction of a minimal illegal core, and reverse determination. When no essential suspension is obtained, the proof obligation returns to induction, recursion, finite descent, or another appropriate mathematical method. The framework supplies no universal truth algorithm: every application must independently construct a finite failure record, a genuine suspended object, its birth stage, its indispensable dependency path, and its minimal illegal core. The first twenty-eight chapters develop the general syntax, semantics, dependency theory, suspension calculus, soundness, refinement invariance, direct limits, and the complementary relation with induction. The final eight chapters examine dynamic primality and several number-theoretic conjectures as proposition-specific audits. Dynamic primality is established by finite verification. For RH, GRH, Twin, Goldbach, Legendre, abc, and BSD, the paper identifies finite interfaces and the precise additional analytic or arithmetic bridges that would be required; it does not claim that finite-stage legality alone proves these conjectures. **Keywords** KM construction–temporal logic; finite-stage semantics; ZFC-relative construction; potential infinity; three-valued semantics; dependency graphs; birth stages; partial evaluation; suspension; historical non-retroactivity; minimal illegal cores; mathematical induction; proposition-specific proof methods; arithmetic applications.
Authors
- Kianming(Jianming) Wang
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-08-21
- DOI
- https://doi.org/10.5281/zenodo.22049648
- Primary Topic
- Formal Methods in Verification
- Type
- preprint