← Archive
lm-002927 · 2026-08

判斷狀態機的形式語義與轉移公理

zh-Hant · md Raw source ↗ Metadata ↗
下載 MD 檔 ⬇

判斷狀態機的形式語義與轉移公理

動態邏輯解與生成判斷系列・第八篇

英文題名： Formal Semantics and Transition Axioms for Judgment State Machines
版本： v0.1
日期： 2026-08-16
作者： Neo.K／Aletheia

摘要

前七篇已建立：判斷具有時間、解可以是一條狀態路徑、 Ω\Omega 是合法未閉合判斷態、動態不動點保存跨狀態不變量、可不可論治理可生成與不可生成轉移，以及暫時閉合後仍需承擔責任。

本文進一步將上述概念收斂成一個最小「判斷狀態機」（Judgment State Machine, JSM）。JSM 並不企圖取代既有 Dynamic Logic、Dynamic Epistemic Logic、Belief Revision、Truth Maintenance System 或 non-monotonic logic；它的工作是把「判斷 runtime」明確變成可執行狀態轉移系統。

定義：

J=(S,E,δ,Π,Θ,I,H)\boxed{ \mathfrak J = ( \mathcal S, \mathcal E, \delta, \Pi, \Theta, \mathcal I, \mathcal H ) }

其中：

  • S\mathcal S：判斷狀態集合；
  • E\mathcal E：事件集合；
  • δ\delta：狀態轉移函數；
  • Π\Pi：對外投影；
  • Θ\Theta：閉合／重開政策；
  • I\mathcal I：必須保持的不變量；
  • H\mathcal H：事件歷史。

本文提出五類核心狀態：

S={O,G,C,Tp,Fp},\mathcal S = \{ O,G,C,T_p,F_p \},

分別表示 open、generating、conflicted、provisionally true、provisionally false；另將 runtime error 放在不同型別：

ERROR∉S.\mathrm{ERROR}\notin\mathcal S.

對外三態投影：

Π3(S)={⊤,S=Tp,⊥,S=Fp,Ω,S∈{O,G,C}.\Pi_3(S)= \begin{cases} \top,&S=T_p,\\ \bot,&S=F_p,\\ \Omega,&S\in\{O,G,C\}. \end{cases}

如此可在不把 Ω\Omega 誤當第三 truth value 的前提下，給它一個可執行形式。

一、為什麼需要狀態機

若只寫：

J(P,t),J(P,t),

仍未指定：

  • 合法狀態有哪些；
  • 哪些事件可以改變狀態；
  • 哪些轉移被禁止；
  • 何時 closure；
  • 何時 reopen；
  • 何時只是 runtime failure。

因此需要明確：

St→etSt+1.S_t \xrightarrow{e_t} S_{t+1}.

二、最小狀態集合

本文第一版使用：

S={O,G,C,Tp,Fp}.\boxed{ \mathcal S = \{ O,G,C,T_p,F_p \}. }

OO — Open

命題已被建立，但尚未進入足夠研究活動。

GG — Generating

正在取得證據、分裂假說、計算或比對。

CC — Conflicted

存在重大支持與反證衝突，不能直接閉合。

TpT_p — Provisionally True

目前政策允許暫時閉合為支持。

FpF_p — Provisionally False

目前政策允許暫時閉合為反對。

三、Error 必須另外分型

定義 runtime status：

Rt∈{OK,BLOCKED,ERROR}.R_t \in \{ \mathrm{OK}, \mathrm{BLOCKED}, \mathrm{ERROR} \}.

判斷狀態：

StS_t

與 runtime status：

RtR_t

互相獨立。

因此可以：

St=G,Rt=BLOCKED,S_t=G, \quad R_t=\mathrm{BLOCKED},

表示：

判斷仍在生成，但目前某工具／權限被阻擋。

不能把它直接投影成：

Ω=ERROR.\Omega=\mathrm{ERROR}.

四、事件集合

最小事件集合：

E={eclaim,e+,e−,einvalidate,econtext,emodel,eclose+,eclose−,ereopen,esplit}.\mathcal E = \{ e_{\mathrm{claim}}, e_{+}, e_{-}, e_{\mathrm{invalidate}}, e_{\mathrm{context}}, e_{\mathrm{model}}, e_{\mathrm{close+}}, e_{\mathrm{close-}}, e_{\mathrm{reopen}}, e_{\mathrm{split}} \}.

分別表示：

  • 建立命題；
  • 支持證據；
  • 反證；
  • 證據失效；
  • 語境變更；
  • 模型變更；
  • 暫時支持閉合；
  • 暫時反對閉合；
  • 重開；
  • 假說分裂。

五、轉移函數

定義：

δ:S×E×Θ→S.\delta: \mathcal S\times\mathcal E\times\Theta \rightarrow \mathcal S.

例如：

δ(O,e+,Θ)=G.\delta(O,e_+,\Theta)=G.

支持證據不應直接：

O→TpO\rightarrow T_p

除非 closure policy 明確允許。

六、閉合公理

公理 J1：閉合必須顯式

若：

St∈{O,G,C},S_t\in\{O,G,C\},

只有在：

Close⁡Θ(St,E≤t)=1\operatorname{Close}_{\Theta}(S_t,E_{\leq t})=1

時，才能：

St+1∈{Tp,Fp}.S_{t+1}\in\{T_p,F_p\}.

不能因畫面停止更新而默認 closure。

七、重開公理

公理 J2：重大新資訊必須能觸發重開

若：

St∈{Tp,Fp}S_t\in\{T_p,F_p\}

且：

Δ(enew,St)>ρ,\Delta(e_{new},S_t)>\rho,

則：

δ(St,enew,Θ)∈{G,C}.\delta(S_t,e_{new},\Theta) \in \{G,C\}.

因此：

Closure≠Irreversible Finality.\boxed{ \text{Closure} \neq \text{Irreversible Finality}. }

八、歷史保存公理

公理 J3：任何有效轉移不得覆寫前一狀態的存在事實

令：

Ht=(e1,…,et).\mathcal H_t = (e_1,\ldots,e_t).

則：

Ht≺Ht+1.\mathcal H_t \prec \mathcal H_{t+1}.

也就是 event log 單調延伸。

狀態可以反轉，事件歷史不能被靜默刪除。

九、證據來源公理

公理 J4：推論不可冒充觀測

對任何 evidence object：

Ei,E_i,

必須具有 source class：

SourceType⁡(Ei)∈{observation,document,derived,inference}.\operatorname{SourceType}(E_i) \in \{ \text{observation}, \text{document}, \text{derived}, \text{inference} \}.

若：

SourceType⁡(Ei)=inference,\operatorname{SourceType}(E_i)=\text{inference},

不得被重新標成 observation 只因模型信心高。

十、閉合不等於真值公理

公理 J5

St=TpS_t=T_p

只推出：

PolicyClosedSupport⁡(P,t)=1.\operatorname{PolicyClosedSupport}(P,t)=1.

不推出：

V(P,W)=⊤V(P,W)=\top

作為形上學定理。

同理：

FpF_p

也只是目前閉合結果。

十一、三態投影

定義：

Π3:S→{⊤,⊥,Ω}.\boxed{ \Pi_3: \mathcal S \rightarrow \{\top,\bot,\Omega\}. } Π3(O)=Ω,\Pi_3(O)=\Omega, Π3(G)=Ω,\Pi_3(G)=\Omega, Π3(C)=Ω,\Pi_3(C)=\Omega, Π3(Tp)=⊤,\Pi_3(T_p)=\top, Π3(Fp)=⊥.\Pi_3(F_p)=\bot.

這裡：

⊤,⊥\top,\bot

都是 judgment projection。

不是直接宣稱 world truth value。

十二、Bayesian 投影

同一個 JSM 可以另外投影：

ΠB(St,Et)=(pt,qt,kt)\Pi_B(S_t,E_t) = ( p_t, q_t, k_t )

其中：

  • ptp_t：support score / posterior；
  • qtq_t：counterpressure；
  • ktk_t：evidence completeness。

所以：

Π3≠ΠB.\boxed{ \Pi_3 \neq \Pi_B. }

一個是狀態投影，一個是數值投影。

十三、可不可投影

還可以：

ΠC(St)=(Cant,Cannott).\Pi_C(S_t) = ( \mathsf{Can}_t, \mathsf{Cannot}_t ).

例如：

St=CS_t=C

時：

Cant={search,split,review},\mathsf{Can}_t = \{ \text{search}, \text{split}, \text{review} \}, Cannott={finalize}.\mathsf{Cannot}_t = \{ \text{finalize} \}.

十四、非法轉移

例如：

Tp→no eventFpT_p \xrightarrow{\text{no event}} F_p

應被禁止。

因為沒有 trigger。

又例如：

ERROR→Tp\mathrm{ERROR} \rightarrow T_p

不是合法 judgment transition。

Error 必須先被修復，再重新 evaluate。

十五、Transition Guard

每一轉移可有：

gi(S,E,Γ)=1.g_i(S,E,\Gamma)=1.

例如：

G→TpG\rightarrow T_p

要求：

gclose+=(pt>θp)∧(kt>θk)∧(ct<θc).g_{\mathrm{close+}} = ( p_t>\theta_p ) \land ( k_t>\theta_k ) \land ( c_t<\theta_c ).

十六、Side Effects

判斷狀態轉移本身與外部行動分開。

St→TpS_t\rightarrow T_p

不自動：

Execute⁡(a).\operatorname{Execute}(a).

需要：

DecisionPolicy⁡(Tp,a)=1.\operatorname{DecisionPolicy}(T_p,a)=1.

這避免：

判斷成立 → 系統直接造成不可逆外部效果。

十七、責任 Event

若外部行動被執行：

at,a_t,

新增：

eaction.e_{\mathrm{action}}.

其後結果：

eoutcome.e_{\mathrm{outcome}}.

修復：

erepair.e_{\mathrm{repair}}.

因此 JSM 可以與責任 ledger 連接。

十八、Replay 等價

若：

H\mathcal H

固定，

且 deterministic policy：

Θ\Theta

固定，

則應要求：

Replay⁡(S0,H,Θ)=Sn.\boxed{ \operatorname{Replay} ( S_0,\mathcal H,\Theta ) = S_n. }

若不成立，runtime state cache 不可信。

十九、模型非決定性

若事件中包含 LLM output，

則 replay 不能只重新呼叫模型。

必須保存：

CommittedOutput⁡i.\operatorname{CommittedOutput}_i.

Replay 使用已提交結果。

Re-evaluation 才重新呼叫新模型。

二十、同一事件歷史下的重新判定

可以另外定義：

Rejudge⁡(H,Mnew).\operatorname{Rejudge} ( \mathcal H, M_{new} ).

它產生新 lineage：

Bnew,B^{new},

不是覆蓋舊 lineage。

這使：

Replay≠Re-evaluation.\text{Replay} \neq \text{Re-evaluation}.

二十一、與 Truth Maintenance System 的關係

Doyle 的 TMS 已經強調：

  • beliefs 要保留 reasons；
  • 新發現可以撤回先前 assumption；
  • explanation 可由 dependency structure 建立。

JSM 不宣稱這些是新發現。

JSM 的新增重點在：

Reason Maintenance+Event-Sourced Runtime+Replay+Visual Projection+Responsibility.\boxed{ \text{Reason Maintenance} + \text{Event-Sourced Runtime} + \text{Replay} + \text{Visual Projection} + \text{Responsibility}. }

二十二、核心定理候選

Replay Consistency Proposition

若：

  1. 初始狀態相同；
  2. event log 完全相同；
  3. deterministic reducer version 相同；
  4. committed nondeterministic outputs 相同；

則：

Replay⁡1=Replay⁡2.\operatorname{Replay}_1 = \operatorname{Replay}_2.

這是一個可工程驗證的 proposition。

二十三、最小 reducer

可概念化為：

state = initial_state

for event in ledger:
    validate(event)
    state = reduce(state, event, policy)

return state

這是整個可執行動態判斷的最小 reference semantics。

二十四、結論

本系列至此從哲學語言：

判斷是動態的。

推進到：

判斷可以被實作為可驗證、可重播、可投影的狀態機。\boxed{ \text{判斷可以被實作為可驗證、可重播、可投影的狀態機。} }

下一篇將進一步處理：

證據、真值、支持度、來源與判斷狀態，究竟應該怎麼分層，才不會再次全部壓成一個數字？