論理体系の解剖-1.4- 推論法則と論理式(2)

共通参考文献はこちら
前回の続き

推論の前提可換

　ここで証明列と推論法則について整理しましょう。証明列は例えば式Ｑa3の証明を示す次のようなものです。
式列1.4-1
　1) 式Ｐ1　前提(公理または仮定)
　2) 式Ｐ2　前提
　a1) 式Ｑa1　Ｐ1,Ｐ2,推論法則からの帰結
　3) 式Ｐ3　前提
　a2) 式Ｑa2　Ｑa1,Ｐ3,推論法則からの帰結
　a3) 式Ｑa3　Ｐ1,Ｑa2,推論法則からの帰結＝最終結論

　この証明列は３つの前提Ｐ1、Ｐ2、Ｐ3から結論Ｑa3が得られること、つまり次の推論法則が成立していることを示しています。
推論1.4-1　　Ｐ1、Ｐ2、Ｐ3 |--- Ｑa3

　一般には証明列により次の推論法則の成立を示すことになります。
推論1.4-2　　Ｐ1、Ｐ2、・・・、Ｐn |--- Ｑ

　ここで前提のＰ1、Ｐ2、・・・、Ｐnがどんな順序でも証明は成立するのですが、それは次のようにすると明確に示せます。先の例で示せば、「Ａ |--- Ａ」は明らかであることを利用して次のような証明列に書き直します。
式列1.4-2
　z1) 式Ｐ1　前提(公理または仮定)
　z2) 式Ｐ2　前提
　z3) 式Ｐ3　前提
　1) 式Ｐ1　　∵z1
　2) 式Ｐ2　　∵z2
　a1) 式Ｑa1　Ｐ1,Ｐ2,推論法則からの帰結
　3) 式Ｐ3　　∵z3
　a2) 式Ｑa2　Ｑa1,Ｐ3,推論法則からの帰結
　a3) 式Ｑa3　Ｐ1,Ｑa2,推論法則からの帰結＝最終結論

　ここでz1,z2,z3の順序をどのように入れ替えても証明列が成立することは明らかでしょう。ということで推論1.4-2は次の論理式に対応します。
式1.4-1　　(Ｐ1∧Ｐ2∧・・・∧Ｐn)→Ｑ

　また推論1.4-2は次の論理式にも対応するはずです。
式1.4-2　　(Ｐ1→(Ｐ2→(・・・→(Ｐn→Ｑ)・・・)))

　すると式1.4-2で最後の結論Ｑを除く式Ｐ1、Ｐ2、・・・、Ｐnの順序も入れ替え可能になります。論理記号「→」は前後の入れ替えができませんからこの事実はなんだか不思議に見えますが、最も単純な次の推論法則を証明すれば導くことができます。これは妥当推論法則3-5ですが、前提可換という呼び名は私が勝手に付けたものです。
推論1.4-3　　Ａ→(Ｂ→Ｃ) |--- Ｂ→(Ａ→Ｃ)

論理体系のモデル

　さて幾何学の公理系、群論の公理系、算術の公理系のような場合は公理や定理の真偽は幾何学、群論、算術といった具体的モデル世界の真偽に対応するように決められます。では述語論理や命題論理のような論理体系のモデルは何でしょうか。命題論理に限れば、それは命題の集合と考えられベン図(Venn diagram)で直観的にわかりやすく表すことができます。述語論理もわかりやすく示すのは難しいかも知れませんが、それでも述語命題の集合が論理体系のモデルだと考えてよいでしょう。


　そして推論法則そのものもモデルと考えることができます。すなわち、証明列に現れる論理式は命題を示すものだし、証明列内の式列同士の関係は命題論理記号(特に「→」)で示せるからです。またひとつの式列の中だけの話ではなく、「証明できる論理式が存在する」といった関係であれば述語論理記号で示すことができます。

　そうなると基本的な論理体系だけの話のときは、各論理式の意味と推論法則との整合性がないとまずいということになり、形式的でよいはずの論理式に推論法則の妥当性からの制限がかかる、というのか、論理式と推論法則とが入り混じって混乱しそうになる、ということになります。

　ここで前回紹介したゲンツェン流の体系を見てみますと、名称からわかるように２つの推論法則が対となって１つの論理記号の性質を規定しています。このことから厳密な証明はともかくとして、これらの推論法則がいずれも独立で、必要なものであることが納得できるのではないでしょうか？　そしてヒルベルト流では論理記号の数を少なくして、公理と推論法則の和を見かけ上はゲンツェン流より少なくしています。

　論理記号を少なくすると必要な数学的証明は少なくて済み、たぶん単純にもなります。これは、論理記号を増やした時に必要な証明を全て、論理記号の定義に繰り込んでいるとでも言えるでしょう。しかしその分、その証明を人間が理解するのが困難になります。∧や∨を→と￢だけで定義した式は、人間にとって自然に理解できるものではないからです。

　さて、このヒルベルト流の公理の選び方がどのように巧みなものかという話を次回にします。