Metamath束

🔼用語集
⬅️
➡️構造的積極的分離理論
🔗DwG-1-対話篇：相対的ニヒリズムの深化と普及
🔗DwG-3-対話篇：構造的積極的分離理論の説明と普及
🔗DwG-3-4：Metamath束による積極的分離理論の分析
🔗DwG-1-22：Metamath束

概要

「二分木のみで表現されたMetamath」をベースとした束構造のことです。構造的積極的分離理論はMetamath束に立脚します。

定義

カリー化を駆使して、Metamathの仕組みをアトムを葉に持つ二分木のみを用いて表現した形式系を仮に”Binary Tree Metamath”と呼びます。

Binary Tree Metamathにおいて、全ての束縛変数からなる可算集合(≒全命題集合にわたって付与されるde Bruijn Level)をBVarとし、全ての自由変数からなる可算集合をFVarとします。さらに、全ての「自由変数に割り当て可能な値」からなる集合をValue := Tree BVarとし、自由変数への値の割り当てをv : FVar → Valueとします。

$A$を「束縛変数だけからなる型環境${\Gamma }_A$と、自由変数を含む対象論理式$P_A$の組」とし、$A$が持つ型をPreSystemと表現することにします。$P_A(v)$を$A$の対象論理式$P_A$内の自由変数$i$を$v(i)$で置換したものとし、形式的モデル集合$M(A)$を$v\in M(A)⟺{\Gamma }_A⊢P_A(v)$が成立するように定めます。

以下、各$A,B$に対して、$A$と$B$に登場する束縛変数をうまく合わせる(単一化する)ことが可能だとします。

PreSystem上の同値関係 $\equiv$ を$M(A)=M(B)⟺A\equiv B$が成立するように定めます。$\equiv$ を用いてPreSystemを割ってできた商集合をSystemと表現します。さらに、半順序関係 $\le$ を$\forall A^{\prime }:System,\forall B^{\prime }:System,(M(A^{\prime })\subseteq M(B^{\prime })\iff A^{\prime }\le B^{\prime })$が成立するように定めます。

Systemに半順序関係 $\le$ を導入することで、Metamath束$L(Metamath)$を構築します。

注意

• DwG-3-対話篇：構造的積極的分離理論の説明と普及では「Metamath束」を「単一化束」と呼んでいることがあります。「単一化束」に近い既存の概念として”Subsumption Lattice”が挙げられます。「Metamath束」と”Subsumption Lattice”が同等の概念であるかどうかは、現時点で不明です。 2026-04-02 00:28:46 +0900

定義者

• aconite(『束跡』管理者)