内包・外部検査・trustの健全性
admin
1 このBookの目的と到達点
MatheliaがThmを認めたとき、どの宣言と証拠に基づく判断なのかを、外部の人が追って検査できるようにします。このBookは、2026-09-08の調査と独立検査の結果、今後の接続仕様をまとめたものです。
実測済み：内包・外延性・束縛変数の名前替えについて、手作業で対応を指定した5件の証明と、その依存証明272件を、独立に開発された二つのMetamath検査器で検査しました。正常版は両方が受理し、結論または変数条件を壊した3種類は両方が拒否しました。
未達成：任意のMathelソースからの自動翻訳、Mathelia本番の外部検査接続、cvt+とcls-elimの一般的な受理条件の一致、hyperionを含む全体の健全性の証明です。Mizarとの接続は文献調査までで、今回は実行していません。
本文は調査と仕様の説明です。このBook自体の表示成功や査読ボタンが、ここに書いたメタ定理の証明を意味するものではありません。
実験資料をダウンロードできます。証明ファイル、失敗例、実測ログ、再実行スクリプト、版とSHA-256、対応表を含みます。
2 Thm・trust・検査器を区別する
P ◀ Γ はgoalとsosを持つ形式的なThmです。◀自体に特定の論理での「推論できる」という意味を固定しません。Thmの変換と対象論理を指定し、その対象論理で成立することをtrustの受理条件にします。
したがって、健全性について説明するときは、まず「何を条件に認めると宣言したか」を示します。そのうえで、実際に出したOKがその条件を満たす証拠を持つかを確認します。未宣言の「翻訳前のThmの真偽」を持ち込む必要はありません。
対象論理と証明器は別です。同じ対象論理を扱う複数の証明器・検査器を使えます。新しい検査器が増えただけなら、必ずしも新しいtrustは必要ありません。新しい公理体系や受理条件を採用する場合は、その違いを宣言します。
外部検査器の受理は「指定された公理・仮定から、この対象言語の主張が導ける」という証拠になります。その公理体系の無矛盾性や、Matheliaの別のtrustとの一致まで自動的に保証するものではありません。
3 健全性の説明を四つに分ける
① 宣言：入力したThm、適用する翻訳、その対象言語・論理、使用する定義・背景公理を明示します。版によって条件が変わるときは、別の検査条件として区別します。
② 対応：Mathel原文からMCL、MCLから対象言語へ、goal・sos・変数の範囲がどう写ったかを記録します。新しく追加したsosは元からの仮定と区別し、その生成規則も示します。外部検査器は、入力の取り違えまでは発見できません。
③ 証明：対象言語の主張に対する証明を保存し、独立した検査器に渡します。最終結論だけでなく、仮定と変数条件が、翻訳した問題に一致することも照合します。
④ 合成：複数のtrustで認めた結果をhyperionで使う各規則について、どの受理条件からどの受理条件へ進めるかを確認します。対象論理ごとの検査が正しくても、接続規則が違えば全体の根拠にはなりません。
この四つのうち、今回実際に行ったのは、範囲を限定した手作業の対応付けと、③の独立検査の実験です。①②④の全体を完成させたとはしません。
4 参考体系①：Metamathの仮想クラス
Metamathは形式体系を記述して証明を検査する枠組みです。ここで参考にする集合論のライブラリは、その一つであるset.mmです。Metamathという検査器とset.mmという公理・定義・定理の集まりを区別します。
set.mmの df-clab は、x ∈ {y | φ} ⇔ [x/y]φ によって内包への所属を扱います。クラス等号は df-cleq で別に扱います。所属を代入へ展開する点は、Matheliaのcvtを検討する直接の参考です。
重要な区別：set.mmのclass変数はクラス式を代入するメタ変数です。Matheliaのcソートを走る対象言語の変数と、そのまま同一視しません。今回の実験はクラス量化 ∀_, ∃_ の翻訳を含みません。
公式説明は、クラスの導入について消去可能性・保守性のメタ数学的な根拠も区別しています。検査器にとってはdf-clabやdf-cleqも公理的な宣言です。「定義と呼んだから無条件に安全」「Metamathが全体の保守性まで検査した」とは言えません。詳しくは Theory of Classes を参照してください。
以前の調査の「外延性は独立の前提なしに自動的に従う」という要約は不正確でした。今回の実測では、内包の基本式abidの依存先にはax-extがありませんが、クラス等号の特徴付けdfcleqの依存先にはax-extとdf-cleqがあります。何が必要かは、定理ごとに追います。
5 参考体系②：IsabelleとMizar
Isabelle/HOLのSet理論 は、内包を Collect (λx. P) と表し、a ∈ Collect(P) ⇔ P(a) と Collect(λx. x ∈ A) = A を備えます。所属の展開と集合へ戻す性質をそろえ、型と束縛を明示する構成が参考になります。ただし型付き高階論理上の集合であり、その結果をそのままcソートの仕様とはしません。
Mizarの FRAENKEL には、集合Aの要素を動かす {F(x) where x is Element of A : P[x]} と、そのような項を扱うschemeがあります。集合を構成する記法と、構成した項の性質を利用する規則の整理が参考になります。
Mizar Mathematical Library はTarski–Grothendieck集合論を基礎とします。利用したMMLの定理について、その公理依存をMathelia側でも明示する必要があります。MizarとMatheliaのクラスが同じだとも、両体系が一切接続できないとも、名前だけから判断しません。
この比較から取り入れる方針は、内包の構文・所属の展開・等号・変数条件・存在を支える仮定を分けて記述し、翻訳と証明の各段階でそれらを追跡できるようにすることです。
6 今回の対応表
内包の基本式：Matheliaで検討する「xが{x | P}に属する ⇔ P」に、set.mmのabidを対応させました。Metamathのφは任意のwffを代入できるメタ変数です。MatheliaのP^のpropごとの定数化とは、同じ機構だと仮定しません。
否定・連言：abidにそれぞれ ¬φ と φ∧ψ を代入した証明を作りました。内包の本体の構造を変えても同じ定理を利用できます。
クラス外延性：dfcleqを利用しました。量化する変数xがクラス式A,Bに現れないことに対応する、Metamathの $d x A, $d x B という条件を保持します。これは現在の記号の綴りが違うというだけでなく、後の代入も制限する条件です。
束縛変数の名前替え：cbvabvを利用しました。x=y ⇒ (φ⇔ψ) という仮定と、$d φ y, $d ψ x, $d x y を必要とする条件付きの規則です。無条件に変数名を替えてよいという主張ではありません。
未対応：任意のMCL、自由クラス変数の一般的な扱い、クラス量化、生成したsosと命題変数の範囲、任意のThm・Γの外部形式への変換です。対応表の詳細は実験資料のcorrespondence.mdにあります。
7 実験：正常版と意図的に壊した版
公式set.mmから、abid・dfcleq・abbi・cbvabvに必要な宣言と依存証明を、公式検査器の WRITE SOURCE /EXTRACT で抽出しました。抽出部分には272件の証明と29件の$a宣言があり、そこに5件の$p証明を追加しました。今回新たな$a宣言は追加していません。29件には論理公理だけでなく構文や定義の宣言も含みます。
正常版の5件は、内包の基本式・否定の本体・連言の本体・クラス等号・条件付きの名前替えです。依存証明を省略せず、計277件すべてを検査しました。
検査器は metamath-exe（C実装）と mmverify.py（Python実装）です。両方が正常版を受理しました。
不正版①では、否定の内包の右辺から否定だけを消しました。両検査器とも、証明の結論が主張と一致しないことを理由に拒否しました。
不正版②では、外延性の証明から $d x A を消しました。両検査器とも、必要な変数条件が欠けていることを理由に拒否しました。
不正版③では、名前替えの証明から $d φ y を消しました。これも両検査器が必要な変数条件の欠落として拒否しました。
観測結果は正常1種類×2検査器の受理、不正3種類×2検査器の拒否です。有限個の例の検査なので、検査器にあらゆる誤りが無いことや、Mathelia全体の正しさの証明にはなりません。
8 実測で見つかった結果受取の注意点
今回使用したmetamath-exeでは、不正版に対して明確な ?Error を出した後でも、終了コードは0で、最後には All proofs in the database were verified という文が出ました。終了コード0や最後の成功風の文だけでOKとしてはいけません。
実験用スクリプトは、エラー診断、検査完了、未完成証明の印を確認し、二つの検査器の結果を記録します。mmverify.pyも三つの不正版を非0の終了コードで拒否しました。生のログを実験資料に含めています。
これは使用した版での観測です。将来の本番接続には、版を固定した出力契約、入力と結果の対応照合、エラーや未完成証明を受理しない検査が必要です。今回の実験用スクリプトを、そのまま認証済みの汎用adapterとはしません。
9 第3のtrustか、既存trustの別検査か
利用方法は三つあります。第一に、既存の対象論理の証明を別形式へ移し、独立検査器で再検査する方法です。対象論理と仮定が同じであることを確認できれば、既存のtrustを別の検査器で確認する構成にできます。
第二に、set.mmやMMLの特定の公理・定義・定理を利用する翻訳を宣言し、その成立を第3のtrust条件にする方法です。この場合、体系名だけでなく、実際に使用できる公理・定義と翻訳の適用範囲を指定します。
第三に、Matheliaの翻訳やhyperionの規則を外部体系で形式化し、そのメタ定理を検査する方法です。自作の規則をそのまま外部体系の公理として登録するだけでは、その規則の健全性を証明したことにはなりません。
各結果には、どの形式的Thmに対応するか、対象の主張と仮定、公理依存、自由変数・代入条件、証明、検査器とライブラリの版を結び付けます。生のOKだけを返す接続にはしません。
10 Mizarを利用する具体的な道
Jesse Alamaの Escape to Mizar for ATPs（2012）は、Eの導出をMizarの証明へ写すツールを報告しています。外部ATPの証明を、別体系の検査可能な証明として再構成する先行例です。現在のProver9/Vampire出力をそのまま扱えることは意味しません。
Matheliaでは、まず対象論理の小さなThmとその証明を固定し、Mizarの仮定・主張・証明へ写してローカル検査する実験が考えられます。依存する定義と公理も記録します。今回はこの接続の実行・対応形式・現行ツールの互換性確認までは行っていません。
MMLの定理を利用する場合も、名前や表示式が似ているだけでは取り込みません。記号の定義、型の条件、仮定、公理依存を照合したうえで、その翻訳を宣言します。
11 複数trustの整合性について残る課題
1_basis/2_thmel.book では、cvt+側をA、cls-elim側をBとしたときの受理条件を比較しています。共通の適用範囲でAならB、BならAを示すことが目標です。従来の規則には、外延性と命題変数の定数化の時点について反例があり、訂正案を記載しました。
今回のMetamath実験は、その訂正案の一般的な同値性を証明したものではありません。両経路の対象論理を比較するメタ定理と、Matheliaの実装がその翻訳を実行していることの検証が別に必要です。
第3のtrustを加えるときも、既存の全経路と常に同じ範囲を扱う必要はありません。どの範囲で同値か、どの方向の含意があるか、どの公理を追加しているかを宣言します。
共通範囲での一致だけでは、全体の健全性は完了しません。異なる経路で認めた結果を混ぜるhyperionの各規則にも根拠が必要です。可能なら共通の検査可能な証明体系へ証明を再構成するか、経路をまたぐ各規則をメタ定理として正当化します。
任意の公理体系の無矛盾性を、証明検査器が無条件に保証するとは主張しません。宣言した前提と検査器等への信頼を明示し、その前提のもとで誤った受理を防ぐ構成を説明します。
12 仕様案と現行実装の区別
2026-09-08に確認した mathelia/thmel/default.thmel の有効行には、backend・target・sort・translate・inference等があります。このファイルには、このBook群で説明している形のtrust文はまだ書かれていません。コメントにも旧い段階の説明があります。
したがって、Bookに書いたtrust構想や訂正案が、そのまま本番で実行されていると説明してはいけません。各規則について、Book上の定義、実装の入口、出力した対象問題、検査の証拠を対応付ける作業が必要です。今回、PHP・DB・.thmelの実装は変更していません。
13 次に完成させる検査単位
第一段：内包の所属の展開だけを扱う小さな自動exporterを作り、Mathelの解析結果からMetamathの証明までの対応を機械的に確認します。未対応のクラス量化等は理由付きで拒否します。今回の5件はその出発点ですが、自動exporterではありません。
第二段：変数捕獲を避ける代入・名前替え、クラス外延性、補助定義生成へ範囲を広げます。各段で、正常例と意味を壊した例を同じ外部検査器に通します。
第三段：cvt+とcls-elimの共通範囲を厳密に定義し、対象論理のモデルまたは証明の対応を示します。その後、hyperionの経路をまたぐ規則を検査します。
受入基準：他の人が公開した証明・依存宣言・固定した版を使って同じ結果を再現でき、何がまだ人手の対応付けやメタ数学的な前提に残るかを説明できることです。
14 再現用資料と参考文献
実験資料の README.md に手順、provenance.json に版、SHA256SUMS にファイルのハッシュがあります。ハッシュは同じ資料を使ったことの照合に用い、それ自体を証明とはしません。
固定したcommitは、metamath-exeが 022156b95faf9c8bf5baae23fe4d418f4bb8b990、set.mmが f3c3fc60589447ed0c23c4d3243898537ed55b32、mmverify.pyが 63a2aa3815cd5bf67892dbfc7f2048cbb177524c です。
positive.mm が正常版、bad-conclusion.mm, bad-distinct.mm, bad-rename.mm が不正版です。run_checks.py で二つの検査器を再実行できます。外部ツールの取得・ビルド方法もREADMEにあります。
補助定義を導入する翻訳の参考として、Kotelnikov・Kovács・Voronkovの FOOLの論文（2015）第3節も挙げます。FOOLで定義された意味に対する結果と、Matheliaの複数trustの比較は区別して利用します。