Globular探り 10：定理と証明

定理と証明の関係がよく分からなかったが、そもそもが曖昧だった。ハッキリさせる。

定理に関連して3つの概念を導入する。

1. あるnに対するn-セル（n-ダイアグラム）を命題と呼ぶ。
2. A, Bを命題として、s:(n + 1) A→B という(n + 1)-セルをステートメントと呼ぶ。
3. 別な p:(n + 1) A→B を証明ダイアグラムと呼ぶ。
4. T:(n + 2) s→p という(n + 2)-セルをリンクと呼ぶ。

現状の用語法では、

• ステートメントを「定理」と呼ぶことがある。
• リンクを「定理」と呼ぶことがある。
• 証明ダイアグラムを「証明」と呼ぶことがある。
• リンクを「証明」と呼ぶことがある。

したがって、

• 定理：ステートメントかリンクか曖昧
• 証明：証明ダイアグラムかリンクか曖昧
• リンクは、「定理」と呼ぶこともあり、「証明」と呼ぶこともある。

次の使い方が良さそう。

• ステートメントを「定理」と呼んでもよい。
• リンクを「証明」と呼んでもよい。
• 証明ダイアグラムを「証明」と呼んでもよい。

しかしこれでも、違う次元のモノを同じ「証明」で呼んでいることになる。証明ダイアグラムを証拠とでも呼んで、「証明（リンク）はステートメントと証拠を結ぶ1次元高いセル」とするのが一番妥当だろう。