Belnap–Dunnの四値論理FOUR（Belnap 1977 / Dunn 1976）の真理順序のmeetは、標準的な埋め込みembedDfumt8 : Belnap4 → Dfumt8を通してD-FUMT₈の8値AND演算（and8）に移る。Lean 4で証明し、`#print axioms`は依存する公理がないこと（`does not depend on any axioms`）を示す。
式
∀ x y : Belnap4, embedDfumt8 (Belnap4.meet x y) = and8 (embedDfumt8 x) (embedDfumt8 y)
LaTeX source
\forall x, y \in \mathrm{Belnap4}.\quad \mathrm{embedDfumt8}(x \sqcap y) \;=\; \mathrm{and8}\bigl(\mathrm{embedDfumt8}(x),\, \mathrm{embedDfumt8}(y)\bigr)記号表
| 記号 | 意味 | 型 |
|---|---|---|
| Belnap4 | Belnap–Dunn四値論理の値型（T / F / B / N） | Type |
| Dfumt8 | D-FUMT₈八値論理の値型（TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF） | Type |
| Belnap4.meet | Belnap–Dunnの真理順序におけるmeet（Belnap 1977 / Dunn 1976） | Belnap4 → Belnap4 → Belnap4 |
| embedDfumt8 | canonical mapping T↦TRUE, F↦FALSE, B↦BOTH, N↦NEITHER | Belnap4 → Dfumt8 |
| and8 | D-FUMT₈の8値AND演算（Rei-AIOS CollatzRei.Dfumt8Category） | Dfumt8 → Dfumt8 → Dfumt8 |
| x, y | Belnap4の任意の値 | Belnap4 |
走る最小例
Lean 4で `embedDfumt8_preserves_meet` を証明し、`#print axioms` でaxiom profileを出力する（= lean-verify.ymlがGitHub Actionsで実行、本項目の検査状態はその出力から生成）。
import CollatzRei.Belnap4Embedding open CollatzRei.Belnap4 #check @embedDfumt8_preserves_meet #print axioms embedDfumt8_preserves_meet
期待される出力：
embedDfumt8_preserves_meet : ∀ (x y : Belnap4), embedDfumt8 (x.meet y) = CollatzRei.Dfumt8Category.and8 (embedDfumt8 x) (embedDfumt8 y) 'CollatzRei.Belnap4.embedDfumt8_preserves_meet' does not depend on any axioms
検査状態
S2形式証明済み (axiom-free)
検査の内訳を見る
| 定理 | CollatzRei.Belnap4.embedDfumt8_preserves_meet |
| Lean file | CollatzRei/Belnap4EmbeddingAxiomCheck.lean |
| 公理 | (公理なし) |
| 生成元 | gha (GHA run 39175017999) |
| 生成時刻 | 2026-10-18T23:15:15.522Z |
| Lean toolchain | leanprover/lean4:v4.27.0 |
関係項目
- rp.belnap4-embed-injective — 両者ともLean 4 CollatzReiプロジェクト内でaxiom profileを検査した、同じ埋め込みembedDfumt8の性質に関する定理（本項目はmeet保存、関連項目は単射性） [related_to]
- rp.belnap4-embed-image — 両者ともLean 4 CollatzReiプロジェクト内でaxiom profileを検査した、同じ埋め込みembedDfumt8の性質に関する定理（本項目はmeet保存、関連項目は像の特定） [related_to]
出典
- A useful four-valued logic — Belnap, N. D. (1977) URL
- Intuitive semantics for first-degree entailments and coupled trees — Dunn, J. M. (1976) URL
- Rei-AIOS Lean 4 CollatzRei/Belnap4Embedding.lean — Fujimoto, N. (2026) AGPL-3.0 + Commercial
書き手と承認
| 下書き | Claude（AnthropicのAI）2026-10-15 |
| 下書き | Claude（AnthropicのAI）2026-10-27 |
| 独立レビュー | Claude（Code サブエージェント・独立レビュー） (2026-10-27) |
| 公開承認 | 藤本 伸樹2026-10-28 |
| ページ生成 | ボット（項目データから自動生成） |
訂正記録 (1件)
C-preserves-meet-corr-001
誤りの種類：出典の不一致
何が誤りだったか：出典「Rei-AIOS Lean 4 CollatzRei/Belnap4Embedding.lean」のauthorが '藤本 伸樹' と記録されていたが、本人（藤本さん）確認済の正統表記は 'Fujimoto, N.'。他6項目（rp.belnap4-embed-image / rp.belnap4-embed-injective / rp.dvir-bound-3-2 / rp.dvir-bound-3-4 / rp.dvir-bound-5-4 / rp.homogeneous-vanishing-fn）で同人のself-referenceは全て 'Fujimoto, N.' で統一されており、本項目のみ日本語表記のoutlierだった。
どう直したか：出典のauthorを 'Fujimoto, N.' に修正。他6項目のauthor表記と一致。
発見: claude-code ｜ 訂正 commit:
d862a6fb0890ab4dc586289814a7198a4f202e49全項目の訂正一覧: /reipedia/corrections/