「チャットAIで形式証明も自然言語混じりで書ける（はず）」と「自然言語証明から形式証明を抽出できる（はず）」で述べたように、自然言語を使って形式証明が書けるようになるだろうと予測（むしろ期待）してます。しかし、自然言語であろうが形式言語であろうが、ものごとをハッキリと述べるための枠組みは必要です。この枠組みの記述には、当面は形式言語のほうが有利でしょう。
「自然言語ヒント／キュー前提の形式証明の書き方」への補足の形で、枠組みの記述法を述べます。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\par}{\Keyword{par } }
\newcommand{\case}{\Keyword{case } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\consider}{\Keyword{consider } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\achieved}{\Keyword{achieved } }
\newcommand{\aiming}{\Keyword{aiming } }
\newcommand{\fact}{\Keyword{fact } }
\newcommand{\postulate}{\Keyword{postulate } }
\newcommand{\providing}{\Keyword{providing } }
\newcommand{\backlog}{\Keyword{backlog } }
\newcommand{\proof}{\Keyword{proof } }
\newcommand{\qed}{\Keyword{qed } }
%
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\hyp}{ \text{-} }
\newcommand{\ent}{ \mathrel{\triangleright\!\!\longrightarrow} } % entails
`$
内容：
シリーズ・ハブ記事：
矢印問題
矢印記号の使用法はホントに悩みの種です。
一番問題なのは、論理の含意記号とステートメントの仮定と結論を区切る記号がオーバーロードされることです。ステートメント〈statement〉とは、論理のシーケント、型理論の型判断、圏論のプロファイルに相当する表現の、より親しみやすい呼び名です。ここでは、ステートメントの区切り記号に新しい矢印記号を割り当てることにします。以下の表の折衷案が今回採用する矢印記号です。
| $`\text{型理論}`$ | $`\text{論理}`$ | $`\text{圏論}`$ | $`\text{折衷案}`$ |
| $`\to`$ | $`\Rightarrow`$ | $`[\hyp, \hyp]`$ | $`\to, \Imp`$ |
| $`\vdash`$ | $`\to`$ | $`\to`$ | $`\ent`$ |
| $`\vdash`$ | $`\vdash`$ |
仮定〈文脈 | コンテキスト〉が $`\Gamma`$ で結論が $`P`$ であるステートメント〈シーケント | 判断〉は $`\Gamma \ent P`$ と書きます。$`\Gamma`$ は、次のいずれかをカンマで区切って並べたものです。
- $`x: X`$ のような変数の型宣言
- $`a: A`$ のようなラベル付きの命題
命題のラベルは、命題そのものの呼び名ではなくて、命題の証拠・証明に付けられた名前です。なので、混乱・誤解を避けたいときは命題の証拠ラベル〈witness label of proposition〉とも呼びます。
次はステートメントの例です。
$`\quad (x, y, a, b : {\bf R}), (x - a)(y -b) = 0 \ent x = a \lor y = b`$
これは略式の書き方で、複数の変数を一度に宣言し、命題の証拠ラベルを省略しています。次のように変形したものを正式だとします。命題のラベルは何でもいいので適当に付けました。
$`\quad (x : {\bf R}),(y : {\bf R}),( a : {\bf R}),(b : {\bf R}), (\text{_1} : (x - a)(y -b) = 0) \\
\qquad \ent x = a \lor y = b`$
依存カリー化
$`\Gamma \ent P`$ というステートメントがあるとき、矢印の左側に何もない形に変形できます。その手順は：
- $`x: X`$ のような変数の型宣言は、全称記号 $`\forall (x: X).`$ として右側に“移項”する。
- $`a: A`$ のようなラベル付き命題は、含意の前件として右側に“移項”する。ラベルは取り除いてよい（あっても害はない）。
前節の例を、ワンステップずつ変形してみましょう。
$`\quad (x : {\bf R}),(y : {\bf R}),( a : {\bf R}),(b : {\bf R}), ( \text{_1}: (x - a)(y -b) = 0) \\
\qquad \ent x = a \lor y = b\\
\:\\
\downarrow ( (x - a)(y -b) = 0) \text{ を含意の前件に}\\
\:\\
\quad (x : {\bf R}),(y : {\bf R}),( a : {\bf R}),(b : {\bf R}) \\
\qquad \ent (x - a)(y -b) = 0 \Imp x = a \lor y = b\\
\:\\
\downarrow (b : {\bf R}) \text{ を全称記号に}\\
\:\\
\quad (x : {\bf R}),(y : {\bf R}),( a : {\bf R}) \\
\qquad \ent \forall(b : {\bf R}). (x - a)(y -b) = 0 \Imp x = a \lor y = b\\
\:\\
\downarrow ( a : {\bf R}) \text{ を全称記号に}\\
\:\\
\quad (x : {\bf R}),(y : {\bf R}) \\
\qquad \ent \forall ( a : {\bf R}).\forall(b : {\bf R}). (x - a)(y -b) = 0 \Imp x = a \lor y = b\\
\:\\
\downarrow (y : {\bf R}) \text{ を全称記号に}\\
\:\\
\quad (x : {\bf R}) \\
\qquad \ent \forall (y : {\bf R}). \forall ( a : {\bf R}).\forall(b : {\bf R}). (x - a)(y -b) = 0 \Imp x = a \lor y = b\\
\:\\
\downarrow (x : {\bf R}) \text{ を全称記号に}\\
\:\\
\qquad \ent \forall (x : {\bf R}). \forall (y : {\bf R}). \forall ( a : {\bf R}).\forall(b : {\bf R}). (x - a)(y -b) = 0 \Imp x = a \lor y = b\\
`$
最後に得られたステートメントを略式に短く書けば：
$`\quad \ent \forall (x, y, a, b : {\bf R}). (x - a)(y -b) = 0 \Imp x = a \lor y = b`$
以上のような手順を依存カリー化〈dependent Currying〉と呼びます。
ステートメント $`\Gamma \ent P`$ に依存カリー化を可能な限り行って、矢印の左側が空になったときの右側の論理式〈命題〉を $`[\Gamma \ent P]`$ と書くことにします。
集合 $`A`$ へのポインティング写像 $`{\bf 1} \to A`$ と集合 $`A`$ の要素を同一視するのと同じ事情で、左側が空のステートメント $`\ent Q`$ の証明と、命題 $`Q`$ の証拠 $`w : Q`$ は同一視されます。具体的には、次の2つは適宜同一視されます。
- ステートメント $`\ent [\Gamma \ent P]`$ の証明
- 命題〈論理式〉 $`[\Gamma \ent P]`$ の証拠
証明済みのステートメントをコンテキストに格納するときは、証拠ラベル付き命題として格納します。
ブロックと目標・成果物
証明を記述するためのブロックには以下があります（「自然言語ヒント／キュー前提の形式証明の書き方」参照）。
- $`\proof /\: \qed`$ ： 一般的な証明記述ブロック
- $`\letsShow /\: \conclude`$ ： これも一般的な証明ブロック
- $`\par /\: \endBlock`$ ： 論理AND導入のためのブロック
- $`\case /\: \endBlock`$ ： 論理OR除去のためのブロック
- $`\assume /\: \endBlock`$ ： 含意と全称記号導入のためのブロック
- $`\consider /\: \endBlock`$ ： 存在記号除去のためのブロック
ブロックの直前には、そのブロックで示すべきステートメントを $`\aiming`$で書けるとします。ブロックの直後には、そのブロックで示せたステートメントを $`\achieved`$で書けるとします。例えば次のようです。
$`\aiming \ent \forall(x:X). P\\
\assume x : X\\
\quad \cdots\\
\endBlock\\
\achieved \ent \forall(x:X). P
`$
$`\aiming`$の連続、$`\achieved`$の連続を認めます。
$`\aiming (x: X) \ent P\\
\downarrow 依存カリー化\\
\aiming \ent \forall(x:X). P\\
\assume x : X\\
\quad \cdots\\
\endBlock\\
\achieved \ent \forall(x:X). P\\
\downarrow 依存反カリー化\\
\achieved (x:X) \ent P
`$
以下の2つの書き方は同じことです。
$`\letsShow \Gamma \ent P\\
\quad \cdots\\
\conclude \Gamma \ent P
`$
$`\aiming \Gamma \ent P\\
\proof\\
\quad \cdots\\
\qed\\
\achieved \Gamma \ent P
`$
適宜、目標の提示と達成した成果物の確認を書くと分かりやすくなります。
大域状態管理
証明の大域状態管理とは、“使えるモノ”と“目標”と“やり残し”を管理することです。管理対象は：
- 利用可能な資源としてのファクト
- 現時点の目標〈ゴール〉としてのステートメント
- 直近の成果物としてのステートメント
- 未履行の証明責務であるバックログのステートメント
現状の証明支援系でタクティク・インタープリタを使うと、局所的な証明状態〈局所的なゴール達〉は表示してくれます。しかし、それはとても狭い範囲で、大域的な状態の表示・検索・操作はサポートされてません。僕は、紙に絵を描いたりメモ書きしたりしてます。ほんとトホホな気分になりますわ。
証明をドキュメントとみなしても、ゲームとしてみなしても、いずれにしてもストーリーがあり、そのストーリーのある時点／ある場所における状態があります。現在の時点／地点における状態を把握することは、証明を書く／する場合でも、読む／見る場合でも大事です。なのに、証明ソフトウェアはほぼ何もしてくれません。
目標の提示と成果物の確認は前節の $`\aiming`$と $`\achieved`$で記述できるので、その他の状態／管理対象について述べます。
現在点〈カレント・ポイント〉の大域状態は、通常（日常で）は暗黙的で不確定だし、確定する必要もありません。しかし証明ソフトウェアでは、「どのライブラリ／パッケージ／モジュールの何という名前の定理／公理」というような明示的な形で大域状態の構成要素を特定しなくてはなりません。自然言語記述が使えるようになると、「いつもの基本定理」「よく知られた例の公理」「先ほど示した結果」「中学生でも知っている簡単な計算」のような言い回しで利用可能な定理／公理を指示できるようになるかも知れません。
参照方法はともかくとして、利用してよい定理／公理の確認のために $`\fact`$ を使いましょう。“ファクト”は証明されている定理または公理のステートメントのことです。例えば：
$`\fact \text{w1} : (x, y : {\bf R}), x y = 0 \ent x = 0\land y = 0`$
$`\text{w1}`$ はファクトのラベルですが、ステートメントの呼び名ではなくて証明の呼び名です。カリー化した命題の形で書くと：
$`\fact \text{w2} : \forall(x, y : {\bf R}). x y = 0 \Imp x = 0\land y = 0`$
$`\text{w2}`$ は命題の証拠ラベルです。
バックログは幾つかのタイミングで発生します。$`\postulate`$で証明してない仮定を導入すると、それはバックログ（履行してない証明責務）になります。$`\postulate`$は公理ではなく、いずれは証明するつもりがあるときに使います（そう約束します）。例えば：
$`\postulate \text{b1} : (n, m, k : {\bf N}), n \le m \ent nk \le mk`$
ステートメントを依存カリー化した単一の命題の形で書けば：
$`\postulate \text{b2} : \forall (n, m, k : {\bf N}). n \le m \Imp nk \le mk`$
$`\backlog`$ で証明を中断すると、そこから先の証明（書いてない部分）がバックログになります。Idrisでは、この種のバックログを“ホール”と呼び、処理系がある程度管理してくれます。Lean 4には、そのような機能はありません。
バックログを仮定している定理をファクトとして宣言したいときは次の形にします。
$`\fact \text{w3} : \forall (n, m, a, b : {\bf N}). n \le m \land a \le b \Imp na \le mb\\
\quad \providing \text{b2} : \forall (n, m, k : {\bf N}). n \le m \Imp nk \le mk`$
証明のバックログの管理には、ToDo管理／タスク管理／イシュー管理のソフトウェアのような機能／UIが必要になるでしょう。コードエディタ＋タクティク・インタープリタではまったく不十分です。
ソフトウェアにやって欲しいこと
「証明支援系がダメだった理由と、AIでブーストする理由」で、「期待が持てるようになったから不満と願望を言う気になる」と書きました。以下に不満と願望を書くのも実現できるだろうと期待するからです。現状、証明記述に付随するつまらなくて手間がかかる作業は、何とかして欲しい。
大域的証明状態の把握はほんとに難しいです。モジュールをインポートしても、そのなかにどのくらいのファクト（定理や公理）があるかよく分からないし、目的のファクトが実際にはなかったりもします。$`\fact`$宣言を書いたら、それが現在の環境内に在るか無いか、無いならどのモジュール／パッケージ／ライブラリをインポートすればいいか、といったアドバイスは欲しい。もちろん、ファクトを形式記述しなくて自然言語で曖昧に書いても、確認や検索をして欲しいですよね。
ライブラリ内のファクトや自分が書いた定理の論理的依存関係のグラフィカルな表示は必須だと思うのだけど、証明ソフトウェアには付属してませんね。なんで？ バックログは色を変えて表示も是非欲しい。
そもそもバックログの生成や管理の機能も（Idrisのホールくらいしか）無い。証明の難しい箇所や、逆にすぐ出来そうな所は後回しにするのはよくやることなのに、sorryで謝ることしかできないし、後で文字列"sorry"をgrep検索するというね、石器時代のやり方。
練習問題の設問にsorryを使っている例を見かけますが、質問・応答のフォーマットは欲しいところ。内部的なメカニズムは、バックログ（質問）とその解消（応答）でいいと思います。
対話的証明支援系と銘打ちながらも、実際にはたいして対話的でもないし、たいして支援もしてくれなかったのですが、今後は看板通りの機能性を備えてくれると（何度も繰り返しますが）期待してます。
