目次

本書における命題、定理、補題、言明について

• 命題とは： 論理的に真か偽かが定まる主張
• 定理とは： 命題の内、真であるもの
• 補題とは： 定理の別名
• 言明とは： 命題の主張を表す文章や記号の列

形式化とは

私たちが普段使うような文章（言明）を、定理証明支援器（支援系）向けに変換すること。

Coqは、これらの言明の正しさをチェックする定理証明支援器の1つ。

どのように支援器は正しさを保証するか

定理証明支援器の根幹をなす、数学基礎論によって保証する。
これは定理証明支援器が数学基礎論を機械化（ソフトウェア化）したものであることから。

Coqは 型理論 と呼ばれる基礎論に基づいて実装されている。

型理論の基礎

型理論は、その名の通り 型 という概念が根幹をなしている。

a : A

と書くと 「型Aの要素a」 という意味を表す。
これは集合でいうところの「集合Aのaという要素」と全く同じ意味である。

論理演算

形式論理 での論理和

A \/ B

を

A + B

と表す型に対応させる。A + Bは「AまたはBの型（の要素）で構成される型」という意味。

なお、A + B と B + A は別の型を意味する。

形式論理 での論理積

A /\ B

は、型理論では、∑x: A, B を表す型に対応させる。これは、順序対(a,b)を要素に持つ型を意味する。

形式論理での含意

A --> B

は 型理論の Πx: A, B を表す型に対応させる。これは、関数 f: A --> B に相当する要素によって構成される型、すなわち A型からB型への写像を持つ関数という捉え方ができる。

最後に

なぜかMathJaxが動かない・・・
きれいな数式が書けない！！！書きたい！！！