証明論 (2): シーケント計算の導入、およびカット除去定理の紹介とそのありがたみ [証明論]

第2回目の授業のメモ。

やったこと。

• シーケント計算の導入
• そもそもシーケント計算って？
  「シーケント」と呼ばれるものから別のシーケントを導き出すこと。
• じゃあ、「シーケント」ってのは何？
  形式的には $\Gamma \rightarrow \Theta$ というかたちのものを言い、$\Gamma$ と $\Theta$ はそれぞれ「前件」「後件」と呼ばれる。（$\Gamma$ と $\Theta$ は任意有限個の論理式の集まりを表すとする。$\Gamma$ と $\Theta$ はそれぞれ空であってもかまわない）。
• その意味するところは？
  $\rightarrow$ を通常の含意「〜であれば…」であるととらえると、「$\Gamma$ 内の論理式がすべて真であれば $\Theta$ のいずれかの論理式が真である」と解釈できる。たとえば $\Gamma$ の各文（自由変数が現れない論理式を「文」と呼ぶ）が「明日は晴れである」「明日は仕事が休みである」であり、$\Theta$ の各文が「明日は遊園地に行く」「明日は映画を見に行く」であるとすると、シーケント $\Gamma \rightarrow \Theta$ は「明日、晴れていて、かつ仕事が休みであれば、遊園地に行くか、あるいは映画を見に行く」を意味すると考えられる。
• ということは、このシーケントは、「明日」と名指される日が晴れており、かつ仕事が休みにもかかわらず、遊園地にも行かず、かつ映画を見にも行かないとき、そのときにかぎって偽と見なされる、ってこと？
  そのとおり。
• 具体的なシーケント計算の例をあげてもらえる？
  それには、まず、各々の論理演算子について、それらを前件あるいは後件に導入するルールと、論理演算子が関係しない、シーケントのかたちを変えるルールを理解しなければならない。論理演算子が関係しないルールは、以下の7つ。
  
  $\large{\frac{\Gamma \rightarrow \Theta}{\mathfrak{D},\Gamma \rightarrow \Theta} \quad \frac{\Gamma \rightarrow \Theta}{\Gamma \rightarrow \Theta,\mathfrak{D}}}$（薄め）
  
  $\large{\frac{\mathfrak{D},\mathfrak{D},\Gamma \rightarrow \Theta}{\mathfrak{D},\Gamma \rightarrow \Theta} \quad \frac{\Gamma \rightarrow \Theta,\mathfrak{D},\mathfrak{D}}{\Gamma \rightarrow \Theta,\mathfrak{D}}}$（縮約）
  
  $\large{\frac{\Delta,\mathfrak{D},\mathfrak{E},\Gamma \rightarrow \Theta}{\Delta,\mathfrak{E},\mathfrak{D},\Gamma \rightarrow \Theta} \quad \frac{\Gamma \rightarrow \Theta,\mathfrak{E},\mathfrak{D},\Lambda}{\Gamma \rightarrow \Theta,\mathfrak{D},\mathfrak{E},\Lambda}}$（交換）
  
  $\large{\frac{\Gamma \rightarrow \Theta, \mathfrak{D} \quad \mathfrak{D}, \Delta \rightarrow \Lambda}{\Gamma, \Delta \rightarrow \Theta, \Lambda}}$（カット）
  
  論理演算子のルールは、長くなるのでとりあえず選言 $\vee$ と否定 $\neg$ についてのものだけあげる（他のルールは適宜あげることとする）。
  
  $\large{\frac{\mathfrak{A},\Gamma \rightarrow \Theta \quad \mathfrak{B},\Gamma \rightarrow \Theta}{\mathfrak{A}\vee\mathfrak{B},\Gamma \rightarrow \Theta}}$（$\vee$ を前件に導入）
  
  $\large{\frac{\Gamma \rightarrow \Theta,\mathfrak{A}}{\Gamma \rightarrow \Theta,\mathfrak{A}\vee\mathfrak{B}} \quad \frac{\Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\vee\mathfrak{B}}}$（$\vee$ を後件に導入）
  
  $\large{\frac{\Gamma \rightarrow \Theta,\mathfrak{A}}{\neg \mathfrak{A},\Gamma \rightarrow \Theta} \quad \frac{\mathfrak{A},\Gamma \rightarrow \Theta}{\Gamma \rightarrow \Theta, \neg \mathfrak{A}}}$（否定）
  
  上記ルールを用いて、排中律 $A \vee \neg A$ はつぎのように証明される。
  
  $\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{A \rightarrow A}{\qquad \quad \ \rightarrow A, \neg A}}{\qquad \qquad \qquad \rightarrow A, A \vee \neg A}}{\qquad \qquad \qquad \rightarrow A \vee \neg A, A}}{\qquad \qquad \qquad \qquad \ \rightarrow A \vee \neg A, A \vee \neg A}}{\qquad \qquad \ \rightarrow A \vee \neg A}$
  
  適用されているルールは上からそれぞれ、否定導入（後件）、$\vee$ 導入（後件）、交換（後件）、$\vee$ 導入（後件）、縮約（後件）となる。上の例で示されたとおり、計算は「始式」と呼ばれる $\mathfrak{A} \rightarrow \mathfrak{A}$ のかたちを持つ式（$\mathfrak{A}$ は任意の論理式とするが空ではないとする）から出発する。また、最後の式（「終式」と呼ばれる）が $\rightarrow \mathfrak{A}$ である場合、それは $\mathfrak{A}$ がトートロジーであることを示す。

• カット除去定理のありがたみとその証明方針
• まず、カット除去定理って何？
  「カットを用いてなされた証明はカットなしの証明に書き換えることができる」という定理を言う。たとえば、説明のため $A \supset B, B \supset C \rightarrow A \supset C$ というよく知られた定理（げんみつには、これは $\rightarrow ((A \supset B) \& (B \supset C)) \supset (A \supset C)$ と表されるべきだが、ちょっと無精をさせてもらう）をカットを用いて示す。まず、含意を表す論理演算子 $\supset$ のルールを導入する。
  
  $\large{\frac{\Gamma \rightarrow \Theta, \mathfrak{A} \quad \mathfrak{B}, \Delta \rightarrow \Lambda}{\mathfrak{A} \supset \mathfrak{B}, \Gamma, \Delta \rightarrow \Theta, \Lambda} \quad \frac{\mathfrak{A}, \Gamma \rightarrow \Theta, \mathfrak{B}}{\Gamma \rightarrow \Theta, \mathfrak{A} \supset \mathfrak{B}}}$
  
  上記ルールとカットを用い、$A \supset B, B \supset C \rightarrow A \supset C$ は以下のように証明される。
  
  $\cfrac{\cfrac{\cfrac{A \rightarrow A \quad B \rightarrow B}{A, A \supset B \rightarrow B} \quad \cfrac{B \rightarrow B \quad C \rightarrow C}{B, B \supset C \rightarrow C}}{A, A \supset B, B \supset C \rightarrow C}}{A \supset B, B \supset C \rightarrow A \supset C}$
  
  カット除去定理の言うところによれば、この導出はカットなしでも遂行可能ということになる。（カットなしの導出は読者の演習とする）
• ってことは、つまり「ルールのうちカットはいらないよ」ってだけのことでしょ？　それが何だってそんなに重要なの？
  たとえば、カットを用いると以下のように矛盾（前件も後件も空の $\rightarrow$ で表される）が導き出される可能性がある。
  
  $\cfrac{\cfrac{\vdots}{\rightarrow A} \quad \cfrac{\vdots}{A \rightarrow}}{\rightarrow}$
  
  カット除去定理によれば、もしカットを用いて $\rightarrow$ が導出できるのであればカットなしでもそれは導出できる、ということになる。しかし、シーケントを導き出すルールのうち、始式に含まれるパーツが完全に消失するのはカットだけである。言いかえれば、始式に含まれるパーツは何らかのかたちで終式にも現れなければならない。また、始式 $\mathfrak{A} \rightarrow \mathfrak{A}$ の $\mathfrak{A}$ が空であることは許されないということをあわせると、カットなしでは $\rightarrow$ はどうがんばっても導出され得ないということが分かる。つまり、この体系内では矛盾は導出され得ないということになって、これは重要な帰結である。