Belnap–Dunnの四値論理FOUR（1977）の4値T/F/B/Nは、D-FUMT₈の8値のうちTRUE/FALSE/BOTH/NEITHERに単射で埋め込める（Lean 4で形式化。依存する公理はpropextのみ）。
式
∀ x y : Belnap4, embedDfumt8 x = embedDfumt8 y → x = y
LaTeX source
\forall x\, y \in \mathrm{Belnap4}.\quad \mathrm{embedDfumt8}(x) = \mathrm{embedDfumt8}(y) \;\Longrightarrow\; x = y記号表
| 記号 | 意味 | 型 |
|---|---|---|
| Belnap4 | Belnap-Dunn四値論理の値型（constructors: T / F / B / N） | Type |
| Dfumt8 | D-FUMT₈八値論理の値型（TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF） | Type |
| embedDfumt8 | canonical mapping: T↦TRUE, F↦FALSE, B↦BOTH, N↦NEITHER | Belnap4 → Dfumt8 |
| x, y | Belnap4の任意の値 | Belnap4 |
走る最小例
Lean 4で `embedDfumt8_injective` を証明し、`#print axioms` でaxiom profileを出力する（= lean-verify.ymlが実行、本項目の検査状態はその出力から生成）。
import CollatzRei.Belnap4Embedding open CollatzRei.Belnap4 #check @embedDfumt8_injective #print axioms embedDfumt8_injective
期待される出力：
embedDfumt8_injective : ∀ (x y : Belnap4), embedDfumt8 x = embedDfumt8 y → x = y 'CollatzRei.Belnap4.embedDfumt8_injective' depends on axioms: [propext]
検査状態
S2形式証明済み (mathlib base)
検査の内訳を見る
| 定理 | CollatzRei.Belnap4.embedDfumt8_injective |
| Lean file | CollatzRei/Belnap4EmbeddingAxiomCheck.lean |
| 公理 | [propext] |
| 生成元 | gha (GHA run 39175017999) |
| 生成時刻 | 2026-10-18T23:15:15.522Z |
| Lean toolchain | leanprover/lean4:v4.27.0 |
関係項目
- rp.belnap4-embed-image — 単射性（本項目）と像の特定（関連項目）を合わせると、embedDfumt8はBelnap4とD-FUMT₈の4値｛TRUE, FALSE, BOTH, NEITHER｝の間の全単射になる [related_to]
- rp.belnap4-embed-preserves-meet — 両者ともLean 4 CollatzReiプロジェクト内でaxiom profileを検査した、同じ埋め込みembedDfumt8の性質に関する定理（本項目は単射性、関連項目はmeet保存） [related_to]
出典
- A useful four-valued logic — Belnap, N. D. (1977) URLSpringer (chapter in Modern Uses of Multiple-Valued Logic)
- Intuitive semantics for first-degree entailments and coupled trees — Dunn, J. M. (1976) URLSpringer (Philosophical Studies)
- Rei-AIOS Paper 137 — D-FUMT₈ foundational mapping — Fujimoto, N. (2026) AGPL-3.0 + Commercial
書き手と承認
| 下書き | Claude（AnthropicのAI）2026-10-13 |
| 独立レビュー | Claude（独立レビュー） (2026-10-13) / Claude（独立レビュー） (2026-10-14) |
| 公開承認 | 藤本 伸樹2026-10-14 |
| ページ生成 | ボット（項目データから自動生成） |
訂正記録 (2件)
C1-corr-001
誤りの種類：前提の書き落とし2026-10-19 改訂
初版での分類：主張の範囲の言い過ぎ (scope-overclaim)
何が誤りだったか：summary.ja で 「axiom-free 相当」 と 書き、 relations[0] は kind: generalizes + 「axiom profile 対象 定理」 note、 wikidata_q に Q816111 を 設定 — 本件 の 定理 `embedDfumt8_injective` が 実際 に 依存 する 公理 は `propext` の みで、 「axiom-free」 の 曖昧 表記 と 「別分野 の 定理 を generalizes」 の 誤 kind、 独立 verify して いない Wikidata ID を 載せた 書き方
どう直したか：summary.ja の 「axiom-free 相当」 を 「依存する公理は propext のみ」 に 置換 (= 実測 axiom profile = [propext] に 揃え)、 relations[0] の kind を generalizes → related_to、 note を 「両者 と も Lean 4 CollatzRei project 内 で axiom profile を 検査 した 定理 (別分野)」 に 変更、 wikidata_q を Q816111 → null (= 独立 verify 未実施、 加えて `rp.belnap4-embed-injective` は 定理 に 対応 する 概念 で、 Belnap4 一般 の Wikidata ID と は 粒度 が 異なる)
発見: Claude（独立レビュー） ｜ 訂正 commit:
ef4a0970f改訂の根拠（1 件、承認順）
- 改訂 1（判断日 2026-10-19）： scope-overclaim → assumption-dropped by 藤本 伸樹理由：addendum-3 §1.4.1 「原因 を 選ぶ」 原則 で、 原因 = 依存 公理 (propext) の 書き落とし (= assumption-dropped)、 範囲 の 広書き (= scope-overclaim) は その 結果根拠：addendum-4-v1.0 §1.5 ｜ 承認記録： ebf01154b0a3cd709dad43efa160d357df0854eb
C1-corr-002
誤りの種類：出典の不一致
何が誤りだったか：走る最小例の期待出力を、Leanを実際に走らせずに書いていた。実際に走る最小例をLeanで実行すると、`open CollatzRei.Belnap4` の影響で短い名前（embedDfumt8_injective）で表示されるが、以前の期待出力では完全な名前（@CollatzRei.Belnap4.embedDfumt8_injective）で書いていた。定理の内容、必要な公理、検査状態の表示は実機の出力と一致している（表示の仕方だけが違っていた）。
どう直したか：走る最小例の期待出力を、実際にLeanで実行した結果に合わせて直しました。以前の期待出力は実行せずに書いたもので、定理名の表示の仕方（完全な名前か短い名前か）が実際の出力と違っていました。定理の内容、必要な公理、検査状態の表示は変わっていません。
発見: 藤本 伸樹 ｜ 訂正 commit:
2dfb14ea15c1bab822e4cee7badb2bac00925564全項目の訂正一覧: /reipedia/corrections/