かじもとにっき

ゆるふわなおはなしをかきます

限量化された論理式への含意の分配

xに現れるdummyが式Qに自由に現れない場合、
(\mathop {\exists x}\limits_R .P) \Rightarrow Q \equiv (\mathop {\forall x}\limits_R .P \Rightarrow Q)
及び、
\exists x.R \Rightarrow ( (\mathop {\forall x}\limits_R .P) \Rightarrow Q \equiv (\mathop {\exists x}\limits_R .P \Rightarrow Q))
が成り立ちます。
特に2つ目の定理において、\forall x.\neg Rの時結論の左辺は{\mathop{\rm true}\nolimits}  \Rightarrow Q\equiv Q)、右辺は{\mathop{\rm false}\nolimits}  \Rightarrow Q\equiv \rm true)となり、仮定\exists x.Rがなければ恒真になりません。