| 第二部 信仰と理性論 | 星加弘文 |
Chapter 2 信仰と理性の多対多関係 (13)
Hard study 5-2-4 「証明表」
しかし、疑問はさらに増えている。意味論のどこに拒否が仕込まれているのだろうか。そして、意味論と構文論間の矛盾と見える事柄は、結局、どう理解すべきなのか。これを理解するために「証明表」の全行に証明値を入れてみよう。
ところでこの「証明表」は、古典論理の「真理表」に相当するものだが、同書には直観主義論理の意味論を「真理表で表わすことはできませんけど」（p.173）と書かれていて、古典論理の「真理表」に相当するようなものは示されていない。
もちろん証明値⊩、⊮を論理式の肯定、否定とする直観主義論理は、真理値1、0を論理式の肯定、否定とする古典論理とは異なるので、この意味で、直観主義論理の意味論を古典論理の真理表で表わすことができないのは当然のことだが、「真理表で表わすことはできません」というのはその意味で言われているのではないだろう。真理値であれ証明値であれ、ともかく古典論理の真理表のような原子命題の値から構成された表で直観主義論理の意味論を示すことはできない、というのがそこで言われていることの主旨と思われる。
ただし、同書p.175「分子式の分析」では、認識史K0（認識史01）について、いくつかの論理式の証明値を求めている。そこで求められている証明値は認識史01に関してだけであり、また頭初期α、後続期βのうち頭初期だけの場合もあるが、この「分子式の分析」を、認識史11、01、00の頭初期α、後続期βすべてについて行うことができれば「証明表」が得られることは確かである。
また、直観主義命題論理では古典命題論理と同じように「妥当式か否かを機械的に示す方法（認識史分析）」があるということなので（p.178）、この点からも「真理表」に代わる「証明表」のような固定値を持つ表で、意味論（ここでは「直観主義論理の意味論」Ⅱの部分）を別様に表現することが可能であるように思われる。
しかしながら「分子式の分析」に、∧、∨、⊃、￢の4つの結合子のうち⊃だけ、証明値の分析が書かれていない点が気がかりである。⊃の分析が慎重に避けられており、このところに「真理表で表わすことはできませんけど」ということの真意が暗示されている可能性も考えられる。
ここに示す「証明表」は、１命題Ｐに否定子と結合子を加えた分子式（論理式）、すなわち排中律と二重否定除去則に関するものだけであり、これについては以下に見るとおり、直観主義論理の状況をよく表現しているといえる。しかし２命題Ａ、Ｂにおける論理式でも同様に「証明表」が作成でき、かつ、直観主義論理の定理を表現するものであるのかは確認できていない。
例えば、同書p.168問題77に挙げられている、ド・モルガンの法則の一つである￢(Ａ∧Ｂ)⊃(￢Ａ∨￢Ｂ)が、直観主義論理で非定理であるのに従って、この「証明表」でも妥当式とならないことが表現され、その逆の(￢Ａ∨￢Ｂ)⊃￢(Ａ∧Ｂ)が、直観主義論理で定理であるのに従って、この「証明表」で妥当式として表現される、などの確認は行えていないので、以下の「証明表」は、とりあえずは直観主義論理を理解するための便宜的な方法として理解していただきたい。（これについての見解はEasy study 5-4-5に「追記」として掲載予定。2021年2月。→ Hard study 5-5-1 ～ 5-5-4として追記。2024年2月。その中で、ここで作成した「1命題Ｐ」に関する証明表については、Hard study 5-5-1に作成した「2命題ＡＢ」に関する証明表と共に、直観主義論理のもう一つの意味論であるハイティング代数の「3値モデル」真理表に相当することが確認された。なお、Easy study 5-4-5は、Hard study 5-4-5として内容を改訂。）
さて、結構な留保付きではあるが、以下では先の「証明表」を使って、直観主義論理の理解を得ていこう。排中律では￢Ｐ、二重否定除去則では￢￢Ｐが出てくるので、まずこれらの証明値を確定してみる。
与えられているのは、Easy study 5-2 -1の「直観主義論理の意味論Ⅰ～Ⅲ」と、Hard study 5-2-2での意味論Ⅱ(5)の読み替え(ｲ)(ﾛ)(ﾊ)(ﾆ)、および下のＰの認識史である。（以下、認識史10は除外）
■直観主義論理￢Ｐの証明値
認識史11α
α⊩Ｐなのでα⊮￢Ｐ
認識史11~β
~β⊩Ｐなので~β⊮￢Ｐ
認識史01α
意味論規定Ⅱ(5)←方向により、すべてのβで⊮Ｐならばαで⊩￢Ｐ
すなわち、α⊮Ｐかつ~β⊮Ｐである認識史のとき、αで⊩￢Ｐ
（※Ⅱ(5)は同値（双条件）なので、両辺の真理値は一致する）
ところが認識史01はα⊮Ｐかつ~β⊩Ｐなので、αで⊩￢Ｐとはならない。
すなわち、αでは⊮￢Ｐ
認識史01~β
認識史01では~β⊩Ｐ
ゆえに、~β⊮￢Ｐ
認識史00α
意味論規定Ⅱ(5)←方向により、すべてのβで⊮Ｐならばαで⊩￢Ｐ
すなわち、α⊮Ｐかつ~β⊮Ｐの認識史のとき、αで⊩￢Ｐ
認識史00はα⊮Ｐかつ~β⊮Ｐなので、αで⊩￢Ｐ
認識史00~β
認識史00ではα⊩￢Ｐ
ゆえに意味論Ⅱ(1)より、~β⊩￢Ｐ
以上から、直観主義論理の￢Ｐの証明表は次のようになる。
上の証明表からα期、~β期それぞれのＰと￢Ｐの選言の証明値を直観主義論理の意味論規定Ⅱ(3)に従ってとってみると以下のようになる。（認識史11のα｜Ｐとα｜￢Ｐ、認識史11の~β｜Ｐと~β｜￢Ｐ、認識史01のα｜Ｐとα｜￢Ｐ…の証明値をそれぞれ古典論理の∨の真理表と同じように演算しても以下の値が得られる。）
直観主義論理のＰ∨￢Ｐの証明値が上表のようになることは、意味論規定からも直接、以下のように確認できる。
■直観主義論理Ｐ∨￢Ｐの証明値
認識史11α
認識史11によりα⊩Ｐ
ゆえに、α⊩Ｐ∨￢Ｐ
認識史01α
（前段 Hard study 5-2-3に既出）
認識史00α
意味論規定Ⅱ(3)←方向により､α⊩Ｐまたはα⊩￢Ｐならば､α⊩Ｐ∨￢Ｐ……(1)
もし(1)の前件が成立しなければ後件も成立せず、α⊮Ｐ∨￢Ｐとなる。
(1)の前件は選言なので「または」の前後いずれかが成立すれば、後件が成立する。
以下、α⊩￢Ｐであることを確認する。
意味論規定Ⅱ(5)←方向により、すべてのβで⊮Ｐならばαで⊩￢Ｐ
すなわち、α⊮Ｐかつ~β⊮Ｐの認識史のとき、αで⊩￢Ｐ
認識史00はα⊮Ｐかつ~β⊮Ｐなので、
αでは⊩￢Ｐ…(2)
(2)により、(1)の前件が成立することが確認された。
ゆえに(3)の後件が成立し、α⊩Ｐ∨￢Ｐ
認識史11~β
α⊩Ｐ∨￢Ｐなので~β⊩Ｐ∨￢Ｐ（式の証明は後続期に引き継がれる）
認識史01~β
認識史01では~β⊩Ｐ
ゆえに、~β⊩Ｐ∨￢Ｐ
認識史00~β
α⊩Ｐ∨￢Ｐなので~β⊩Ｐ∨￢Ｐ
続いて、￢￢Ｐの各認識史の証明値は以下の通り。
■直観主義論理￢￢Ｐの証明値
認識史11α
認識史11ではα⊩Ｐなので、α⊮￢Ｐ……(1)
また~β⊩Ｐであるから、~β⊮￢Ｐ……(2)
(1)、(2)と、Ⅱ(5)←方向により、α⊩￢￢Ｐ……(3)
認識史11~β
α⊩￢￢Ｐなので~β⊩￢￢Ｐ
認識史01α
認識史01では~β⊩Ｐなので、Ⅱ(5)←方向裏により、α⊮￢Ｐ……(1)
また~β⊩Ｐであるから、~β⊮￢Ｐ……(2)
(1)、(2)と、Ⅱ(5)←方向により、α⊩￢￢Ｐ……(3)
※このように、認識史01ではαで￢￢Ｐが証明されているのにＰが証明されていない。この事態が二重否定除去則が公理ではないことを示している。
認識史01~β
α⊩￢￢Ｐなので~β⊩￢￢Ｐ
認識史00α
認識史00ではα⊮Ｐかつ~β⊮Ｐなので、Ⅱ(5)←方向によりα⊩￢Ｐ……(1)
(1)より~β⊩￢Ｐ……(2)
(2)とⅡ(5)←方向裏により、α⊮￢￢Ｐ……(3)
認識史00~β
上により認識史00ではα⊩￢￢Ｐ⊃Ｐ（偽を前件とする条件法は真）
したがって~β⊩￢￢Ｐ⊃Ｐ
認識史00では~β⊮Ｐなので、~βで￢￢Ｐ⊃Ｐの証明値が真となるためには、前件の証明値は偽でなければならない。
したがって~β⊮￢￢Ｐ
以上から、直観主義論理の￢￢Ｐの証明表は次のようになる。
上の証明表からα期、~β期それぞれの￢￢ＰとＰの条件法の証明値を直観主義論理の意味論Ⅱ(4)に従ってとってみると以下のようになる。（めんどうであれば古典論理の⊃の真理表のように演算しても同じ証明値を得るが、⊃の場合に古典論理と同じように演算してよいかどうかは確認していない。2021年2月。→ ￢￢Ｐ⊃Ｐは、直観主義論理⊃の特異性（Hard study 5-5-1 直観主義論理⊃の証明表に記載）に触れない論理式のため上の演算で正しいことを確認。2024年2月。）
直観主義論理の￢￢Ｐ⊃Ｐの証明値が上表のようになることは、意味論規定から直接、以下のように確認できる。
■直観主義論理￢￢Ｐ⊃Ｐの証明値
認識史11α
認識史11ではα⊩Ｐなので、α⊮￢Ｐ……(1)
また~β⊩Ｐであるから、β⊮￢Ｐ……(2)
(1)、(2)と、Ⅱ(5)←方向により、α⊩￢￢Ｐ……(3)
前件が真、後件が真である条件式は真であるから、
(3)と、認識史11のα⊩Ｐにより、α⊩￢￢Ｐ⊃Ｐ
認識史01α
（前段に既出）
認識史00α
認識史00ではα⊮Ｐかつ~β⊮Ｐなので、Ⅱ(5)←方向によりα⊩￢Ｐ……(1)
また(1)より~β⊩￢Ｐ……(2)
(2)とⅡ(5)←方向裏により、α⊮￢￢Ｐ……(3)
前件が偽である条件式は、後件の真偽にかかわらず真であるから、
(3)により、α⊩￢￢Ｐ⊃Ｐ
認識史01~β
認識史01では~β⊩Ｐ
後件が真である条件式は、前件の真偽にかかわらず真であるから、
~β⊩￢￢Ｐ⊃Ｐ
ここでいま一度確認しておくと、知りたいのは意味論のどこに排中律および二重否定除去則の拒否が仕込まれているのかということ、そして意味論と構文論間の矛盾と見える事態をどう理解すべきかの二点である。
また(ﾛ)の意味を理解し、最終的には、Easy study 5-1からの問題意識である「古典論理と直観主義論理を分ける境界」について理解したい。
まず老婆心ながら次を確認しておく。証明表で確認してきた論理式を、今後、考察するにあたり、￢Ｐと￢￢Ｐではα⊮、~β⊩、Ｐ∨￢Ｐと￢￢Ｐ⊃Ｐではα⊮、~β⊮という証明状況が出ていないが、これで￢Ｐ、￢￢Ｐ、Ｐ∨￢Ｐ、￢￢Ｐ⊃Ｐにおけるすべての事態が言い尽くされているのかという疑問が起こるかもしれない。もしすべての事態が出ていないならば、上に導いた証明値に基づく今後の考察は不十分なものとなる懸念がある。
しかしこの懸念は、古典論理のトートロジーの真理表を思い出すことで払拭される。先に見た「Ｐ∨￢Ｐの真理表」や「前件肯定式の真理表」では当該列に1だけがあって0はない。それでもそれは排中律や前件肯定式のありえるすべての事態を示していたのであった。つまり、それらにおいては真理であることがありえる事態のすべてだったのである。論理式の考察において「ありえるすべての事態」というのは元の命題において求められることであって、演算を経た論理式で、真／偽、証明／不証明すべての組み合せが必ず出揃うわけではないということである。
そのようなわけで、上の証明表からは早速次のことが明らかとなる。
￢Ｐと￢￢Ｐでは頭初期で不証明でありながら後に証明される事態というのはない。この事態は、命題Ｐに関しては認識史01として存在し、Ｐのあり方そのものだが、￢Ｐと￢￢Ｐではそれはないということである。
また、Ｐ∨￢Ｐと￢￢Ｐ⊃Ｐでは最終的に不証明に終わる事態がないことも帰結している。これが実際には何を言うものなのかは今のところまったく分からないが、次節でいくらかの理解が得られるはずである。