このシリーズのひとつ前の記事「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論法則として使う」において、証明可能性判断と推論規則を同義語のように使ったのですが、これはミスリーディングかも、と思うので補足します。
内容:
メタな立場と証明可能性判断
証明を実行する主体であるあなた、あなたが行う証明行為、そのときのあなたの頭の中などを外から観察している超越的存在がいるとします。手っ取り早いのは、超越的存在として神様を想定することです(「論理を身に付けるには」参照)。
上記のような、証明行為を外から眺める超越者は、メタなヤツと言えます。メタなヤツによる観察や主張はメタな立場からなされます。そういうメタな立場からの発言として証明可能性判断(provability judgement)があります。
- P1, ..., Pn |- Q
メタな立場から、行為主体(コイツと呼ぶ)の証明行為を眺めて、「コイツは確かに、P1, ..., Pn からQを証明しているぞ」と発言している、あるいは保証しているのが証明可能性判断です。
我々人間は、証明可能性判断を発言できるメタな立場に立つことができるでしょうか。ある状況では、ハッキリとメタな立場に立てます。あなたが、証明を実行するソフトウェアの実装者であり利用者でもあるとします。あなたは、証明を実行するソフトウェアの挙動を外から観察できるし、その動作のメカニズムも理解しているでしょう。そして次のような発言ができます。
- 「このソフトウェアは確かに、P1, ..., Pn からQを証明しているぞ」
生きている人間であれ、ソフトウェアであれ、抽象的・概念的な仕掛けであれ、証明を行うようなシステムは演繹系(deductive system; 証明系、論理系、推論系)と呼びます。証明可能性判断は、演繹系を外から眺めて記述するときの命題(メタな立場の命題なのでメタ命題)です。
演繹系の性質は、結局はメタ命題=証明可能性判断により記述されるので、もとの演繹系の研究が、証明可能性判断の体系の研究に移ってしまうことになります。対象物である演繹系と、外側にある証明可能性判断の体系を一緒に扱うべきだ、といった話になります。
今言ったことは、数理論理学や形式的体系の方法論というだけではなくて、普通の非形式的(半形式的)証明の場合にも適用されるのです。我々は、ほとんど無意識にメタな立場を使っています。証明ソフトウェアに対してメタな立場に立つだけでなくて、自分自身に対してもメタな立場に立つことがあるのです。このシリーズで話題にしている“証明のお膳立て”も、メタな立場からの発想だと言っていいでしょう。「自分自身に対してもメタな立場に立つ」現象の不思議さに付いては次の記事で述べています。
推論規則と証明可能性判断
「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論規則として使う」では、推論規則と証明可能性判断を同じ形で書きました。同じ形で書いて差し支えないですが、厳密には、推論規則と証明可能性判断は別物です。
推論規則とは、その名のとおり、どのような推論が可能かを書き下したものです。例えば、命題Pが証明済み、命題Qも証明済みのとき、連言命題P∧Qを導いてかまいません。これは次のように書けます。
証明済みの命題 P Q -----------------------------[推論のステップ] 推論で導出された命題 P∧Q
縦の図式を横1行で書けば、
- P, Q |- P∧Q
これは証明可能性判断と同じです。
推論規則と証明可能性判断が違う点は、推論規則が演繹系の内部にあり、証明可能性判断は演繹系の外にあることです。
今我々はメタな立場ではなくて、地面を這いつくばってひたすら証明作業に従事しているとします。そのときでも、推論規則は見えています。見えてないと作業ができないので、推論規則は地面にあるのです。それに対して、我々を上空から(文字通り上から目線で)観察している超越者の発言(つぶやきやナイショ話かも知れない)を、地上の我々は知ることができません。
仮定の命題を推論規則に変換して使う
論理学では通常、証明の最中に演繹系を変化させることはしません。しかし、我々が実際に行う証明行為(リーズニング)では、必要なら推論規則を足していくことは普通です。そのことを「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論規則として使う」で述べたかったのです。
混同と混乱を避けるために、推論規則を横書きにしたものは、次の形で書くことにします。
- Γ/ Δ |-! P
ビックリマークを付けています。'|-?'と'|-!'だとバランスがいいかな、と思って。
推論規則はビックリマーク付きで書く、という約束で「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」で述べたお膳立てを書き直しましょう。
Γ/ ∀x∈X.(P(x)⇒Q(x)), Δ |-? R ---------------------------------------------[前提を推論規則に] Γ/ Δ |-? R Γ/ (x : X), P(x) |-! Q(x)
右下の Γ/ (x : X), P(x) |-! Q(x) は推論規則なので、次のように解釈します。
- Γは文脈(予備知識、背景知識)。
- (x : X) と P(x) は既に証明済みで、得られている。
- この状況で、推論の1ステップの結果として、Q(x)を結論してよい。Q(x)は証明済みとなる。
これは超越者が上空(メタな立場)で言っていることではなくて、地上の作業者が利用してよい手順です。
「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」で出した具体例を再掲すると; 証明要求は次です。
- Γ/ ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T), (x : X), x∈S, ¬(x∈W) |-? x∈T
前提に、命題 ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) が含まれます。これを推論規則に直すと:
- Γ/ (x : X), x∈S, ¬(x∈W) |-! x∈T
したがって、もとの証明要求は、新しい証明要求と新しい推論規則に分解されます。
- 新しい証明要求 : もとの証明要求の前提から ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) を除いた*1証明要求
- 新しい推論規則 : ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) を推論規則に直したもの
具体的には、
- Γ/ (x : X), x∈S, ¬(x∈W) |-? x∈T
- Γ/ (x : X), x∈S, ¬(x∈W) |-! x∈T
要求のほうが「… を(可能なら)証明せよ」であるのに対して、推論規則が「… は1ステップ推論で証明済みとしてよい」と保証しているので、実質的な作業は何もしなくても、「証明できました」と納品(「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル』参照)できます。