数学書を読むのに一番苦労するのは証明をどう理解するかということである。体系的に積み上げて書かれているので、ひとつでも理解できない証明があると全く先へ進むことができない。その場合書かれている個々の文そのものが理解できなければどうしようもないが、個々の文の意味は分かるのに、その論理の運びかたが分からないために理解できないと感じることも多い。
一口に論理的推論といっても単純な三段論法だけでなく、背理法や、様々の仮定を付加した議論など様々な形態がありその論理的道筋をきちんと追っていくのはなかなか大変である。ところが、命題論理の公理系について勉強していたところ、論理的な推論は簡単な方法で定式化できることに気づいた。
命題論理学の公理系では、少数の公理から三段論法(前件肯定)を用いて証明できるものが定理となる。たとえばウカシェビッチ(Lukasziewic)の公理系では公理は次の3つである。
P1. A→(B→A) P2. (A→(B→C))→((A→B)→(A→C)) P3. (¬B→¬A)→(A→B)
また、命題論理の定理は次のように定義される。
(1) 公理 P1、P2、P3 は定理である
(2) A と A→B が定理なら、Bも定理である。(三段論法)
さらに、定理 An の証明は次のような条件を満たす命題 A0, A1, ... , An の命題の列である。すなわち、各 k <= n について、
(1) Ak は公理(P1, P2, P3)であるか、
(2) i,j < k が存在して Aj は Ai → Ak である。(Ak は、Ai と Aj から三段論法によって導かれる。)
例として次の命題の列 Ao, A1, A2, A3, A4 は、A→A の証明である。
A0 = A → ((A → A) → A) : P1 A1 = (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) : P2 A2 = (A → (A → A)) → (A → A) : A1 = A0 → A2 A3 = A → (A → A) : P1 A4 = A → A : A2 = A3 → A4
定理 A → A の証明を考え出すのは大変であるが、上の命題の列が A → A の証明であることを確かめるのは難しくはない。一番上の命題から始めてその命題が公理であるか、または、上流の命題からの三段論法の帰結であるかを確かめれば良いだけだからである。したがって、推論の理解は機械的になる。さらに、この際の推論のチェックは構文論的に行われるため、命題の意味を考慮に入れる必要がないのである。この証明の流れの単純さは次のような一般的な証明の記述と比較するとよくわかる。
ここで、どんな「定理も」必ず「証明」をもつことを示しておこう。「証明」をもつ命題全体は、全ての公理を含み、三段論法に関して閉じている。「定理」全体の集合は、そのような性質を持つ最小の集合として定義されるのだから、「証明を」もつ命題全体の集合の部分集合になる。つまり、どんな「定理」も「証明」をもつ。逆に「証明」を持つ命題が「定理」になることは明らかである。(田中一之編・著「数学基礎論講義」日本評論社)
そこで上の例を次のような命題の列に変えてみよう。つまり、一行に1つの命題を書き、その命題は公理や定理や、上流の命題からの三段論法の帰結となるようにするのである。
推論1
A1=証明をもつ命題の集合は全ての公理を含む(公理だけの命題は証明であるから)
A2=証明をもつ命題の集合の要素に三段論法を適用しても帰結となる命題はその集合に属している(ある命題と別の命題から三段論法で帰結となる命題を作っても帰結は証明を持つ命題となるから)
A3=定理の集合は全ての公理を含む(公理は定理であるから)
A4=定理の集合は三段論法に関して閉じている(公理や定理から三段論法で演繹された命題はやはり定理であるから)
A5=ある集合の全ての要素が別の集合の要素でもあるならその集合はその別の集合の部分集合である(部分集合の公理)
A6=定理の集合は証明を持つ命題の集合の部分集合である
A7=どんな定理も証明を持つ
推論2
B1=証明をもつ命題は定理である。(定義)
結論
A7 と B1 より、
C1=命題が証明を持つことと、命題が定理であることは同値である
これが元の文より本当に分かりやすいかどうかは分からないが、少なくとも論理の流れは上から下に一方向に流れていっている。また、その推論の妥当性のチェックは三段論法に適合しているかどうかだけなので極めて簡単である。このように、命題論理の公理系における証明の表現法が一般的な議論を整理するのにも役に立つと言うのは面白い。