奇妙な恒真式

(A ∨ B → A) ∨ (A ∨ B → B) は(古典論理で)恒真なのですが，これはわりと奇妙に見えます。そこで，なんで奇妙か考えてみた。

簡単にいうと「A または B」からは A と B のどっちもいえないので，二つの成立しないものが ∨ でつながってても正しくなさそう，ということのように思うけど，すべての ∨ がそう見えるわけではない。例えば A∨B → A∨B なら別に違和感がないけど，結論の部分で A も B も成り立っていないのはさっきと同じ状況だ。

もっと具体的に (x = 0 ∨ x > 0 → x = 0) ∨ (x = 0 ∨ x > 0 → x > 0) を考えてみるとどうか。x は非負なんだけど 0 か正かどっちかはわからない，という状況が仮定されているにもかかわらず，x = 0 か x > 0 かのどっちかに決まると言っているように見える。そうするとなんか変に聞こえる。

たぶん各々の disjunct が ∀x で囲まれているように感じられるのではなかろうか。つまり (∀x(x = 0 ∨ x > 0 → x = 0)) ∨ (∀x(x = 0 ∨ x > 0 → x > 0)) のように見えているのではないか。もしこのように量化されていると，正しくない論理式になる。

一方 ∀x が一番外側に一つだけあるとすると正しい。つまり ∀x( (x = 0 ∨ x > 0 → x = 0) ∨ (x = 0 ∨ x > 0 → x > 0) ) ということで，こちらが本来されるべき解釈。これは x が与えられたとして，それが 0 だったら左，正だったら右，負だったら両方が成り立つのだから結局いつでも成り立つ。こっちは ∨ の両側に現れる x が同じ数を指しているから問題ないのだ。

ところで x が自然数のとき，x = 0 ∨ x > 0 と書くとこれには違和感がない。これもどっちが成り立つかはわからないはずだけど。もしかしたら「ならば」が特別なのだろうか。つまり「ならば」と言われるとその外側になんとなく ∀ がついてるような気がするのではないか。もうちょっと例を探してみるとおもしろいかもしれない。