種別[gsm] 2022-02-11T13:15:16Z
セクショングローバル共有メモ
日時2022-02-11T13:15:16Z
元URL(URLなし)

(承前) ……。 とりとめのない話 その4。 IM(P,Q) が成り立つ P,…

jrf> (承前)

……。

とりとめのない話 その4。

IM(P,Q) が成り立つ P, Q の条件を考える。

その1 を参考に、x のある範囲内に P Q を限定するという方向が考えられる。そのような x の範囲として その3 を参考に x が「必然的に Q や ¬Q 」ではありえない範囲であれば、◇Q(x) を自由に導き出しても問題ないだろうとあたりを付ける。「「必然的に Q や ¬Q 」ではありえない範囲」に x が属することを x∈(¬◇□(Q,¬Q)) と表そう。

新しい「因明述語組 P, Q」を

IM4_1(P,Q) == (∃y.P(y)∧Q(y))→(∀x. x∈(¬◇□(Q,¬Q)) → P(x)→◇Q(x))

…としよう。問題として (∃y.P(y)∧Q(y)) の y にも y∈(¬◇□(Q,¬Q)) が必要ではないかというのがあるが、それは後ほど疑似問題とわかるので、おいておこう。

◇Q(x) と □Q(x) は重なっていて良いので、¬◇□(Q,¬Q) の中から □Q(x) は抜こう。すると、

IM4_2(P,Q) == (∃y.P(y)∧Q(y))→(∀x. x∈(¬◇□¬Q) → P(x)→◇Q(x))

ところで、これが任意の P,Q について成り立つとすると、結局 P(x) = True でも良いから Q(y) が成り立てば ◇Q(x) が成り立ち、そうなると今度は IM4_2 において P(x) の役割がなくなる。これを役割あるようにするには (∃y.P(y)∧Q(y)) ではなく、(∃y.P(y)→Q(y)) を使ったほうが良いとなる。つまり、

IM4_3(P,Q) == (∃y.P(y)→Q(y))→(∀x. x∈(¬◇□¬Q) → P(x)→◇Q(x))

ところで、x∈(¬◇□¬Q) というのは結局 ¬◇□¬Q(x) のことではないか…と考える。すると、式を簡約化でき、

IM4_4(P,Q) == (∃y.P(y)→Q(y))→(∀x. □◇Q(x) → P(x)→◇Q(x))

つまり、x∈(¬◇□¬Q) というのは□◇Q(x)…Q(x) が可能なのが必然となる範囲だったことになる。ところで □◇Q(x) にも P の限定が付けられるはずだ。すると、

IM4_5(P,Q) == (∃y.P(y)→Q(y))→(∀x. □(P(x)→◇Q(x)) → P(x)→◇Q(x))

ところで、□R → R であるから

□(P(x)→◇Q(x)) → (P(x)→◇Q(x))

は当然成り立つ。つまり、IM4_5(P,Q) は (∃y.P(y)→Q(y)) に意味がなくなり(つまり疑似問題となり)、常に真になる。

議論はつぶれてしまった!

ただ、ここの議論から救い出すべき部分がある。それは、(∃y.P(y)∧Q(y)) ではなく、(∃y.P(y)→Q(y)) を使ったほうが良い…という部分である。これは一般の因明述語対にも言えて、だから、IM(P,Q) は次のように定義しなおしたほうがよいことがわかる。

IM1_2(P,Q) == (∃y.P(y)→Q(y))→(∀x.P(x)→◇Q(x))

ところで、ここで、上のほうで、(4-2) の Q(b) を ◇Q(b) に置き換えるのに相当することを導入しよう。すると、

IM1_3(P,Q) == (∃y.P(y)→◇Q(y))→(∀x.P(x)→◇Q(x))

さて、これは存在記号(∃)を全称記号(∀)に置き換えるという式になっている。そんなことは普通やってはいけない。しかし、やっていいとすれば、IM4_5 を参考に、

P(x)→◇Q(x) == P(x)→◇Q(x) ∧ □(P(x)→◇Q(x))

…なるような P, Q … P Q が x∈(¬◇P∧□¬Q) に限定されるように作った P,Q でのみ言えるとすればいい…ということになる。ただ、よくよく考えれば、必然記号は取って良く、結局 (∀x.P(x)→◇Q(x)) が成り立つような P, Q について IM1_3(P,Q) が言えるということになる。…となると、IM1_3(P,Q) の (∃y.P(y)→◇Q(y)) は真であれば都合が良いだけの疑似問題になる。

そして、それは (∀x.P(x)→◇Q(x)) が成り立つのはどういうときか…というどうどう巡りになることを意味している。

IM1_3 ではなく IM1_2 を取れば結果は変わるが、今回のその2と合わせた議論が必要になるというだけのことだろう。