MWT-02:Global Legality Calculus
跨 Presentation 合法作用、四態判定、約束合成、非交換排程與證書化執行
英文題名: MWT-02: Global Legality Calculus — Cross-Presentation Admissibility, Four-State Judgments, Constraint Composition, Noncommutative Scheduling, and Certified Execution
系列: Mathematical World Theory(MWT)
篇次: 02
文件編號: EML-MWT-02-2026-v0.1
作者: Neo.K
協作: Aletheia / GPT-5.6 Sol
機構: EveMissLab/一言諾科技有限公司
日期: 2026-08-18
版本: v0.1
文件性質: 數學世界論第二篇形式母稿/Global Legality Calculus/AI-native mathematical runtime foundation
前置文件: 《MWT-01:World Primitive 與 Presentation Theory》
狀態: 可使用研究稿;尚非完備決定程序;不宣稱所有合法性問題皆可判定
摘要
MWT-01 建立了 World primitive 與 Presentation Theory,將可操作數學重新定位為帶有 context、observer、identity、history、semantics 與 certificate 的 presentations,並以動態 presentation graph 作為 AI-native 全域數學運行的第一層 substrate。由此立即產生下一個無法迴避的問題:
當多個合法 presentations 被放入同一數學世界後,什麼條件下它們之中的對象、算子、證明、資料與狀態有資格彼此作用?
若只因兩個節點都存在於 registry 就允許交互,MWT 將退化成「萬物可以任意互算」的完全圖;若只允許同一 presentation 內部運算,MWT 又退回傳統局部數學,失去全域跨表示交互的核心目標。
本文提出 Global Legality Calculus(GLC),將「合法」從單一布林標籤提升為一組可版本化、可證書化、可分層、可合成、可衝突且可保留未知的判定結構。對一個候選交互 episode:
其中 是在 native presentation 中定義的作用, 來自不同 presentations , 是必要的跨 presentation bridge, 是形式與運行 context, 是歷史/先後資訊。GLC 不直接問「要不要算」,而先形成 judgment:
其中:
本文強調:這四態首先是 legality evidence states,不是命題真值。為每個判定保留兩個證據方向:
其中 表示是否已形成足夠的允許證書鏈, 表示是否存在有效阻斷證書。由此:
此結構吸收四態/相容矛盾推理的非爆炸精神,但不把 Belnap-Dunn/FDE 直接等同於 MWT 的合法性語義。MWT 的 Conflicted 只表示「允許鏈與阻斷鏈同時存在且皆未被合法消解」,不是宣稱某個數學命題本體上同時真與假。
GLC 將一個 candidate interaction 拆成一族可配置的 hard gates,包括:
- well-formedness;
- presentation/version validity;
- source-domain membership;
- bridge validity;
- type compatibility;
- identity compatibility;
- semantic compatibility;
- context admissibility;
- constraint satisfiability;
- invariant preservation;
- history/order admissibility;
- observer/governance permission;
- resource admissibility;
- certificate availability;
- realizability。
其中 hard constraints 不允許用其他高分補償。本文因此延續 X 約束算子論的核心區分:
甚至再增加:
一個 interaction 可以在形式上合法執行,但其輸出命題仍然可能是假的;合法性只表示「依目前明示規則有資格執行/推導/轉譯」,不等於結果自動具有 World-level 真實性。
本文進一步處理非交換排程。若兩個操作:
則不能把「都合法」簡化成「可任意平行執行」。GLC 將 legality 擴張到 path:
並要求每一步在前一步更新後的 state/context 上重新判定。因此:
不推出:
或:
本文由此建立 strict、exploratory 與 simulation 三種 runtime mode。Strict mode 只有 可 commit; 與 可進 sandbox、研究或人工複核,但不得偽裝成正式合法結果; 預設拒絕,除非經顯式 theory revision 或 exception rule 產生新版本規則。
最後,本文提出 Legality Engine、Gate Registry、Constraint Registry、Certificate Ledger、Conflict Ledger、History Ledger、Execution Queue 與 Commit/Rollback Layer 等最低運行模組,並提供一個可執行 reference evaluator。GLC 的目標不是成為能判定一切數學活動的全知 oracle,而是建立一個可以明確說「不知道」「衝突」「不允許」的全域數學控制平面。正因為它拒絕強迫所有 candidate interaction 得到二值答案,MWT 才能在 AI/AGI 時代安全地進行大規模異質、非交換、跨基礎與跨觀察者計算。
關鍵詞: Mathematical World Theory、Global Legality Calculus、合法作用、四態判定、partial operators、constraint composition、refinement types、effect systems、paraconsistency、noncommutativity、certificate、AI-native mathematics、global scheduler
0. 本文的責任:MWT 不能只會「把東西放進世界」
MWT-01 解決:
的分離。
但如果下一步只做:
然後宣稱:
既然它們都在 World Registry 裡,就讓它們全部互相作用。
那麼 MWT 會立即崩潰。
因為:
- 一個微分算子未必能作用於任意 graph;
- 一個群作用未必對任意 object 有定義;
- 一個 proof term 未必能送入 numerical solver;
- 一個 probability distribution 未必具有另一個 presentation 所要求的 identity semantics;
- 一個 coarse-grained state 未必能恢復被操作需要的 microscopic degree of freedom;
- 一個 bridge 可以存在,但只在真子域上合法;
- 一個 action 今天合法,執行第一步後第二步可能不再合法;
- 一個局部 contradiction 不應授權全世界所有結論。
因此 MWT 必須有第二層:
本文建立的就是這一層。
1. 「合法」不是法律詞,而是 admissibility
本文中的「合法」首先不是:
- 合法律;
- 合倫理;
- 合政策;
- 合社會規範。
它的最低數學意義是:
在一組已明示的 domain、type、identity、semantics、constraint、history、permission 與 certificate 規則下,一個候選構造、作用、合成、翻譯或執行是否具有被接受進下一層運行的資格。
英文核心詞採:
與:
交替使用。
若某個應用真的涉及法律、倫理、權限或治理,這些只是 legality gates 的特定類型,而不是本文全部含義。
2. 從作用對象改成 Interaction Episode
如果只寫:
資訊太少。
因為 MWT 必須知道:
- 來自哪個 presentation;
- 的 native presentation 是什麼;
- 是否需要 bridge;
- bridge 哪一版;
- identity contract 是什麼;
- context 是什麼;
- 之前發生過什麼;
- resource budget 是什麼;
- 哪個 observer / agent 在執行。
因此定義 interaction episode:
其中:
3. Native Presentation 與 Partiality
每個 operator:
至少在某個 presentation:
中具有 native meaning。
寫:
使用 partial arrow 表示:
不必對所有可能輸入有定義。
MWT-02 正式保留:
這也是本文與「既然都在同一世界就都能相互作用」之間最重要的第一道牆。
4. Cross-Presentation Input
若:
已經位於:
可以有:
若:
則需要 bridge:
但 bridge existence 仍然不夠。
還要判定:
以及:
所以:
5. Global Legality Judgment
MWT-02 的基本 judgment:
其中:
- :完整 legality context;
- :candidate interaction;
- :當前 legality ruleset;
- :合法性狀態。
注意:
不等於單一 total function。
它可以包含:
- decidable rules;
- theorem prover;
- type checker;
- constraint solver;
- external evidence verifier;
- bounded search;
- human decision;
- versioned policy。
所以此式是一個 judgment interface,而不是宣稱已擁有 universal decision procedure。
6. 四態合法性狀態
定義:
6.1 Legal
表示:
對當前 run 所要求的全部 hard gates,已形成足夠的正向合法性證書,且目前沒有有效 blocking certificate。
它不是:
6.2 Illegal
表示:
至少存在一個有效 blocking certificate,且尚未同時形成完整正向允許鏈。
6.3 Undetermined
表示:
尚未形成完整正向證書鏈,也沒有足夠 blocking certificate。
可能原因包括 proof 尚未完成、solver timeout、缺資料、bridge 未知、不可判片段、resource budget 不足或 observer 不可辨識。
MWT 明確禁止:
也禁止:
6.4 Conflicted
表示:
已形成完整正向合法性支持鏈,同時存在一個或多個仍有效的阻斷證書。
Conflicted 必須保存,而不是被 majority vote 靜默覆蓋。
7. 四態是合法性證據狀態,不是真值
本文使用雙軸形式:
其中:
表示已存在完整正向 admissibility support;
表示存在有效 rejection / blocking support。
因此:
但:
合法性只處理「有資格執行/推導/翻譯」,不是一般真值。
8. 與 Belnap-Dunn 四值的關係
Belnap 的四值邏輯與 First-Degree Entailment 提供成熟參照:positive information、negative information、both 與 neither。
MWT-02 吸收的主要工程精神是:
但不宣稱:
因為 MWT legality 處理的是可作用性、合成、型別、版本、證書與執行資格,而不是一般命題的 truth semantics。
9. Non-Explosion Principle
如果:
MWT 不允許由此推出:
即:
衝突必須被限制在相關 gate、context、dependency descendants 與顯式允許的 propagation edges。
10. Gate Decomposition
令:
為 的 required hard gates。
v0.1 提供十五類候選 gate:
不是每個 interaction 都需要十五個。
required subset 由 operator、presentation capability 與 execution mode 共同決定。
11. Gate Result
每個 gate:
返回:
並附正向或阻斷證書:
最低 gate record:
其中 是 ruleset/version, 是 validity horizon。
12. Full Positive Certificate
一個 candidate interaction 要形成完整正向合法性證書:
要求所有 required hard gates 都有正向支持:
並組成:
certificate 不必全部同格式,可以是 proof term、type-check result、solver certificate、hash、test evidence、human authorization 或 measurement record。
13. Blocking Certificate
只要存在 required hard gate:
具有有效 blocking support:
則:
並至少保存:
因此 hard failure 可以 early reject,而不需要等所有 gate 都完成。
14. Default Aggregation Rule
strict default:
得到:
特定 domain 可以覆寫 aggregation policy,但必須版本化並產生新的 rule identity。
15. 為什麼不是 Majority Vote?
若十五個 gate 中十四個通過,一個 hard type gate 明確失敗,不能做:
然後宣稱「93.3% 合法」。
如果失敗的是硬條件,作用仍然:
因此:
16. Soft Preferences 不屬於 Legality Core
例如比較快、比較便宜、比較漂亮、比較容易讀或 GPU utilization 較佳,都可進:
或:
層。
但不應把:
靠高 performance 分數補回:
所以:
先合法,再比較優劣。
17. Operator Legality、Applicability、Executability、Realization
一個 operator:
本身在 presentation 中可以:
這不推出:
若:
且:
可稱:
但 applicability 仍不包含 permission、resource、history 與 global invariant。
再進一步,若當前 runtime 資源與執行條件滿足:
如果結果還需要對外部/物理 backend 有效,另問:
因此完整階層:
18. Truth 再額外分離
如果 interaction 是推導命題:
即使:
仍然不直接推出:
最多先得到:
或:
相對指定 foundation/model。
因此:
19. 五種不能混同的合法性
延續 X 約束算子論,至少區分:
這五個層級共同構成 GLC 的基本骨架。
20. Composition Legality
即使:
且:
也不能推出:
因為可能:
或者 改變某個 invariant,使 的 precondition 失效。
21. Constraint Satisfiability
設 hard constraints:
各自都合法。
仍可能:
這表示:
此時應輸出 constraint diagnosis,例如:
而不是說每個 constraint 本身非法。
22. Unsatisfiable 不等於 Illegal Rule
例如:
與:
兩個約束各自完全合法。
共同 system:
在實數域不可滿足。
所以:
23. Bridge Legality
MWT-01 定義:
MWT-02 要求 bridge 至少檢查:
其中:
- :source domain;
- :preserved inquiries;
- :identity contract;
- :declared loss;
- :bridge certificate。
即使 bridge 存在,若:
則本次使用仍不合法。
24. Type Gate 與 Refinement Gate
若:
而 bridge 後輸入:
需要:
或相應 subtype/coercion relation。
若沒有合法 coercion:
普通 type:
也可能不夠。
若 operator 要求:
則:
即使 base type 正確仍不合法。
因此:
25. Effect Gate
某 operation 可能 type-correct,但具有 effect:
若當前 context 禁止 write、network、mutation、nondeterminism 或 external call,則:
或在 effect inference 未完成時為:
effect system 因而可以成為 GLC 後端之一。
26. Semantic Gate
兩個 presentations 的資料型別相同不表示語義相同。
例如:
可以表示 probability、count、boolean encoding、physical unit 或 category label。
因此 bridge 必須確認:
符合 translation contract。
27. Unit / Dimension Gate
在物理或工程 presentation 中:
不能直接與:
進行任意加法。
即使兩者底層都使用:
所以 numeric base type 相同不保證 legal action。
28. Identity Gate
如果 operator 假定 在 path 中保持某種 identity,但 bridge 只保留 coarse equivalence,則不能直接使用。
例如:
不表示:
因此 operator identity requirement 必須被 bridge identity contract 覆蓋。
29. Context Gate
同一作用:
在不同:
可以有不同 legality。
例如不同 assumptions、foundation、time horizon、permission 或 error tolerance。
因此:
若沒有 context index,只是 shorthand。
canonical 形式仍是:
30. Invariant Gate
若:
被標記為 hard invariant,
則 action 需要證明:
若已證明:
則:
若尚未證明保持或破壞:
31. History Gate
如果 operator legality 依賴之前發生的 path:
則:
不能縮成:
例如 token 已被消耗、theorem dependency 已撤回、resource 已被前一步占用、state 曾經通過 irreversible transition,或 previous bridge 已產生 lossy coarse-graining。
32. Noncommutative Legality
若:
則可能:
甚至:
但:
所以非交換不只是結果差異,也可能改變「是否還有資格繼續作用」。
33. Path Legality
對 path:
定義:
並要求:
對所有:
其中:
34. Path Legal 不等於所有節點預先 Legal
第二步 legality 必須在第一步之後重算。
所以不能只在:
檢查:
然後永久授權整條鏈。
需要:
35. Legality Is Stateful
定義:
與:
可以不同,即使 ruleset 版本不變。
因為 state、resource、history、evidence 或 certificate horizon 可以改變。
所以:
36. Validity Horizon
每個 certificate:
可以帶:
或其他有效條件。
過期後不能自動 reuse。
若無法重新驗證:
37. Permission Gate
純數學 theorem proving 通常不需要人類權限。
但 MWT runtime 可能連接 databases、external tools、private sources、robots 或 deployment systems。
因此 action 可以有:
它不是數學真理 gate,而是 execution governance gate。
38. Resource Gate
action 理論上可計算,但在 budget:
下不一定可執行。
令:
為成本估計。
若有硬上界且:
strict runtime 可判:
這個阻斷原因不能被誤讀成 mathematical impossibility。
39. Certificate Gate
有些高風險 interaction 要求 proof-carrying execution。
例如:
若 policy 要求 certificate,但目前只有 heuristic evidence:
而不是 Legal。
40. Evidence Gate 與 Realization Gate
對 empirical action,可能存在:
如果正反 evidence 同時充分,可出現:
這與 formal contradiction 不完全相同。
形式模型也可能:
但其 physical realization:
MWT 禁止把兩層混成一個 verdict。
41. Layered Legality Profile
更完整地:
Global verdict 是相對 execution policy 的投影:
42. Strict Mode
Strict mode:
其餘三態:
都不 commit。
43. Exploratory Mode
Exploratory mode 可以允許:
進 sandbox。
但結果必須帶:
與:
Conflicted 也可進 isolated branch,但不得污染 stable core。
44. Simulation Mode
如果某 action:
但:
可以在 simulation sandbox 執行。
因此:
45. Commit Semantics 與 Transactional Legality
一次正式 interaction 建議分:
令:
為 stable state。
candidate action 先在 staging state:
執行。
只有:
才:
否則 stable state 不被污染,系統進 rollback、failure branch 或 repair queue。
46. Repair Obligation
若:
或:
GLC 可以產生:
作為 repair obligations。
例如:
- find bridge;
- add proof;
- refine type;
- collect data;
- reorder path;
- relax soft constraint;
- choose new presentation;
- request theory revision。
這使 failure 不只是停止訊號,而成為下一步研究資料。
47. Illegal 不能靠重新命名變 Legal
若:
type mismatch,
不能只建立新名稱:
就假裝通過。
任何 repair 必須產生:
因此 MWT 對「語言包裝」與「真正轉換」做明確區分。
48. Exception Rule
某些系統需要 exception。
但 exception 不能是:
管理員說可以,所以原規則不存在。
正確形式是產生新 rule context:
並重新判定:
所以 exception 是規則的一部分,不是規則外的黑洞。
49. Rule Versioning
legality ruleset:
必須固定版本。
同一 action:
可能:
而:
這不是 contradiction,除非版本 index 被刪掉。
50. Run-Level Foundation Freeze
延續 MWT 母稿,對 formal run:
AI 不得因 candidate action 不合法就自動:
並繼續假裝是同一 run。
ruleset revision 必須是:
且留下 migration、invalidation 與 rollback 資訊。
51. Conflict Ledger
所有:
interaction 應進:
至少保存:
interaction_id
positive_certificate_chain
blocking_certificate_chain
contexts
rule_versions
observer_sources
affected_dependencies
resolution_status
52. Conflict Propagation Guard
衝突只能沿:
中的合法 propagation edges 傳播。
不能:
對任意 。
53. Dependency-Scoped Non-Explosion
若:
不依賴:
且沒有 conflict propagation path:
則:
局部衝突不應停掉整個世界。
54. Global Interaction Graph
令 candidate interactions:
形成:
其中 nodes 可以是:
- presentations;
- objects;
- operators;
- gates;
- certificates;
- results。
edges 包含:
- dependency;
- bridge;
- order;
- conflict;
- invariant;
- certificate;
- resource。
55. 四個 Legality 子圖
定義 strict legal interaction set:
只有:
進 commit-capable scheduler。
定義未知集合:
它進 research queue、proof search、bridge discovery、evidence acquisition 或 human review。
定義衝突集合:
它採:
定義非法集合:
它可以保留作 negative knowledge、failed route、regression test 或 future revision target。
56. Scheduler 不是 Topological Sort 就結束
若 dependency graph 是 DAG,topological sort 可以提供合法先後的一部分。
但 MWT 還要處理:
- commutativity;
- shared mutable state;
- bridge loss;
- dynamic legality;
- resource;
- alternative branches。
因此 scheduler 必須是:
57. Commutativity Certificate
如果兩個 actions:
被允許交換,最好有:
證明或驗證:
沒有 certificate 時,不能只因看起來互不相關就永久假設交換。
58. Conditional Commutativity
可能只有在:
上:
所以 certificate 必須帶 domain:
超出 必須重檢。
59. Branch on Order
如果:
與:
都合法且非交換,scheduler 可以產生:
並行探索兩支。
這是 AI-native mathematics 的重要能力:人類可能因分支太多而被迫提前假設某些交換性,AI 則可以在資源允許時保留多條合法歷史。
60. Path Certificate
對完整 path:
建立:
它證明的不是單一 theorem,而是:
這條執行歷史在當前 ruleset 下可合法重放。
61. Replay
若:
仍有效,另一 runtime 應能重建:
若版本或 bridge 改變,replay 必須標記:
而不是靜默使用新環境。
62. Certificate Algebra
證書也需要合成。
如果:
證明 合法,
證明 在 後合法,
則可形成:
但:
一般不是交換操作。
通常:
因為 preconditions 與 postconditions 不同。
63. Certificate Composition 也可能失敗
即使:
各自有效,若:
無法滿足:
則:
未定義。
再次得到:
64. Static Legality 與 Dynamic Legality
某些 gate 可在 execution 前完成:
- syntax;
- type;
- signature;
- bridge version;
- static effect;
- theorem certificate。
形成:
另一些只能 runtime 知道:
- current state;
- resource;
- lock;
- latest data;
- dynamic permission;
- path-dependent invariant。
形成:
global legality 需要兩者。
65. Static Legal 不等於 Runtime Legal
例如程式:
type checks,
但 memory:
不足。
則:
反過來,runtime 暫時有資源也不能改寫 static operator definition。
66. Monotone 與 Non-Monotone Legality
若增加證據:
只可能讓:
朝 definitive verdict 移動,可稱某 gate evidence-monotone。
但很多現實 legality 是 non-monotone。
新增 blocker 後:
規則撤回後:
MWT 不預設全域單調。
67. Revocation
certificate:
可以被撤銷:
所有依賴 的 stable results 必須進:
這是世界長期運行的必要機制。
68. Legality Provenance
每個 verdict:
必須可追溯:
沒有 provenance 的 Legal 不進 stable core。
69. Reason Codes
Illegal、Undetermined 與 Conflicted 都應有 reason set:
例如:
TYPE_MISMATCH
BRIDGE_OUT_OF_DOMAIN
CERTIFICATE_MISSING
INVARIANT_VIOLATION
RESOURCE_LIMIT
RULE_VERSION_CONFLICT
IDENTITY_CONTRACT_MISMATCH
HISTORY_DEPENDENCY_UNRESOLVED
這使 AI 能自動生成 repair plan。
70. Legality Maturity
一個 legality claim 可以分成熟度:
L0 — Claimed
只有自然語言說「可以」。
L1 — Rule-Structured
有明確 gate 與規則。
L2 — Machine-Checked
至少部分 gate 可機器驗證。
L3 — Certificate-Carrying
關鍵 hard gates 有證書。
L4 — Cross-Implementation
至少兩個獨立 verifier 重放。
L5 — Stable Runtime
跨版本或長時間仍保持指定 invariants。
不是所有普通運算都需要 L5,依風險設定。
71. Example A:代數數到浮點 Solver
有:
在 algebraic presentation:
numerical solver native 於:
需要 bridge:
如果 只提供:
而 solver 要求 error:
則:
或:
取決於是否還能 refinement。
不是因為 非法,而是當前 bridge 不足。
72. Example B:Proof Assistant 與 Numerical Evidence
某 theorem:
有大型 numerical evidence。
但 formal proof presentation:
要求完整 proof term。
則:
不等於:
global verdict 可能仍是:
這保留:
73. Example C:P vs NP 多 Presentation
candidate argument 在:
中得到某結論。
要輸送到:
需要 bridge:
若 theorem 只證明 在 restricted circuit family 上 sound,則超出 domain 的 claim:
這可阻止「局部等價被偷換成全域等價」。
74. Example D:非交換 Constraint
兩個 constraints:
各自合法。
但:
先刪除某些 states,使另一條後續路徑不可恢復。
反序:
得到不同 feasible set。
因此:
本身必須進 history。
75. Example E:Observer Translation
observer 與 各自有合法 presentation。
若:
尚未證明保持某 invariant:
則 cross-observer merge:
而不是直接說「只是不同視角,所以等價」。
76. Example F:Conflicted Bridge
bridge:
有:
證明對 identity:
保真。
另一個 audit:
指出對:
失真。
如果 interaction 沒有聲明 identity specification,則:
比強行選一方更正確。
77. Example G:合法計算得到錯誤 Conjecture
AI 可以合法執行:
輸出:
這表示生成 action:
但:
仍然是:
因此:
78. Example H:Global Coupling
三個 presentations:
各自有 interactions:
假設 和 可交換,但 和 不可交換。
scheduler 不能只建立:
的 unordered set。
需要保存 partial order,例如:
以及 與 的有條件 independence。
79. Global Coupling 不是一次矩陣乘法
MWT 的全域交互不能預設:
已涵蓋全部 legality。
runtime 更接近:
80. Candidate Generation 與 Legality 分離
AI 可以非常激進地生成:
這本身不危險。
真正危險的是 candidate 未經 legality 就直接 commit。
所以 MWT 鼓勵:
81. Legality Search 也可以展開
若:
是 Undetermined,AI 可以展開:
- proof search;
- bridge search;
- alternate presentation;
- counterexample search;
- constraint decomposition;
- type refinement;
- observer comparison。
因此 legality calculus 本身也參與:
82. Legality Convergence
多個 verifier:
給:
MWT 不做單純 vote。
先分析:
- same ruleset?
- same context?
- independent implementation?
- same certificate?
- shared bug?
- foundation difference?
最後形成:
其中 是 stable legality support, 是 disagreement, 是 unresolved, 是 certificates。
83. Cross-Implementation Legality
如果兩個獨立 verifier:
都重放:
可以提高 Legality Maturity。
但:
共享 specification bug 仍可能存在。
84. External Theory Interface:Partial Functions
MWT-02 的:
與既有 partial-function / partial-algebra 傳統相容。
MWT 不重新發明 partiality。
MWT 的增量在於:把 partiality 與 presentation bridge、history、observer、certificate、runtime resource 共同納入 global interaction judgment。
85. External Theory Interface:Type Systems
type systems 已成熟處理 term formation、type safety、effect restrictions 與 subtype/refinement constraints。
MWT 不重新發明 type checking。
它把:
視為 legality gate family 的一員。
86. External Theory Interface:Effect Systems
Lucassen 與 Gifford 的 polymorphic effect systems 已展示 effect information 可以用於發現 expression scheduling constraints。
這正好說明:
MWT 將此精神推廣到跨 presentation global scheduler。
87. External Theory Interface:Liquid / Refinement Types
Liquid Types 將 type inference 與 predicate abstraction 結合,用於靜態驗證 safety properties。
MWT 可以把 refinement proof 直接作為:
或:
因此 GLC 是 meta-orchestration,不是另一個 competing refinement type system。
88. External Theory Interface:Paraconsistency
Belnap 的 four-valued logic 以及後續 paraconsistent traditions 顯示:
可以成為嚴格形式系統。
MWT-02 的 Conflict Isolation 接受這個成熟精神,但 legality state 仍不是一般 truth semantics。
89. External Theory Interface:Heterogeneous Reasoning
heterogeneous dynamic logic 與 logic-pluralistic formalised reasoning 已研究:
- 多 object logics;
- 不同 program logics;
- common meta-framework;
- modular combination;
- sound cross-language reasoning。
MWT 與此高度鄰接。
MWT 的進一步目標是:
這是研究方向,不是已證明的 universal reduction。
90. Global Legality 不是 Universal Decision Procedure
MWT-02 不主張存在:
可以對所有未來 mathematics 的所有 在有限時間給出:
或:
正因如此:
是永久第一級狀態,不是暫時 UI placeholder。
91. Bounded Runtime Semantics
實際 AI system 可以設定:
若 budget 到期且無 definitive result:
不准偽造 verdict。
92. Legality Engine
MWT-02 第一核心 runtime 模組:
輸入:
輸出:
93. Gate Registry
第二個模組:
記錄:
gate_id
gate_type
version
required_capabilities
input_contract
positive_certificate_type
blocking_certificate_type
validity_horizon
dependencies
94. Constraint Registry
第三個模組:
保存 hard constraints、soft preferences、scope、exception rules 與 version。
硬/軟必須分開。
95. Certificate、Conflict、History、Execution 與 Commit 模組
第四個模組:
保存 positive certificates、blockers、provenance、hash、verifier、expiry、revocation 與 dependency graph。
第五個模組:
確保:
不被自動 collapse。
第六個模組:
保存每條 history:
以及每一步 state hash、context、legality verdict、certificate、branch 與 rollback。
第七個模組:
至少分:
STRICT_COMMIT
SANDBOX
RESEARCH
CONFLICT_REVIEW
REJECTED
REVALIDATION
第八個模組:
負責 Commit / Rollback。
只有 strict legal 且 postcheck 通過的 action 才修改 canonical stable state。
96. First Reference Algorithm
概念 pseudocode:
function judge(interaction alpha, context Gamma, rules Lambda):
gates = required_gates(alpha, Gamma, Lambda)
positive_chain = []
blockers = []
unresolved = []
for gate in gates:
result = evaluate(gate, alpha, Gamma)
if result.support:
positive_chain.append(result.positive_certificate)
if result.block:
blockers.append(result.blocking_certificate)
if not result.support and not result.block:
unresolved.append(result.reason)
full_support = every required gate has support
any_block = blockers is not empty
if full_support and not any_block:
status = LEGAL
elif not full_support and any_block:
status = ILLEGAL
elif full_support and any_block:
status = CONFLICTED
else:
status = UNDETERMINED
return status, positive_chain, blockers, unresolved
這一 reference policy 有意維持簡單。
它固定的是 v0.1 的最低語義,不宣稱所有 domain 都必須永遠使用同一 aggregation。
97. Scheduler Algorithm
1. collect strict-legal actions
2. build dependency edges
3. attach noncommutativity relations
4. attach commutativity certificates
5. compute currently enabled frontier
6. execute commuting independent actions in parallel
7. branch when multiple noncommuting legal orders are intentionally explored
8. after every committed step, update state/context
9. re-run affected legality gates
10. invalidate stale certificates
11. postcheck invariants
12. commit or rollback
這個 algorithm 在 MWT-02 只固定接口。
真正的 scheduler theory 留給 MWT-03。
98. Why AI-Native?
人類可以理解:
gate、certificate、path 與 commit。
但大規模 runtime 可能需要同時維護:
- 幾十萬 gate results;
- 多個 foundations;
- 多個 observers;
- 大量 cross-presentation bridges;
- 非交換 path branches;
- certificate validity graph;
- resource / dependency frontier。
這正是 AI/AGI 比較適合承載的部分。
因此本文所稱 AI-native 不是:
而是:
99. Human Governance
Human interface 不需要顯示每個 gate 的所有微觀細節。
至少應顯示:
- why legal;
- why blocked;
- what is unknown;
- what conflicts;
- what will change if committed;
- what certificate supports it;
- rollback availability;
- 哪個 ruleset / version 正在生效。
這使 governance 建立在可追溯結構上,而不是只看 AI 的一句結論。
100. MWT-02 Minimal Constitution
v0.1 固定十六條:
L1 — Legality Before Interaction
任何 cross-presentation interaction 在 commit 前必須經 legality judgment。
L2 — Partiality
operator existence 不代表 universal applicability。
L3 — Four-State Output
系統必須能表達 Legal、Illegal、Undetermined、Conflicted。
L4 — Legality Is Not Truth
Legal 不等於 World-level true。
L5 — Non-Explosion
Conflicted 不得無條件污染無關 interaction。
L6 — Hard Constraints Are Non-Compensatory
硬約束失敗不能靠其他偏好分數抵銷。
L7 — Operator Legality Is Not Composition Legality
合法元件不保證合法合成。
L8 — Composition Legality Is Not Satisfiability
合法合成語法不保證共同解存在。
L9 — Bridge Contract
跨 presentation 作用必須使用有 domain 與 preservation contract 的 bridge。
L10 — Identity Must Be Declared
需要保存的 identity 不得靠名稱默認。
L11 — History Is First-Class When Order Matters
非交換問題必須保存 path。
L12 — Dynamic Recheck
state/context 更新後,受影響 legality 必須重判。
L13 — Certificates Are Versioned
certificate 必須攜帶來源、版本與 validity horizon。
L14 — Unknown Is Stable
系統允許永久保留 Undetermined。
L15 — Conflict Is Preserved
Conflicted 必須被隔離、診斷與追蹤,而不是靜默覆蓋。
L16 — Foundation Revision Is Explicit
AI 不得在同一 formal run 中偷偷改 legality foundation。
101. 命題:Hard Block Dominance
若:
且:
則 default aggregation:
因此:
此命題直接來自四態 aggregation 定義。
102. 命題:Unknown Does Not Authorize Commit
Strict mode 定義:
若且唯若:
因此:
這是 MWT runtime 最重要的安全邊界之一。
103. 命題:Conflict Does Not Explode
由 L5,若:
且:
不在其 dependency / propagation closure,
則不能單由 推出:
這保證局部 conflict 能夠與世界其餘穩定區域共存。
104. 命題:Node Legality Does Not Imply Path Legality
存在:
各自 Legal,
但:
因此:
未定義。
所以:
105. 命題:Order Can Change Legality
若:
改寫一個 gate precondition,使:
失效,而 不破壞 的 precondition,則可能:
但:
故 path order 是 legality datum。
106. 命題:Legal Execution Does Not Imply True Output
若 action:
合法,但輸出 conjecture:
未經 proof,則 legality 定義本身不能推出:
這將 AI 的「合法生成」與「數學證明」永久分離。
107. 條件定理:Sequential Legality Closure
設 path:
並假設:
- 初始 合法;
- 每一步:
- 每一步 postcheck 成功;
- context update 正確;
- 所有 certificate 在執行時有效。
則依定義構造:
為一條可 commit 的 sequentially legal path。
這不是聲稱 path 結果為 World-level true。
它只證明執行歷史符合當前 legality calculus。
108. 條件定理:Certified Bridge Composition
若:
各自具有相對 inquiry family:
的 preservation certificates,且:
並且 identity contracts compatible,則:
可形成對 的候選 composite bridge certificate。
若任一條件失敗,不能由兩個局部 bridge 的存在推出 composite bridge 合法。
109. 研究猜想:Legality-Guided Globalization
對一部分目前必須手工切成多個局部 solver 的問題,若 presentation registry 與 legality engine 足夠成熟,可以先生成較大的 global interaction graph,再由 legality 與 resource gates 動態誘導有效 locality。
這個猜想若成立,代表數學工作流可以從:
逐步轉成:
110. 研究猜想:Conflict-Tolerant Research Acceleration
保存:
與:
而非強迫二值化,可能使多 AI 研究在大量局部 disagreement 存在時仍維持整體推進,降低 premature collapse。
這需要未來以實際 multi-agent research benchmark 驗證。
111. 研究猜想:Certificate-Guided AI Mathematics
當大部分高風險 interactions 都能攜帶 composable certificates 時,AI 可以將更多計算、翻譯與形式化工作從 human micromanagement 轉為 machine-maintained global runtime。
人類的角色因此可以逐步轉向:
- foundation governance;
- value / goal specification;
- high-level inquiry;
- exception approval;
- audit;
- theory revision。
112. 開放問題
O1 — Universal Gate Vocabulary
是否存在足夠小但具有高覆蓋力的 legality gate vocabulary?
O2 — Gate Independence
哪些 gates 可被證明彼此獨立?
O3 — Minimal Certificate
一個跨 presentation action 的最小充分證書是什麼?
O4 — Conflict Algebra
Conflicted gate 的 composition 是否存在有用的通用代數?
O5 — Noncommutative Scheduling Complexity
大量 path-sensitive legality 如何避免 combinatorial explosion?
O6 — Bridge Discovery
AI 如何自動提出並證明新 bridge?
O7 — Legality under Theory Revision
foundation version 改變後,如何最小化 revalidation?
O8 — Observer Disagreement
何時 observer conflict 可以由 covariance / translation 吸收?
O9 — Empirical Legality
模型的 domain-of-validity 如何機器化?
O10 — Physical Realization
形式合法與物理可實現之間如何建立一般接口?
113. Runtime 資料結構
建議最低 interaction record:
Interaction:
interaction_id
operator_id
operator_presentation
inputs[]
bridges[]
context_id
history_ref
rule_version
required_gates[]
execution_mode
每個 input:
InputRef:
presentation_id
object_id
object_version
bridge_id
identity_spec
114. Gate Result Schema
GateResult:
gate_id
required
support
block
positive_certificate
blocking_certificate
reason_codes
rule_version
valid_from
valid_until
115. Judgment Record
LegalityJudgment:
interaction_id
status
full_positive_chain
blockers
unresolved
provenance
repair_obligations
evaluated_at
116. Execution Record
ExecutionRecord:
interaction_id
pre_state
legality_judgment
staging_state
postcheck
commit_status
rollback_ref
resulting_state
history_hash
117. Reference Evaluator 的定位
本 Source Pack 附帶:
mwt02_legality_reference.py
它只實作:
- four-state gate aggregation;
- hard / soft gate separation;
- strict commit rule;
- basic reason tracking。
它不是 MWT-02 完整 theorem prover,更不是 universal legality oracle。
其用途是固定 v0.1 最低 operational semantics,避免未來不同 AI 對四態 aggregation 產生互不相容的隱性解讀。
118. 與內部既有理論的分工
分域算子本體論
提供:
MWT-02 將其提升成跨 presentation gate。
X 約束算子論
提供:
以及:
MWT-02 將其從應用約束中介表示擴張為數學世界控制層。
四態與非爆炸推理
提供:
且:
MWT-02 將此精神轉為 legality conflict isolation。
Series B
提供 relation order、path difference、observer transport、holonomy、covariance 與 local-global obstruction。
MWT-02 將其接到 scheduler 與 history gate。
119. MWT-02 與 MWT-01 的組合
MWT-01 問:
MWT-02 問:
因此:
這是 MWT 第一次從 world representation 進入 world operation。
120. 仍然沒有完成的部分
MWT-02 尚未完整建立:
- optimal global scheduler;
- global convergence protocol;
- branch compression;
- distributed multi-agent transaction;
- world-state canonical runtime;
- proof-carrying bridge synthesis。
這些應由後續文章處理。
121. 下一篇接口
下一篇建議:
MWT-03:Global Interaction Graph and Noncommutative Scheduler
正式處理:
核心將包含:
- dependency graph;
- partial order;
- commutativity certificates;
- dynamic frontier;
- branch explosion control;
- path equivalence;
- transaction;
- multi-AI execution;
- stable-state commit。
MWT-02 管:
MWT-03 管:
122. 一句話版
MWT-02 將「合法性」建立為數學世界的第一級控制結構:任何跨 presentation 作用都必須帶著明示的 domain、type、identity、semantics、constraint、invariant、history、resource 與 certificate 條件接受判定;判定允許 Legal、Illegal、Undetermined 與 Conflicted 四態,並以非爆炸、硬約束不可補償、動態重判、非交換 path 保存與 transactional commit 保證全域計算不退化成任意互算。它不承諾判定一切,而承諾在不知道時說不知道,在衝突時保存衝突,在不合法時拒絕 commit,只有已形成完整正向證書且無有效 blocker 的 interaction 才能進入穩定世界狀態。
附錄 A:核心符號表
| 符號 | 意義 |
|---|---|
| candidate interaction episode | |
| native operator | |
| operator native presentation | |
| cross-presentation bridge | |
| legality context | |
| versioned legality ruleset | |
| legality status | |
| four legality states | |
| legality evidence pair | |
| full positive admissibility support | |
| blocking support | |
| legality gate | |
| positive gate certificate | |
| blocking gate certificate | |
| ordered interaction path | |
| path legality certificate | |
| strict legal interaction set | |
| undetermined interaction set | |
| conflicted interaction set | |
| illegal interaction set | |
| Legality Engine | |
| Gate Registry | |
| Certificate Ledger | |
| Conflict Ledger | |
| History Ledger | |
| Execution Queue | |
| Commit / Rollback Layer |
附錄 B:v0.1 非主張清單
MWT-02 不主張:
- 所有合法性問題可決定;
- 四態 legality 就是 Belnap-Dunn truth semantics;
- Conflicted 表示某命題本體上真且假;
- Legal action 的輸出必然是真的;
- type checking 足以完成所有 legality;
- constraint satisfiability 等於 operator legality;
- 所有合法 actions 可以任意平行;
- 所有非交換 path 都必須全部實際執行;
- 所有 bridges 都能自動發現;
- 所有 certificates 都能形式證明;
- resource block 表示 mathematical impossibility;
- physical unrealizability 表示 formal illegality;
- observer disagreement 必然可消解;
- global legality 需要一個唯一邏輯 foundation;
- MWT-02 取代 refinement types、effect systems、partial algebras、constraint solvers 或 paraconsistent logic;
- AI 有權在同一 run 中自動修改 foundation;
- 多數 verifier 同意就等於 World truth;
- Global Legality Calculus 已經是完整 AGI mathematics runtime。
附錄 C:外部研究接口與參考文獻
- Nuel D. Belnap Jr., A Useful Four-Valued Logic, in J. Michael Dunn and George Epstein (eds.), Modern Uses of Multiple-Valued Logic, 1977, pp. 5–37. DOI: 10.1007/978-94-010-1161-7_2.
- John M. Lucassen and David K. Gifford, Polymorphic Effect Systems, POPL 1988, pp. 47–57. DOI: 10.1145/73560.73564.
- Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala, Liquid Types, PLDI 2008, pp. 159–169.
- J. V. Tucker and J. I. Zucker, Abstract Computability, Algebraic Specification and Initiality, 2001, arXiv:cs/0109001.
- Liyi Li and Elsa Gunter, A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras, 2018, arXiv:1802.06493.
- Célia Borlido and Brett McLean, Difference-Restriction Algebras of Partial Functions with Operators: Discrete Duality and Completion, 2020, arXiv:2012.00224.
- Samuel Teuber, Mattias Ulbrich, André Platzer, and Bernhard Beckert, Heterogeneous Dynamic Logic: Provability Modulo Program Theories, 2025, arXiv:2507.08581.
- Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto, Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning, 2026, arXiv:2605.27246.
附錄 D:內部依賴
MWT-02 主要直接吸收:
- 《MWT-01:World Primitive 與 Presentation Theory》
- 《分域算子本體論:從萬物皆算子到合法作用》
- 《X 約束算子論:局部有限、全局無界的非數值應用約束演算》
- 《四態與非爆炸推理》
- 《多維空間狀態類型論:開放維度、依賴類型與合法態射》
- 《分域憲章:結構域、概念身份與角色型別系統》
- Series B《觀察者、局部關係、非交換與全域守恆》
這些理論不被 MWT-02 廢除。
MWT-02 的責任是把它們已有的 legality、constraint、type、conflict 與 order 思想提升成 World-level cross-presentation control plane。