公理は証明のできない仮定とか前提だとよく言われる。しかし、現代の証明概念では公理も証明できるとされる。なぜかというと、理論θにおける証明は、θ の言語の文から成る列であり、その列のひとつひとつが、
- θ の公理であるか
- その列において先立つ文から、θ の推論規則の適用によって得られる文である
という風に定義されるから*1。
この話を最初に読んだとき、「そりゃそうだね」って思ったのだけど、その時は伝統論理において証明とか演繹がどう定義されてるのか考えてなかった。それで『ケンブリッジ・コンパニオン』を少し調べてみたら、どうもアリストテレス『分析論前書』の三段論法の定義だと、前提と結論は全く別の形をした命題でなければならないらしい。なるほど、たしかに、これだと公理に含まれている命題は証明できないわな。
