メタマス

メタマス証明エクスプローラー
	Metamath Proof Explorerの証明
サイトの種類	オンライン百科事典
本部	アメリカ合衆国
所有者	ノーマン・メギル
作成者	ノーマン・メギル
メールアドレス	us.metamath.org/mpeuni/mmset.html
コマーシャル	いいえ
登録	いいえ

メタマス
開発者	ノーマン・メギル
初回リリース	2005年6月0.07 ; 19年前
安定版リリース	0.198 / 2021年8月7日; 3年前
リポジトリ	github.com/metamath/metamath-exe ;
書かれた	ANSI C
オペレーティング·システム	Linux、Windows、macOS
タイプ	コンピュータ支援による校正
ライセンス	GNU 一般公衆利用許諾書(データベース用のクリエイティブコモンズパブリックドメイン提供)
Webサイト	メタマス

Metamathは数学の証明をアーカイブし検証するための形式言語とそれに関連するコンピュータプログラム（証明支援プログラム）です。 ^{[2] Metamathを使用して、}論理学、集合論、数論、代数、位相幾何学、解析学などの標準的な結果を網羅する証明済み定理のデータベースがいくつか開発されています。^[3]

2023年までに、Metamathは「100の定理の形式化」チャレンジの100の定理のうち74 ^[4]を証明するために使用されました。 ^[5]少なくとも19の証明検証者がMetamath形式を使用しています。^[6] MetamathのWebサイトでは、対話的に閲覧できる形式化された定理のデータベースを提供しています。^[7]

メタマス言語

Metamath言語は形式システムのためのメタ言語である。Metamath言語には特定のロジックは組み込まれていない。代わりに、推論ルール（公理として主張されるか、後で証明される）を適用できることを証明する方法と見なすことができます。証明された定理の最大のデータベースは、従来の一階述語論理とZFC集合論に従っています。^[8]

Metamath言語設計（定義、公理、推論規則、定理を記述するために使用）は、簡潔さに重点を置いています。証明は、変数置換に基づくアルゴリズムを使用してチェックされます。このアルゴリズムには、置換が行われた後もどの変数が区別されなければならないかについてのオプションの条件もあります。^[9]

言語の基礎

数式の構築に使用できる記号のセットは、$c(定数記号) および$v(変数記号) ステートメントを使用して宣言されます。例:

$( 使用する定数シンボルを宣言します $)
    $c 0 + = -> ( ) 項 wff |- $.
$( 使用するメタ変数を宣言します $)
    $vtrs PQ $。

式の文法は、$f(浮動型(変数型)仮説)と$a(公理的アサーション)ステートメントの組み合わせを使用して指定されます。例:

$( メタ変数のプロパティを指定します $)
    tt $f 用語 t $。
    tr $f 用語 r $。
    ts $f 用語 s $。
    wp $f wff P $。
    wq $f wff Q $。
$( 「wff」の定義 (パート 1) $)
    weq $a wff t = r $ です。
$( 「wff」の定義 (パート 2) $)
    wim $a wff ( P -> Q ) $ を実行します。

公理と推論規則は、ブロックスコープとオプション (必須仮説) ステートメントとともにステートメントで指定されます。$a例: ${$}$e

$( 状態公理 a1 $)
    a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( 状態公理 a2 $)
    a2 $a |- ( t + 0 ) = t $です。
    ${
       最小$e |- P $。
       メジャー $e |- ( P -> Q ) $。
$( 手口推論ルールを定義 $)
       mp $a |- Q $。
    $}

1 つの構成要素であるステートメントを使用して構文規則、公理スキーマ、および推論規則をキャプチャすることで、複雑な型システムに依存せずに、高次論理フレームワーク$aと同様のレベルの柔軟性を提供することを目的としています。

証明

定理（および導出された推論規則）は$pステートメントで記述されます。たとえば、次のようになります。

$( 定理を証明する $)
    th1 $p |- t = t $=
  $( ここにその証拠があります: $)
       tt ze tpl tt weq tt tt weq tt a2 tt tze tpl
       tt weq tt tze tpl tt weq tt tt weq wim tt a2
       tt tze tpl tt tt a1 mp mp
     $。

声明の中に証明が含まれていることに注意してください$p。次の詳細な証明が省略されています。

tt $ f用語t              
tze $用語0             
1,2 tpl $ 1項( t + 0 )              
3,1 weq $ a wff ( t + 0 ) = t                
1,1 weq $ a wff t = t            
1 a2 $ a |- ( t + 0 ) = t                   
1,2 tpl $ 1項( t + 0 )              
7,1 weq $ a wff ( t + 0 ) = t                
1,2 tpl $ 1項( t + 0 )              
9,1 weq $ a wff ( t + 0 ) = t                
1,1 weq $ a wff t = t            
10,11 wim $ a wff ( ( t + 0 ) = t -> t = t )                    
1 a2 $ a |- ( t + 0 ) = t                   
1,2 tpl $ 1項( t + 0 )              
14,1,1 a1 $ a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )                              
8,12,13,15 mp $ a |- ( ( t + 0 ) = t -> t = t )                
4,5,6,16 mp $ a |- t = t

証明の「本質的な」形式では、構文の詳細を省略し、より一般的な表現を残します。

a2 $ a |- ( t + 0 ) = t                     
a2 $ a |- ( t + 0 ) = t                     
a1 $ a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )                                     
2,3 mp $ a |- ( ( t + 0 ) = t -> t = t )                        
1,4 mp $ a |- t = t

代替

すべての Metamath 証明手順では、単一の置換規則を使用します。これは、単に変数を式に置き換えるだけであり、述語計算に関する著作で説明されている適切な置換ではありません。適切な置換は、それをサポートする Metamath データベースでは、Metamath 言語自体に組み込まれているものではなく、派生した構造です。

置換ルールでは、使用されているロジックシステムについては何も想定せず、変数の置換が正しく行われることだけを要求します。

このアルゴリズムがどのように機能するかの詳細な例を以下に示します。Metamath 2p2e4Proof Explorer ( set.mm ) の定理のステップ 1 と 2 が左側に示されています。定理を使用するときに、Metamath が置換アルゴリズムを使用して、ステップ 2 がステップ 1 の論理的帰結であることを確認する方法を説明しましょうopreq2i。ステップ 2 は、 $( 2 + 2 ) = ( 2 + ( 1 + 1 ) )$ であると述べています。これが定理の結論ですopreq2i。定理は、 $A$ $=$ $B$ の場合、 $($ $CFA$ $) = ($ $CFB$ $)$ opreq2iであると述べています。この定理は、教科書にこの難解な形式では決して登場しませんが、その読みやすい定式化は平凡です。つまり、2 つの量が等しい場合、演算で一方を他方で置き換えることができます。証明を確認するために、Metamath は $($ $CFA$ $) = ($ $CFB$ $)を$ $( 2 + 2 ) = ( 2 + ( 1 + 1 ) )$ と統合しようとします。それを実現する方法は1つしかありません $。C$ を $2$ 、 $F$ を $+$ 、 $A$ を2と $B を$ $( 1 + 1 )$ で置き換えます。そこで Metamath はの前提を使用しますopreq2i。この前提は $A = B$ であることを示しています。以前の計算の結果、Metamath は $A を$ 次のように置き換える必要があることを知っています。2と $B を$ $( 1 + 1 )$ で割ったものです。前提 $A = B は$ $2=( 1 + 1 )$ となり、したがってステップ 1 が生成されます。今度はステップ 1 がと統一されますdf-2。df-2は数の定義であり2、であると述べています2 = ( 1 + 1 )。ここでの統一は単に定数の問題であり、簡単です (代入する変数の問題はありません)。これで検証は終了し、の証明のこれら 2 つのステップ2p2e4は正しいです。

$Metamath が( 2 + 2 ) を$ $B$ と統合する場合、構文規則が尊重されていることを確認する必要があります。実際、 $B に$ は型があるため、Metamath は $( 2 + 2 )$ も型付けされているclassことを確認する必要があります。 class

メタマス証明チェッカー

Metamath プログラムは、Metamath 言語を使用して記述されたデータベースを操作するために作成されたオリジナルのプログラムです。テキスト (コマンドライン) インターフェイスを備え、C で記述されています。Metamath データベースをメモリに読み込み、データベースの証明を検証し、データベースを変更し (特に証明を追加して)、それらをストレージに書き戻すことができます。

ユーザーが証明を入力できるようにするproveコマンドと、既存の証明を検索するメカニズムがあります。

Metamath プログラムは、ステートメントをHTMLまたはTeX表記に変換できます。たとえば、 set.mm からmodus ponens公理を次のように出力できます。

\vdash \varphi \quad \&\quad \vdash (\varphi \rightarrow \psi )\quad \Rightarrow \quad \vdash \psi

Metamathデータベースを処理できるプログラムは他にもたくさんありますが、特にMetamath形式を使用するデータベース用の証明検証プログラムは少なくとも19個あります。^[10]

Metamath データベース

Metamath の Web サイトには、さまざまな公理系から派生した定理を保存するデータベースがいくつかホストされています。ほとんどのデータベース ( .mmファイル) には、「エクスプローラー」と呼ばれる関連インターフェイスがあり、これを使用すると、Web サイト上でステートメントと証明を対話的に、ユーザーフレンドリーな方法でナビゲートできます。ほとんどのデータベースは、ヒルベルトの形式演繹システムを使用していますが、これは必須ではありません。

メタマス証明エクスプローラー

Metamath Proof Explorer ( set.mmに記録) がメインのデータベースです。これは古典的な一階述語論理とZFC集合論に基づいています (必要に応じて、たとえば圏論でTarski-Grothendieck 集合論が追加されます)。このデータベースは 30 年以上維持されています ( set.mmの最初の証明は 1992 年 9 月のものです)。このデータベースには、集合論 (順序数と基数、再帰、選択公理の同等物、連続体仮説など)、実数系と複素数系の構築、順序理論、グラフ理論、抽象代数、線型代数、一般位相幾何学、実解析と複素解析、ヒルベルト空間、数論、初等幾何学などの分野の発展が含まれています。^[11]

Metamath Proof Explorerは、Metamathと組み合わせて使用できる多くの教科書を参照します。^[12]したがって、数学の勉強に興味のある人は、これらの本と組み合わせてMetamathを使用し、証明された主張が文献と一致しているかどうかを確認することができます。

直観主義論理の探検家

このデータベースは、直観主義論理の公理から始まり、構成的集合論の公理系へと進み、構成的な観点から数学を展開します。

新しい基礎探検家

このデータベースは、クワインの新基礎集合論から数学を展開します。

高階論理エクスプローラー

このデータベースは高階論理から始まり、一階論理と ZFC 集合論の公理に相当するものを導出します。

エクスプローラーなしのデータベース

Metamathのウェブサイトには、探検家とは関係ないが注目に値するデータベースがいくつかある。Robert Solovayが書いたデータベースpeano.mmはペアノ算術を形式化したものである。データベースnat.mm ^[13]は自然演繹を形式化したものである。データベースmiu.mmはゲーデル、エッシャー、バッハが提示した形式体系MIUに基づいてMUパズルを形式化したものである。

昔の探検家

Metamath の Web サイトには、現在 Metamath Proof Explorer に統合されているヒルベルト空間理論に関する定理を提示する「Hilbert Space Explorer」や、直交モジュラー格子の理論から始まる量子論理を展開する「Quantum Logic Explorer」など、現在はメンテナンスされていない古いデータベースもいくつかホストされています。

自然演繹

Metamath は証明に関する非常に一般的な概念 (つまり、推論規則によって接続された式のツリー) を持ち、ソフトウェアに特定のロジックが組み込まれていないため、ヒルベルトスタイルのロジックやシークエントベースのロジック、さらにはラムダ計算など、さまざまな種類のロジックで Metamath を使用できます。

ただし、Metamath は自然演繹システムを直接サポートしていません。前述のように、データベースnat.mmは自然演繹を形式化します。Metamath Proof Explorer (およびそのデータベースset.mm ) は、代わりに、ヒルベルトスタイルのロジック内で自然演繹アプローチを使用できるようにする一連の規則を使用します。

メタマスに関連するその他の作品

証明チェッカー

Metamath に実装された設計アイデアを使用して、Raph Levien は、わずか 500 行の Python コードで非常に小さな証明チェッカーmmverify.py を実装しました。

Ghilbertは、mmverify.pyをベースにした類似の言語だが、より精巧な言語である。^[14] Levienは、複数の人が協力できるシステムを実装したいと考えており、彼の研究ではモジュール性と小さな理論間のつながりを重視している。

Levienの独創的な研究を利用して、Metamathの設計原則の実装がさまざまな言語で実装されてきました。Juha ArpiainenはCommon LispでBourbakiと呼ばれる独自の証明チェッカーを実装しました^{[15]。また、Marnix Kloosterは}HaskellでHmmと呼ばれる証明チェッカーをコーディングしました^[16]。

これらはすべて、正式なシステムチェッカーコーディングに Metamath の全体的なアプローチを使用していますが、独自の新しい概念も実装しています。

編集者

Mel O'Cat は、証明入力用のグラフィカルユーザーインターフェイスを提供するMmj2というシステムを設計しました。 ^[17] Mel O'Cat の当初の目的は、ユーザーが単に式を入力して、Mmj2 がそれらを結び付ける適切な推論規則を見つけるだけで証明を入力できるようにすることでした。対照的に、Metamath では定理名しか入力できません。式を直接入力することはできません。Mmj2 では、証明を前方または後方に入力することもできます (Metamath では証明を後方にしか入力できません)。さらに、Mmj2には実際の文法パーサーがあります (Metamath とは異なります)。この技術的な違いにより、ユーザーはより快適に使用できます。特に、Metamath は分析する複数の式の間で躊躇することがあり (そのほとんどは無意味です)、ユーザーに選択を求めます。Mmj2 ではこの制限はなくなりました。

また、ウィリアム・ヘイルによる、Metamathにグラフィカル・ユーザー・インターフェースを追加するMmideというプロジェクトもあります。^[18]一方、ポール・チャップマンは、置換が行われる前と後の参照定理を確認できるハイライト機能を備えた新しい証明ブラウザの開発に取り組んでいます。

Milpgame は、Filip Cernatescu によって書かれた、Metamath 言語 (set.mm) 用のグラフィックユーザーインターフェイスを備えた証明アシスタントおよびチェッカー (何か問題があった場合にのみメッセージを表示します) であり、オープンソース (MIT ライセンス) の Java アプリケーション (クロスプラットフォームアプリケーション: Windows、Linux、Mac OS) です。ユーザーは、証明するステートメントに対して前方および後方の 2 つのモードでデモンストレーション (証明) を入力できます。Milpgame は、ステートメントが適切に構成されているかどうか (構文検証機能がある) をチェックします。ダミーリンク定理を使用せずに、未完成の証明を保存できます。デモンストレーションはツリーとして表示され、ステートメントは HTML 定義 (タイプセッティングの章で定義) を使用して表示されます。Milpgame は、Java .jar (NetBeans IDE で記述された JRE バージョン 6 アップデート 24) として配布されます。

参照

参考文献

^ “リリース 0.198”. 2021年8月8日. 2022年7月27日閲覧。
^ Megill, Norman; Wheeler, David A. (2019-06-02). Metamath: 数学的証明のためのコンピュータ言語 (第2版). モリスビル、ノースカロライナ州、米国: Lulu Press . p. 248. ISBN 978-0-359-70223-7。
^ Megill, Norman. 「Metamath とは何か?」Metamath ホームページ。
^ メタマス100。
^ 「100の定理の形式化」。
^ Megill, Norman. 「既知のメタマス証明検証者」。 2022年10月8日閲覧。
^ 「定理リストの目次 - Metamath Proof Explorer」。us.metamath.org 。 2023年9月4日閲覧。
^ Wiedijk, Freek. 「世界の17の証明者」（PDF）。pp. 103–105 。 2023年10月14日閲覧。
^ Megill, Norman. 「証明の仕組み」Metamath Proof Explorer ホームページ。
^ Megill, Norman. 「既知のメタマス証明検証者」。 2022年10月8日閲覧。
^ Wheeler, David A. 「Metamath set.mm の貢献を Gource で 2019-10-04 まで閲覧」。YouTube。2021-12-19時点のオリジナルよりアーカイブ。
^ メギル、ノーマン。「読書の提案」。メタマス。
^ Liné, Frédéric. 「自然演繹に基づく Metamath システム」。2012 年 12 月 28 日時点のオリジナルよりアーカイブ。
^ レヴィーン、ラファエル。「ギルバート」。
^ Arpiainen, Juha. 「Bourbaki のプレゼンテーション」。2012 年 12 月 28 日時点のオリジナルよりアーカイブ。
^ Klooster, Marnix. 「Hmmのプレゼンテーション」。2012年4月2日時点のオリジナルよりアーカイブ。
^ O'Cat, Mel. 「mmj2のプレゼンテーション」。2013年12月19日時点のオリジナルよりアーカイブ。
^ Hale, William. 「mmide のプレゼンテーション」。2012 年 12 月 28 日時点のオリジナルよりアーカイブ。

外部リンク

Metamath: 公式サイト。
数学者は Metamath についてどう考えているか: Metamath に関する意見。

[wikidata-7d32d1a3a149e85be2acb3831539d0106d3c08f6-v18-1] “リリース 0.198”. 2021年8月8日. 2022年7月27日閲覧。

[metamath-book-2] Megill, Norman; Wheeler, David A. (2019-06-02). Metamath: 数学的証明のためのコンピュータ言語 (第2版). モリスビル、ノースカロライナ州、米国: Lulu Press . p. 248. ISBN 978-0-359-70223-7。

[3] Megill, Norman. 「Metamath とは何か?」Metamath ホームページ。

[4] メタマス100。

[5] 「100の定理の形式化」。

[6] Megill, Norman. 「既知のメタマス証明検証者」。 2022年10月8日閲覧。

[7] 「定理リストの目次 - Metamath Proof Explorer」。us.metamath.org 。 2023年9月4日閲覧。

[8] Wiedijk, Freek. 「世界の17の証明者」（PDF）。pp. 103–105 。 2023年10月14日閲覧。

[howpswork-9] Megill, Norman. 「証明の仕組み」Metamath Proof Explorer ホームページ。

[10] Megill, Norman. 「既知のメタマス証明検証者」。 2022年10月8日閲覧。

[gource-11] Wheeler, David A. 「Metamath set.mm の貢献を Gource で 2019-10-04 まで閲覧」。YouTube。2021-12-19時点のオリジナルよりアーカイブ。

[reading-12] メギル、ノーマン。「読書の提案」。メタマス。

[natmm-13] Liné, Frédéric. 「自然演繹に基づく Metamath システム」。2012 年 12 月 28 日時点のオリジナルよりアーカイブ。

[ghilbert-14] レヴィーン、ラファエル。「ギルバート」。

[bourbaki-15] Arpiainen, Juha. 「Bourbaki のプレゼンテーション」。2012 年 12 月 28 日時点のオリジナルよりアーカイブ。

[Hmm-16] Klooster, Marnix. 「Hmmのプレゼンテーション」。2012年4月2日時点のオリジナルよりアーカイブ。

[mmj2-17] O'Cat, Mel. 「mmj2のプレゼンテーション」。2013年12月19日時点のオリジナルよりアーカイブ。

[mmide-18] Hale, William. 「mmide のプレゼンテーション」。2012 年 12 月 28 日時点のオリジナルよりアーカイブ。