「チャットAIで形式証明も自然言語混じりで書ける(はず)」と「自然言語証明から形式証明を抽出できる(はず)」において、形式証明と自然言語証明はかなりの程度相互翻訳可能になるはず、という予測(というか期待・願い)を述べたのですが、自然言語ヒント/キューが使える前提での形式証明のフォーマットを提案しておきます。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\have}{\Keyword{have } }
\newcommand{\need}{\Keyword{need } }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\theorem}{\Keyword{theorem } }
\newcommand{\proof}{\Keyword{proof } }
\newcommand{\qed}{\Keyword{qed } }
\newcommand{\for}{\Keyword{for } }
\newcommand{\par}{\Keyword{par } }
\newcommand{\case}{\Keyword{case } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\achieved}{\Keyword{achieved } }
\newcommand{\consider}{\Keyword{consider } }
\newcommand{\st}{\Keyword{ st } }
\newcommand{\next}{\Keyword{next } }
\newcommand{\postulate}{\Keyword{postulate } }
\newcommand{\backlog}{\Keyword{backlog } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\Imp}{ \Rightarrow }`$
内容:
シリーズ・ハブ記事:
はじめに
「ヤシコフスキ/カリシュ/モンタギュー形式の証明: 人間可読・将来的機械可読」で触れた、人間可読・将来的機械可読な証明フォーマットをより詳しく説明します。
「自然言語証明から形式証明を抽出できる(はず)」で述べたように、将来的には自然言語で書いても形式証明に変換できるようになると思います。しかし、それは十分に明確な自然言語で書いた場合です。明確な書き方に慣れるには、まずは人工言語〈形式言語〉で書いてみるのがよいと思います。以下に提案するキーワード/構文は、ダイクストラとヤシコフスキ/カリシュ/モンタギューのアイディアをベースに、Mizar、Isabelle/Isar、ラムダ項の各種シンタックスシュガーなどを参考にしたものです。
使用するキーワード
この記事で説明するキーワードを出現順に列挙します。
- $`\have`$
- $`\need`$
- $`\letsShow/\: \conclude`$
- $`\theorem/\: \proof /\: \qed`$
- $`\par/\:\endBlock`$
- $`\case/\:\endBlock`$
- $`\assume /\: \endBlock`$
- $`\achieved`$
- $`\consider /\: \endBlock`$
- $`\next`$
- $`\for`$
- $`\postulate`$
- $`\backlog`$
命題の提示
命題(を表す論理式)は、$`\have`$または $`\need`$を前置して提示します。ただし、$`\have\need`$が文脈から明らかなら省略可能です。
- $`\have A`$ -- 命題 $`A`$ は、この時点で証明済みの命題であることを示す。
- $`\need A`$ -- 命題 $`A`$ は、これから証明すべきターゲット命題であることを示す。
自然言語によるヒント/キューは次の形です。
- $`\downarrow \text{自然言語ヒント/キュー}`$ -- 次〈下〉の行の命題が成立する根拠を書く。
- $`\uparrow \text{自然言語ヒント/キュー}`$ -- 次〈下〉の行の命題が成立すると仮定すれば、前〈上〉の行の命題が成立する根拠を書く。
上から下への例:
$`\have A\\
\have A\Imp B\\
\downarrow \text{モーダスポネンス}\\
\have B
`$
下から上への例:
$`\need A\land B\\
\uparrow \text{論理ANDの導入規則から}\\
\need A, \, B
`$
この例では、日本語の文が下から上への推論について書いてあります。矢印で方向が明確なので、上から下への操作を書いてもかまいません。また、論理式をカンマで区切って横に並べる代わりに縦に並べても同じです。
$`\need A\land B\\
\uparrow \text{論理ANDを分解する}\\
\need A\\
\need B
`$
下から上(バックワード)の推論で、下の行に何もないときは、誤解がないように $`\Box`$ を置きます。
$`\need A\\
\uparrow \text{仮定にある}\\
\Box
`$
矢印の上下から、証明済み命題かターゲット命題かは分かるので、$`\have\need`$は次のように省略できます。
$`A\\
A\Imp B\\
\downarrow \text{モーダスポネンス}\\
B
`$
$`A\land B\\
\uparrow \text{論理ANDの導入規則から}\\
A, \, B
`$
$`A\\
\uparrow \text{仮定にある}\\
\Box
`$
証明全体
証明全体は $`\letsShow /\: \conclude`$ブロックにします。以下で、$`\Gamma`$ はコンテキストを表します。コンテキストとは、型宣言 $`x: X`$ や命題宣言 $`a:A`$ を並べたものです。矢印 $`\to`$ は含意ではなくて、ステートメント〈シーケント〉の仮定と結論を区切る記号です(「矢印の混乱に対処する: デカルト閉圏のための記法」参照)。
- $`\letsShow \Gamma \to A`$ -- $`\Gamma`$ を仮定して、$`A`$ を結論とする証明を開始する。
- $`\conclude`$ -- 証明の終わり。念のためにステートメントを再掲してもよい。
証明の戦略〈strategy〉や、全体的な構造・流れに関するヒント/キューは黒丸に続けて書きます。
$`\letsShow \Gamma \to A\\
\bullet \text{背理法を使う}\\
\letsShow \Gamma, b: \lnot A \to \bot\\
\quad \cdots\\
\quad \cdots\\
\conclude \Gamma, b: \lnot A \to \bot\\
\conclude \Gamma \to A
`$
$`b`$ は命題 $`\lnot A`$ のラベル(命題成立の根拠、証拠に付けられた名前)です。明示的に参照する必要がないならラベルを付けなくてもかまいません。
仮定をすべて明示しなくてもかまいません。注目している仮定命題だけでもOKです。
$`\letsShow \to A\\
\bullet \text{背理法を使う}\\
\letsShow b :\lnot A \to \bot\\
\quad \cdots\\
\quad \cdots\\
\conclude b : \lnot A \to \bot\\
\conclude \to A
`$
証明に名前を付けたいときは次の形式を使います。
$`\letsShow t : \Gamma \to A\\
\quad \cdots\\
\quad \cdots\\
\conclude
`$
次のように書いても同じです。
$`\theorem t : \Gamma \to A\\
\proof\\
\quad \cdots\\
\quad \cdots\\
\qed
`$
2つ以上の証明をまとめるグルーピング
2つ以上の証明をまとめるには、$`\par`$ブロックと $`\case`$ブロックを使います。$`\par`$ブロックは連言〈論理AND〉の導入に、$`\case`$ブロックは選言〈論理OR〉の除去に使います。「導入」「除去」は論理特有の言い回しで、「連言の導入」とは連言命題をターゲットにした推論(「推論」と「証明」は同義)、「選言の除去」は連言命題からスタートする推論のことです。
$`\par`$(parallel)の使用例を挙げます。
$`\need A\land B\\
\uparrow \text{論理ANDを分解する}\\
\need A,\, B\\
\bullet \text{それぞれを以下で証明する}\\
\par\\
\quad \letsShow \to A\\
\qquad \cdots\\
\quad \conclude\\
\quad \letsShow \to B\\
\qquad \cdots\\
\quad \conclude\\
\endBlock
`$
次は $`\case`$の使用例。
$`\letsShow A\lor B \to C\\
\bullet \text{場合に分けて証明する}\\
\case\\
\quad \letsShow A \to C\\
\qquad \cdots\\
\quad \conclude\\
\quad \letsShow B \to C\\
\qquad \cdots\\
\quad \conclude\\
\endBlock\\
\conclude A\lor B \to C
`$
ローカルな仮定ありの証明
証明全体の仮定(ステートメントの仮定)以外に、その場でローカルな仮定を設定して証明を行う場合は $`\assume`$ブロックを使います。ローカルな仮定には、型を明示した変数と命題のラベル(より正確には証拠のラベル)があります。
例を挙げます。
$`\assume x : X\\
\quad \cdots\\
\quad \have A\\
\endBlock
`$
型付き変数の宣言 $`x:X`$ はブロック内だけで有効で、ブロックの外では無意味です。
上の $`\assume`$ブロックは、全称命題の証明になっているのですが、そのことを次のように書きます。
$`\assume x : X\\
\quad \cdots\\
\quad \have A\\
\endBlock\\
\achieved \Gamma \to \forall x:X. A
`$
キーワード $`\achieved`$は、直前のブロックの成果物をステートメント〈シーケント〉として書きます。これは現状確認なのでなくてもかまいませんが、$`\achieved`$を挿入すると読みやすくなります。
命題(の証拠)をローカルな仮定にする場合は次のようです。
$`\assume a : A\\
\quad \cdots\\
\quad \have B\\
\endBlock\\
\achieved \Gamma \to A \Imp B
`$
コンテキスト $`\Gamma`$ にすべての前提・仮定を書く必要はありません。$`\Gamma`$ が空でもかまいません。コンテキスト(矢印の左)が空でも、何の仮定も無いということではなくて、暗黙の仮定はあります。
条件付き変数を処理するブロック
$`\consider`$ブロックは、条件付きの変数を導入します。ブロック内では、条件を仮定して推論します。$`\assume`$との違いは、存在命題の除去(存在命題からの推論)を目的にしているので、ブロック内の結論には導入された変数が含まれないようにします。$`\st`$は such that です。
$`\consider x:X \st A\\
\quad \cdots\\
\quad \have B\\
\endBlock\\
\achieved \Gamma, \exists x:X. A \to B
`$
もっと具体的な使用例は「チャットAIで形式証明も自然言語混じりで書ける(はず)」にあります。
その他
$`\for`$は、型付きの自由変数を導入します。$`\for`$で宣言された変数は、ブロックの終了まで使えます。(ブロック内ではない)トップレベルで $`\for`$が出現したら、宣言された変数はトップレベル・スコープ全体で有効です。
$`\next`$は、ブロック内を複数のパートに区切る区切り記号です。日本語の「さて」「次は」「それはそうと」のような繋ぎの言葉だと思ってください。
$`\postulate`$は、命題(の証拠ラベル)を宣言します。$`\for`$の命題版です。$`\postulate`$で仮定された命題は証明が付いてないので暫定的なものです。$`\backlog`$も $`\postulate`$と同じく暫定的な命題を宣言します。$`\backlog`$ はそこで証明を打ち切る意図が含まれます。
$`\need A\land B\\
\uparrow \text{論理ANDを分解する}\\
\need A,\, B\\
\bullet \text{それぞれを以下で証明する}\\
\par\\
\quad \letsShow \to A\\
\qquad \cdots\\
\quad \conclude\\
\quad \letsShow \to B\\
\qquad \backlog b: B \text{ // 今は証明しない}\\
\quad \conclude\\
\endBlock
`$
$`\postulate`$、$`\backlog`$で宣言された命題は、後で証明を付けるなり公理扱いするなりします。いずれにしても、判断は後回し/先延ばしになります。