Coq/SSReflect/MathComp による定理証明を読んで(1)本書における命題、定理、補題、言明について 命題とは： 論理的に真か偽かが定まる主張 定理とは： 命題の内、真であるもの 補題とは： 定理の別名 言明とは： 命題の主張を表す文章や記号の列 形式化とは 私たちが普段使うような文章（言明）を、定理証明支援器（支援系）向けに変換すること。 Coqは、これらの言明の正しさをチェックする定理証明支援器の1つ。 どのように支援器は正しさを保証するか 定理証明支援器の根幹をなす、数学基礎論によって保証する。 これは定理証明支援器が数学基礎論を機械化（ソフトウェア化）したものであることから。 Coqは 型理論 と呼ばれる基礎論に基づいて実装されている。 型理論の基礎 型理論は、その名の通り 型 という概念が根幹をなしている。 a : A と書くと 「型Aの要素a」 という意味を表す。 これは集合でいうところの「集合Aのaという要素」と全く同じ意味である。
