Mizar証明の抜群な分かりやすさ

Mizarの処理系はまったく使いにくいです。その使い勝手は極悪ですわ。それにも関わらず僕が我慢して使おうとしているのは、Mizarの構文と意味モデルが素晴らしいからです。最高ですわ。特に、他の証明系のタクティク言語の難読さに辟易した人には感激もんです。

「証明検証系Mizarを試してみる」で例に出した次の証明記述コードを例にします。

reserve i,j,k,l,m,n for natural number;
i+k = j+k implies i=j;
proof
  defpred P[natural number] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume B0: i+0 = j+0;
    B1: i+0 = i by INDUCT:3;
    B2: j+0 = j by INDUCT:3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k st P[k] holds P[succ k]
  proof
    let l such that C1: P[l];
    assume C2: i+succ l=j+succ l;
    then C3: succ(i+l) = j+succ l by C2,INDUCT:4
    .= succ(j+l) by INDUCT:4;
    hence thesis by C1,INDUCT:2;
  end;
  for k holds P[k] from INDUCT:sch 1(A1,A2);
  hence thesis;
end;

これは、チュートリアル・スライド http://mizar.org/cicm_tutorial/mizar.pdf の45ページから取ったものですが、コンパイル（検証）できませんでした。単にenviron部が書いてないだけでなく、構文エラーがあります。また、MML（Mizar Mathematical Library）には存在しないアーティクルを参照しています。

なんとかコンパイルできるように修正したコードが以下です。修正してみると、証明すべき命題 i + k = j + k implies i = j はちょっと簡単過ぎて、自動証明（証明探索）能力がほとんどないMizarでさえ自力で（人間の支援なしで）証明しちゃいます。トホホ*1。まーそれでも、数学的帰納法の使用例としては意味があるでしょう。完全なenviron部と、証明内で使用する基本命題を記述しています。

:: tihs is induct_samp.miz
:: verified by: Mizar Ver. 8.1.04 (Win32/FPC)
::
environ

:: From NAT_1
 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;

 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;

 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;

 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;

 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

:: Added
 constructors NAT_1;
 registrations NAT_1;
 schemes NAT_1;

begin

BASIC1: for n, m being Nat holds
        n + 1 = m  + 1 implies n = m;
BASIC2: for n being Nat holds
        n + 0 = n;
BASIC3: for n, m being Nat holds
        n + (m + 1) = (n + m) + 1;

reserve i,j,k,l,m,n for Nat;

i + k = j + k implies i = j
proof
  defpred P[Nat] means
    i + $1 = j + $1 implies i = j;
  A1: P[0]
  proof
    assume
    B0: i + 0 = j + 0;
    ::hereupon
    B1: i + 0 = i by BASIC2;
    B2: j + 0 = j by BASIC2;
    hence thesis by B0,B1,B2;
  end;
  A2: for k be Nat st P[k] holds P[k + 1]
  proof
    let m such that C1: P[m];
    assume C2: i + (m + 1) = j + (m + 1);
    then C3: (i + m) + 1 = j + (m + 1) by C2,BASIC3
                        .= (j + m) + 1 by BASIC3;
    hence thesis by C1,BASIC1;
  end;
  for k holds P[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

簡単なことを持って回って言ってるような所に目をつぶれば、証明の筋は読み取れるでしょう。英語ベースだからという点で日本人には分かりにくいかも知れません。キーワードを日本語に置換してみましょう。以下は、ほとんど文字列置換ですが、一部は日本語として自然な語順になるように語の入れ替えをしています。また、Mizarのラベルは、アンダースコアを含めたり括弧で囲んだり出来ませんが、その制限は取り払って考えています。コメントも若干足しています。

基本命題_1: 任意の 自然数 n, m に対して、
　　　　    n + 1 = m + 1 ならば n = m 。
基本命題_2: 任意の 自然数 n に対して、
            n + 0 = n 。
基本命題_3: 任意の 自然数 n, m に対して、
            n + (m + 1) = (n + m) + 1 。

以下、i, j, k, l, m, n は 自然数 とする。
このとき、
i + k = j + k ならば i = j
証明:
  まず 述語を定義する: P[自然数] とは ※（その自然数は $1）
    i + $1 = j + $1 ならば i = j であること。
  (A1): P[0] ※帰納法のベース: i + 0 = j + 0 ⇒ i = j
  証明:
    次を仮定する:
    (B0): i + 0 = j + 0 。
    このとき、
    (B1): i + 0 = i その根拠は 基本命題_2 。
    (B2): j + 0 = j その根拠は 基本命題_2 。
    従って 目的の命題、その根拠は B0,B1,B2 。※目的の命題: i = j
  終り。
  (A2): 任意の k ただし P[k] に対して P[k + 1] ※帰納法のステップ
  ※ (i + k = j + k ⇒ i = j) ⇒ (i + (k + 1) = j + (k + 1) ⇒ i = j)
  証明:
    m を導入、ただし
    (C1): P[m] 。※ i + m = j + m ⇒ i = j
    次を仮定する:
    (C2): i + (m + 1) = j + (m + 1) 。
    すると
    (C3): (i + m) + 1 = j + (m + 1) その根拠は C2,基本命題_3
                     .= (j + m) + 1  その根拠は 基本命題_3。
    従って 目的の命題、その根拠は C1,基本命題_1。※目的の命題: i = j
  終り。
  任意の k に対して P[k]、その推論は 数学的帰納法(A1,A2)。
  従って 目的の命題。
終り。

以下に対応表を示します。順番は語の出現順です。

日本語	Mizar
任意の	for
自然数（語順変更）	being Nat
に対して	holds
ならば	implies
。	;
以下	（捨てる）
、	（捨てる）
は とする（語順変更）	reserve
このとき	（捨てる）
証明:	proof
まず	（捨てる）
述語を定義する:	defpred
とは	means
※	::（コメント）
であること	（捨てる）
次を仮定する:	assume
その根拠は	by
従って	hence
目的の命題	thesis
終り	end
を導入（語順変更）	let
ただし	st
すると	then
その推論は	from
数学的帰納法	NAT_1:sch 2

Mizarの構文が素晴らしいのは、他の証明系とは違い、証明記述で使われる自然言語の分析に基づいていることです。最初に人工言語があり、それを自然言語に近づけようとゴチャゴチャ細工しているのとは訳が違います。人間側の言語使用、言語行為、論理的思考をなるべく忠実にコンピュータにシミュレートさせるように設計されています。

人間にフレンドリーな構文なんですよ。なのに、なのに、なのに、処理系はなんであんなにフレンドリーじゃないんだよ！ ギャップが凄いわ。凄すぎるわ。

ともかく、構文(は)最高よ。

*1:Mizarは人間が書いた証明を検証する処理系です。Mizar自身が証明できる命題を人間がご丁寧に証明したからといって文句は言いません。人間が書いた証明の正しさをチェックします。