book集

section このBookの目的と到達点
txt MatheliaがThmを認めたとき、どの宣言と証拠に基づく判断なのかを、外部の人が追って検査できるようにします。このBookは、2026-09-08の調査と独立検査の結果、今後の接続仕様をまとめたものです。
txt 実測済み：内包・外延性・束縛変数の名前替えについて、手作業で対応を指定した5件の証明と、その依存証明272件を、独立に開発された二つのMetamath検査器で検査しました。正常版は両方が受理し、結論または変数条件を壊した3種類は両方が拒否しました。
txt 未達成：任意のFormelソースからの自動翻訳、Mathelia本番の外部検査接続、cvt+とcls-elimの一般的な受理条件の一致、hyperionを含む全体の健全性の証明です。Mizarとの接続は文献調査までで、今回は実行していません。
txt 本文は調査と仕様の説明です。このBook自体の表示成功や査読ボタンが、ここに書いたメタ定理の証明を意味するものではありません。
txt <a href="https://test2.atp-research.com/wp-content/themes/lightning/mathelia/1_basis/4_soundness_evidence.tar.gz">実験資料をダウンロード</a>できます。証明ファイル、失敗例、実測ログ、再実行スクリプト、版とSHA-256、対応表を含みます。

section Thm・trust・検査器を区別する
txt <code>P ◀ Γ</code> はgoalとsosを持つ形式的なThmです。◀自体に特定の論理での「推論できる」という意味を固定しません。Thmの変換と対象論理を指定し、その対象論理で成立することをtrustの受理条件にします。
txt したがって、健全性について説明するときは、まず「何を条件に認めると宣言したか」を示します。そのうえで、実際に出したOKがその条件を満たす証拠を持つかを確認します。未宣言の「翻訳前のThmの真偽」を持ち込む必要はありません。
txt 対象論理と証明器は別です。同じ対象論理を扱う複数の証明器・検査器を使えます。新しい検査器が増えただけなら、必ずしも新しいtrustは必要ありません。新しい公理体系や受理条件を採用する場合は、その違いを宣言します。
txt 外部検査器の受理は「指定された公理・仮定から、この対象言語の主張が導ける」という証拠になります。その公理体系の無矛盾性や、Matheliaの別のtrustとの一致まで自動的に保証するものではありません。

section 健全性の説明を四つに分ける
txt ① 宣言：入力したThm、適用する翻訳、その対象言語・論理、使用する定義・背景公理を明示します。版によって条件が変わるときは、別の検査条件として区別します。
txt ② 対応：Formel原文からFCL、FCLから対象言語へ、goal・sos・変数の範囲がどう写ったかを記録します。新しく追加したsosは元からの仮定と区別し、その生成規則も示します。外部検査器は、入力の取り違えまでは発見できません。
txt ③ 証明：対象言語の主張に対する証明を保存し、独立した検査器に渡します。最終結論だけでなく、仮定と変数条件が、翻訳した問題に一致することも照合します。
txt ④ 合成：複数のtrustで認めた結果をhyperionで使う各規則について、どの受理条件からどの受理条件へ進めるかを確認します。対象論理ごとの検査が正しくても、接続規則が違えば全体の根拠にはなりません。
txt この四つのうち、今回実際に行ったのは、範囲を限定した手作業の対応付けと、③の独立検査の実験です。①②④の全体を完成させたとはしません。

section 参考体系①：Metamathの仮想クラス
txt Metamathは形式体系を記述して証明を検査する枠組みです。ここで参考にする集合論のライブラリは、その一つであるset.mmです。Metamathという検査器とset.mmという公理・定義・定理の集まりを区別します。
txt set.mmの <a href="https://us.metamath.org/mpeuni/df-clab.html">df-clab</a> は、<code>x ∈ {y | φ} ⇔ [x/y]φ</code> によって内包への所属を扱います。クラス等号は <a href="https://us.metamath.org/mpeuni/df-cleq.html">df-cleq</a> で別に扱います。所属を代入へ展開する点は、Matheliaのcvtを検討する直接の参考です。
txt 重要な区別：set.mmのclass変数はクラス式を代入するメタ変数です。Matheliaのcソートを走る対象言語の変数と、そのまま同一視しません。今回の実験はクラス量化 <code>∀_</code>, <code>∃_</code> の翻訳を含みません。
txt 公式説明は、クラスの導入について消去可能性・保守性のメタ数学的な根拠も区別しています。検査器にとってはdf-clabやdf-cleqも公理的な宣言です。「定義と呼んだから無条件に安全」「Metamathが全体の保守性まで検査した」とは言えません。詳しくは <a href="https://us.metamath.org/mpeuni/mmset.html#class">Theory of Classes</a> を参照してください。
txt 以前の調査の「外延性は独立の前提なしに自動的に従う」という要約は不正確でした。今回の実測では、内包の基本式abidの依存先にはax-extがありませんが、クラス等号の特徴付けdfcleqの依存先にはax-extとdf-cleqがあります。何が必要かは、定理ごとに追います。

section 参考体系②：IsabelleとMizar
txt <a href="https://isabelle.in.tum.de/library/HOL/HOL/Set.html">Isabelle/HOLのSet理論</a> は、内包を <code>Collect (λx. P)</code> と表し、<code>a ∈ Collect(P) ⇔ P(a)</code> と <code>Collect(λx. x ∈ A) = A</code> を備えます。所属の展開と集合へ戻す性質をそろえ、型と束縛を明示する構成が参考になります。ただし型付き高階論理上の集合であり、その結果をそのままcソートの仕様とはしません。
txt Mizarの <a href="https://mizar.uwb.edu.pl/JFM/Vol2/fraenkel.abs.html">FRAENKEL</a> には、集合Aの要素を動かす <code>{F(x) where x is Element of A : P[x]}</code> と、そのような項を扱うschemeがあります。集合を構成する記法と、構成した項の性質を利用する規則の整理が参考になります。
txt <a href="https://mizar.uwb.edu.pl/library/">Mizar Mathematical Library</a> はTarski–Grothendieck集合論を基礎とします。利用したMMLの定理について、その公理依存をMathelia側でも明示する必要があります。MizarとMatheliaのクラスが同じだとも、両体系が一切接続できないとも、名前だけから判断しません。
txt この比較から取り入れる方針は、内包の構文・所属の展開・等号・変数条件・存在を支える仮定を分けて記述し、翻訳と証明の各段階でそれらを追跡できるようにすることです。

section 参考体系③：FOOLの翻訳
txt 関連する研究として、Evgenii Kotelnikov・Laura Kovács・Andrei Voronkov, <a href="https://arxiv.org/abs/1505.01682">A First Class Boolean Sort in First-Order Theorem Proving and TPTP</a>（2015）があります。以下の節番号はarXiv版v1によります。
txt FOOLは、真偽値を項としても扱い、if-then-elseやlet-inを使用できる多ソート一階論理の拡張です。第3節では、元の式を新しい式と補助定義の集合Dへ翻訳します。新しい記号の引数に自由変数を持たせ、そのソートも保持します。
txt 特に補題1・2は「追加した定義のもとで変換前後の式が同値」、補題4は「元の解釈を、新しい記号の定義を満たすように拡張できる」という二つの条件を分けています。補題3は翻訳の停止を述べます。これらの証明の詳細は論文では省略されています。
txt FOOLには翻訳前の言語の意味が定義されています。一方、このBookのThmは形式的なものなので、ここで比較するのは二つのtrustの対象論理です。補助定義を満たす解釈の拡張という方法を、その比較の参考にします。FOOLの結果をそのままMatheliaの受理条件の一致と読み替えることはできません。
txt FOOLのboolは真・偽の2要素です。クラス内包が要求するクラスの存在や、propごとに定数化するv^-elimは、この論文の結果だけでは正当化されません。ここでは、翻訳の仕様と根拠を組み立てる参考として挙げています。

section 今回の対応表
txt 内包の基本式：Matheliaで検討する「xが{x | P}に属する ⇔ P」に、set.mmのabidを対応させました。Metamathのφは任意のwffを代入できるメタ変数です。MatheliaのP^のpropごとの定数化とは、同じ機構だと仮定しません。
txt 否定・連言：abidにそれぞれ <code>¬φ</code> と <code>φ∧ψ</code> を代入した証明を作りました。内包の本体の構造を変えても同じ定理を利用できます。
txt クラス外延性：dfcleqを利用しました。量化する変数xがクラス式A,Bに現れないことに対応する、Metamathの <code>$d x A</code>, <code>$d x B</code> という条件を保持します。これは現在の記号の綴りが違うというだけでなく、後の代入も制限する条件です。
txt 束縛変数の名前替え：cbvabvを利用しました。<code>x=y ⇒ (φ⇔ψ)</code> という仮定と、<code>$d φ y</code>, <code>$d ψ x</code>, <code>$d x y</code> を必要とする条件付きの規則です。無条件に変数名を替えてよいという主張ではありません。
txt 未対応：任意のFCL、自由クラス変数の一般的な扱い、クラス量化、生成したsosと命題変数の範囲、任意のThm・Γの外部形式への変換です。対応表の詳細は実験資料のcorrespondence.mdにあります。

section 実験：正常版と意図的に壊した版
txt 公式set.mmから、abid・dfcleq・abbi・cbvabvに必要な宣言と依存証明を、公式検査器の <code>WRITE SOURCE /EXTRACT</code> で抽出しました。抽出部分には272件の証明と29件の$a宣言があり、そこに5件の$p証明を追加しました。今回新たな$a宣言は追加していません。29件には論理公理だけでなく構文や定義の宣言も含みます。
txt 正常版の5件は、内包の基本式・否定の本体・連言の本体・クラス等号・条件付きの名前替えです。依存証明を省略せず、計277件すべてを検査しました。
txt 検査器は <a href="https://github.com/metamath/metamath-exe">metamath-exe</a>（C実装）と <a href="https://github.com/david-a-wheeler/mmverify.py">mmverify.py</a>（Python実装）です。両方が正常版を受理しました。
txt 不正版①では、否定の内包の右辺から否定だけを消しました。両検査器とも、証明の結論が主張と一致しないことを理由に拒否しました。
txt 不正版②では、外延性の証明から <code>$d x A</code> を消しました。両検査器とも、必要な変数条件が欠けていることを理由に拒否しました。
txt 不正版③では、名前替えの証明から <code>$d φ y</code> を消しました。これも両検査器が必要な変数条件の欠落として拒否しました。
txt 観測結果は正常1種類×2検査器の受理、不正3種類×2検査器の拒否です。有限個の例の検査なので、検査器にあらゆる誤りが無いことや、Mathelia全体の正しさの証明にはなりません。

section 実測で見つかった結果受取の注意点
txt 今回使用したmetamath-exeでは、不正版に対して明確な <code>?Error</code> を出した後でも、終了コードは0で、最後には <code>All proofs in the database were verified</code> という文が出ました。終了コード0や最後の成功風の文だけでOKとしてはいけません。
txt 実験用スクリプトは、エラー診断、検査完了、未完成証明の印を確認し、二つの検査器の結果を記録します。mmverify.pyも三つの不正版を非0の終了コードで拒否しました。生のログを実験資料に含めています。
txt これは使用した版での観測です。将来の本番接続には、版を固定した出力契約、入力と結果の対応照合、エラーや未完成証明を受理しない検査が必要です。今回の実験用スクリプトを、そのまま認証済みの汎用adapterとはしません。

section 第3のtrustか、既存trustの別検査か
txt 利用方法は三つあります。第一に、既存の対象論理の証明を別形式へ移し、独立検査器で再検査する方法です。対象論理と仮定が同じであることを確認できれば、既存のtrustを別の検査器で確認する構成にできます。
txt 第二に、set.mmやMMLの特定の公理・定義・定理を利用する翻訳を宣言し、その成立を第3のtrust条件にする方法です。この場合、体系名だけでなく、実際に使用できる公理・定義と翻訳の適用範囲を指定します。
txt 第三に、Matheliaの翻訳やhyperionの規則を外部体系で形式化し、そのメタ定理を検査する方法です。自作の規則をそのまま外部体系の公理として登録するだけでは、その規則の健全性を証明したことにはなりません。
txt 各結果には、どの形式的Thmに対応するか、対象の主張と仮定、公理依存、自由変数・代入条件、証明、検査器とライブラリの版を結び付けます。生のOKだけを返す接続にはしません。

section Mizarを利用する具体的な道
txt Jesse Alamaの <a href="https://arxiv.org/abs/1204.6615">Escape to Mizar for ATPs</a>（2012）は、Eの導出をMizarの証明へ写すツールを報告しています。外部ATPの証明を、別体系の検査可能な証明として再構成する先行例です。現在のProver9/Vampire出力をそのまま扱えることは意味しません。
txt Matheliaでは、まず対象論理の小さなThmとその証明を固定し、Mizarの仮定・主張・証明へ写してローカル検査する実験が考えられます。依存する定義と公理も記録します。今回はこの接続の実行・対応形式・現行ツールの互換性確認までは行っていません。
txt MMLの定理を利用する場合も、名前や表示式が似ているだけでは取り込みません。記号の定義、型の条件、仮定、公理依存を照合したうえで、その翻訳を宣言します。

section 複数trustの整合性について残る課題
txt <code>1_basis/2_thmel.book</code> では、cvt+側をA、cls-elim側をBとしたときの受理条件を比較しています。共通の適用範囲でAならB、BならAを示すことが目標です。外延性と命題変数の定数化の時点に関する定式化は、下の「モデル比較によるA(T)とB(T)の検証方針」「A(T)とB(T)の定式化」節にまとめました。現在、両者が定義上意味を持つ範囲で確認済みの同値性の反例はありません。自由クラス変数の例は、cvt+の後にW+の∈_が残り、一階翻訳がエラーとなるため、その範囲には入りません。
txt 今回のMetamath実験は、その定式化の一般的な同値性を証明したものではありません。両経路の対象論理を比較するメタ定理と、Matheliaの実装がその翻訳を実行していることの検証が別に必要です。
txt 第3のtrustを加えるときも、既存の全経路と常に同じ範囲を扱う必要はありません。どの範囲で同値か、どの方向の含意があるか、どの公理を追加しているかを宣言します。
txt 共通範囲での一致だけでは、全体の健全性は完了しません。異なる経路で認めた結果を混ぜるhyperionの各規則にも根拠が必要です。可能なら共通の検査可能な証明体系へ証明を再構成するか、経路をまたぐ各規則をメタ定理として正当化します。
txt 任意の公理体系の無矛盾性を、証明検査器が無条件に保証するとは主張しません。宣言した前提と検査器等への信頼を明示し、その前提のもとで誤った受理を防ぐ構成を説明します。

section モデル比較によるA(T)とB(T)の検証方針
txt cls-elimが追加する所属条件は、多ソート側で許されるモデルを制限します。例えばs領域が1要素でc領域に空クラスしかない構造は、<code>∀x (x ∈ k ⇔ ⊤)</code> を満たせません。この事実だけでtrustが不正だとはしません。
txt 一致を調べるには、二つの対象論理の間で反例を移せるかを調べます。A(T)ならB(T)を示すには、B(T)の反例からA(T)の反例を構成できれば十分です。B(T)ならA(T)には反対方向の構成が必要です。
txt 特に一階側の反例から多ソート側を構成するときは、クラス領域・所属関係・新しいクラス値の関数を用意し、cls-elimで追加した仮定をすべて満たしながら、sosを真、goalを偽にできることを確認します。
txt 未解決：この構成を一般に行えることは、まだ示していません。Pの中のクラス量化、自由なクラス変数、クラス等号、命題変数、追加する定義の相互作用まで含めた条件が必要です。

section A(T)とB(T)の定式化：外延性と命題変数の前処理F
txt <code>soundness_status.book</code> に記録した外延性・命題変数の二つの実装不一致（W+.を反映する前の受理条件に対する反例だった）を踏まえ、A(T)・B(T)を次のように定式化します。Extは外延性を翻訳後のsosに追加する操作、1とscは命題変数の残らないFormをそれぞれの対象言語へ写す翻訳です。
txt 外延性：--|側で、クラス等号を対象論理の等号として扱うときは、翻訳後のsosにクラス外延性を追加します。現行実装ではクラス等号を使用するときに生成します。対象論理の記法で <code>∀C:c ∀D:c ((∀x:s (E(x,C) ⇔ E(x,D))) ⇒ C=D)</code> です。Eは所属の翻訳先です。逆向きは対象論理の等号の性質から出ます。この外延性は、元のsosに=_.が書かれているかに依存しない、翻訳が生成する仮定とします。
txt 命題変数の前処理F：命題変数の定数化は、cls-elimによってsosを増やす前に行います。FormelによるFCL変換後の元のgoalと各sosを単位とし、propごとに独立な、衝突しない命題定数を割り当てます。内包の本体を含め、そのprop全体の出現を一貫して置換します。この前処理をFと呼びます。
txt Fの後で生成した補助定義には、置換済みの命題定数をそのまま引き継ぎます。生成した定義を新しい独立なpropとして再定数化しません。cvt規則中の穴には置換済みの式を代入します。cvtが新たな裸の命題変数を導入する規則については、その範囲と割当てを別に指定する必要があります。この定式化の保証範囲には、そのような規則は含めません。Fは、一階+v^・多ソート+v^の論理の定義として既に導入したv^-elimの入力言語を、説明なしに変更するものではありません。
txt <code>A(T) … T|F|cvt+|1</code> が一階論理で成立する。
txt <code>B(T) … T|F|cls-elim|sc|Ext</code> が{s,c}ソート論理で成立する。
txt 対応するtrustは「trust T if A(T)」および「trust T if B(T)」です。-|と--|をこの経路に改める場合、従来の経路と同じだとはせず、受理条件の訂正として扱います。
txt 確認できた範囲：<code>soundness_status.book</code> に記録した外延性・命題変数の二つの例については、A(T)とB(T)の両方が成立します。外延性の例はExtと等号の性質から、命題変数の例は生成したsosとgoalが束縛変数の名前以外同じになることから従います。
txt なお未解決：A(T)ならB(T)、および一階側の適用範囲でB(T)ならA(T)という一般的な含意は、まだ証明していません。他のcvt規則に対応する定義の扱い、自由なクラス変数の範囲、内包の補助仮定を満たすモデルの構成、hyperionとの接続が残ります。外延性だけを加えればすべてのcvt規則との対応が取れる、とはしません。

section 仕様案と現行実装の区別
txt 2026-09-08に確認した <code>mathelia/thmel/default.thmel</code>（2026-09-13に <code>mathelia/common/default.thmel</code> へ移動）の有効行には、backend・target・sort・translate・inference等があります。このファイルには、このBook群で説明している形のtrust文はまだ書かれていません。コメントにも旧い段階の説明があります。
txt したがって、Bookに書いたtrust構想や訂正案が、そのまま本番で実行されていると説明してはいけません。各規則について、Book上の定義、実装の入口、出力した対象問題、検査の証拠を対応付ける作業が必要です。今回、PHP・DB・.thmelの実装は変更していません。

section 次に完成させる検査単位
txt 第一段：内包の所属の展開だけを扱う小さな自動exporterを作り、Formelの解析結果からMetamathの証明までの対応を機械的に確認します。未対応のクラス量化等は理由付きで拒否します。今回の5件はその出発点ですが、自動exporterではありません。
txt 第二段：変数捕獲を避ける代入・名前替え、クラス外延性、補助定義生成へ範囲を広げます。各段で、正常例と意味を壊した例を同じ外部検査器に通します。
txt 第三段：cvt+とcls-elimの共通範囲を厳密に定義し、対象論理のモデルまたは証明の対応を示します。その後、hyperionの経路をまたぐ規則を検査します。
txt 受入基準：他の人が公開した証明・依存宣言・固定した版を使って同じ結果を再現でき、何がまだ人手の対応付けやメタ数学的な前提に残るかを説明できることです。

section 再現用資料と参考文献
txt 実験資料の <code>README.md</code> に手順、<code>provenance.json</code> に版、<code>SHA256SUMS</code> にファイルのハッシュがあります。ハッシュは同じ資料を使ったことの照合に用い、それ自体を証明とはしません。
txt 固定したcommitは、metamath-exeが <code>022156b95faf9c8bf5baae23fe4d418f4bb8b990</code>、set.mmが <code>f3c3fc60589447ed0c23c4d3243898537ed55b32</code>、mmverify.pyが <code>63a2aa3815cd5bf67892dbfc7f2048cbb177524c</code> です。
txt <code>positive.mm</code> が正常版、<code>bad-conclusion.mm</code>, <code>bad-distinct.mm</code>, <code>bad-rename.mm</code> が不正版です。<code>run_checks.py</code> で二つの検査器を再実行できます。外部ツールの取得・ビルド方法もREADMEにあります。
txt 補助定義を導入する翻訳の参考文献は、上の「参考体系③：FOOLの翻訳」節にまとめました。

1_basis/soundness.book

`1_basis/soundness.book`