記号論理学(3)

含意に対して割り切った姿勢をとって先へ進む。
証明論の推論規則にいわく「右含意」
\begin{equation}
\frac{A,\Gamma \vdash \Theta,B}{\Gamma \vdash \Theta, A \to B}
\end{equation}

というのがあるが、長らくここで心が折れて進めなかったが、やっと少し見えてきたのでメモを残したい。

推件式「$\Gamma \vdash \Theta$」(或は長～い矢印をもって $\Gamma \longrightarrow \Theta$)というやつは「$\Gamma$ を $A_1,A_2,\cdots,A_m $ 、 $\Theta$ を $B_1,B_2,\cdots,B_n$ とする時、$A_1 \land A_2 \land \cdots \land A_m $ なる仮定のもと $B_1 \lor B_2 \lor \cdots \lor B_n$ が成立する」ことを意味する記述である。

推論のシンプルなものは広義の三段論法である
\begin{equation}
\frac{A \vdash B \hspace{1em} B \vdash C}{A \vdash C}
\end{equation}

などがある。定理「$A \vdash B$」および定理「$B \vdash C$」が正しいならば、定理「$A \vdash C$」も正しい、という内容だ。【「Aという前提からBという結論が出てきて」かつ「Bという前提からCという結論が出てきる」ということが正しいのであれば、「Aという前提からCという結論が出てくる」という推論も正しい】と言える。

こういったことを証明するにあたって必要となる21の推論規則のうち冒頭の右含意
\begin{equation}
\frac{A,\Gamma \vdash \Theta,B}{\Gamma \vdash \Theta, A \to B}
\end{equation}

は何を言っているのか非常に分からない。自然言語で書いてみよう:【「$A$ および $\Gamma$ という前提から $\Theta$ と $B$ のうち少なくとも1つが結論として出てくる」ということが正しいのであれば「$\Gamma$ という前提から $\Theta$ と ``$A$ ならば $B$'' のうち少なくとも1つの結論が出てくる」こともまた正しい】という内容だ。これは脳みそが腐る。彌永・赤本では「これらが、すべて、推論の規則として、大多数の人々が正しいと認めるようなものであることは、容易に見てとれるであろう。」とあったが、大多数に含まれなかったので数年以上前に断念した。

しかし、含意を $P \to Q \iff \lnot P \lor Q$ として割り切れば、後は以下のような非常にゆるい解釈でぼちぼち納得できることが分かった:

背理法を使おう。ここでは背理法 ――― その裏にある排中律 ――― を無条件で正しいとする。

(1) $\Gamma \vdash \Theta, A \to B$ が正しくないとする。即ち、前提 $\Gamma$ のもと $\Theta$ も $A \to B$ も結論できないとする。更に後者を分解すると、 $\lnot A$ が結論できず、かつ $B$ が結論できないとなる。つまり 前提 $\Gamma$ のもと $\Theta,\ \lnot A,\ B$ のいずれも結論できないとなる。これを $\lnot (\Theta \lor \lnot A \lor B) = \lnot \Theta \land A \land \lnot B$ と書いてみよう。これが結論できると考える。
(2) さて、 $A,\Gamma \vdash \Theta,B$ は正しいとしていた。一方、手順(1)では前提として $\Gamma$ を置くことで、 $A$ を結論として得ていた。このことから、$\Gamma,A$ が成立すると考えられるので、 $\Theta \lor B$ が正しいことが導かれる。しかるに、同じく手順(1)では $\lnot \Theta \land \lnot B = \lnot (\Theta \lor B)$ が導かれていた。
(3) よって、$R = \Theta \lor B$ とすると、$R$ が正しいことが導かれると同時に $\lnot R$ が正しいことが導かれ、結局 $R \land \lnot R$ が正しいこと、即ち矛盾が導かれてしまう。
(4) このことから背理法によって、右含意の推論規則は正しいことが導かれる。

この証明が正しいとか厳密だとかは思わないが、「右含意」の意味するところのものが何かは以前よりは少しは見えた。但し、背理法を使っていて、排中律を使っているので、できれば直接法で示したい、理解したいところではある。