現在、論理学での「証明」のやり方としてしばしば採用されるものとしては、「タブロー」の他に、ゲンツェンが考案した「自然演繹」と呼ばれる方法がある。そして自然演繹の方法は、かつての「公理的方法」などに比べれば、はるかに習得が容易であるしー公理的方法では、簡単な論理式を証明するのも、ほとんど「職人芸」であった！ーまた、「論理語の意味とは何か」といった問題や、通常の体型とは異なる論理体系を考えたりする上では、極めて有用なものである*1。
ヒルベルトスタイルの証明は確かにどうしようもなく不便だが、「職人芸」というほどだろうか…などと思っていた時期が私にもあった。コンビネータでいうK, Sに対応する公理型があれば、演繹定理をわりあい容易に証明できるため、仮定による証明ができてしまう。だから、コツを掴めばそれほど難しくない、などとナメていたのだ。
しかし、公理系によっては、上の引用にもあるように、簡単な論理式を証明するのもほとんど職人芸になってしまう。例えば、カルナップ「論理学と数学の基礎」にある公理系を見てみよう*2。
- wenn ... so [wenn nicht ..., so ---]
- wenn [wenn nicht ..., so ...], so ...
- wenn [wenn ..., so ---], so [wenn [wenn ---, so .-.-], so [wenn ..., so .-.-]]
ドイツ語で書かれているので、もう少し分かりやすい記号で表すと
- p → (not-p → q)
- (not-p → p) → p
- (p → q) → [(q → r) → (p → r)]
のようになると思う。なお、推論規則はmodus ponensのみである。この公理系の嫌なところは、条件文のみのトートロジー（例えば、K）を証明するにも否定のついた公理を使わなければならないところにある。証明はうんざりするほどトリッキーなものとなる。
あるいは、戸田山和久『論理学をつくる』で紹介されている、一つしか公理をもたないメレディスの公理系：
- ( ( (A → B) → (¬C → ¬D) ) → C → E) → ( (E → A) → (D → A) )
この公理系の証明も、（試してはいないが）ものすごくトリッキーなものとなるだろう。
*1:丹治『タブローの方法による論理学入門』p. i-ii
*2:カルナップ『論理学の形式化』所収, p. 189あたり。List of Hilbert systems - Wikipediaによると、ウカシェーヴィチに由来する公理系のようだ。
