分からない理由6 定義や定理、補題、命題、証明がごちゃまぜになっている。 - Scala で TAPLを勉強しつつ LLVM コンパイラを作る日記

恥ずかしい話ですが、定義と定理の違いが良くわかってませんでした。

出来るだけ避けるべき存在になってました。

でも、Coqをやってみて考え方が変わりました。

定義とか定理とかは、typedefとかdefとかのようなキーワードであり、構造化された文章を書く為の構文の１つと捉えるといいようです。TAPLはドメイン特化言語を使って書かれていると考えると楽しいです。文法を定義してもいいんですけど、文法を見ても分かりずらくて、例が有るのが分かりやすいんですよね。

良書
　謝辞
　目次
　第1部ほげほげ
　3章ほげほげ
　　3.1 ほげ
　　ほげほげ
　　　定義3.1.1　ほげほげとする
　　　補題3.1.2 [ほげのほげげ]
　　　[証明]ほげほげはほげゆえにほげである。よってほげ。
　　　定理3.1.3 [ほげのほげほげ性]
　　　[証明]ほげほげはほげゆえにほげである。補題3.1.2によりほげなのでほげ。
　　　演習3.1.4 [推奨, ★★]ほげ
　　　演習3.1.5 [★]ほげ
　　　演習3.1.6 [★]ほげ

TAPLの場合、定義3.1.1とか補題3.1.2のような項目はまるでCoqで書いたプログラムのように見えます。

で、定義とか命題とか、仮定とかその辺が訳が分からないので分かったつもりになるとずいぶん、眠くならなくなりました。

定義	Definition	CoqではDefinitionは関数の定義、Inductiveは型の定義,Variableは変数の定義, Fixpointは再帰関数の定義
命題	Proposition	証明するための論理的問題
仮定	Hypothesis	真偽はともかくとして、何らかの現象や法則性を説明するのに役立つ命題
公理	Axiom	その他の命題を導きだすための前提として導入される最も基本的な前提のない仮定
定理	Theorem	公理を前提として演繹手続きによって導きだされる命題
補題	Lemma	定理を証明する為の証明されている命題
系	Corollary	(ある定理から直ちに導かれる定理)
事実	Fact	カエサルは殺された
注意	Remark
演習	Drill	学習するために行う計算。
ヒント	Hint	自動証明(auto)で使われる定理をヒントDBに登録する
慣習	Convention	同意、規定あるいは一般に受け入れられたしきたり、規範
例	example	実際に使った場合にどのようになるかを示したもの
解答	Result	演習の答え

定義は前提無しに決めたことです。定義は、命題だけではなくて、関数や型や値も決めることが出来ます。命題を定義した場合は、証明を行うことが出来ます。

命題は証明をすることを試みることが出来ますが、必ず証明できるわけではありません。型がProp(命題)な定義は命題です。命題を評価することは、証明することになります。（カリーハワード対応）

証明出来る命題を定理とか補題とか系等と言います。
公理は証明は出来ていないけど、自明な命題のことです。
公理は証明出来ると定理と呼べるが、２つの公理が同じ意味を表す場合は、どちらか一方の公理を使えば、もう一方の公理を証明出来る。また、公理を使って定義された定理を使って公理を証明することも出来るのです。

この辺を理解してしまえば、多分、TAPLは大分読み進めるはずです。