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

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
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

KM Construction–Temporal Logic: Finite Stages, Suspension, and Proposition-Specific Proof Methods

Kianming(Jianming) Wang
Zenodo (CERN European Organization for Nuclear Research)
Formal Methods in Verification
preprint

KM Construction–Temporal Logic: Finite Stages, Suspension, and Proposition-Specific Proof Methods

Kianming(Jianming) Wang
preprint en

Abstract

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.

Zenodo (CERN European Organization for Nuclear Research)
Peace, Justice and strong institutions
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.