\exist x.Pxが\forall x.Pxを含意する

つまり、\forall x.Pxが成り立つような命題は、\forallを\existに変えても常に成り立つ

p.119の図

右側だけを見てみると、

緑が全称量化子、青が存在量化子を使っている

左右の同じ場所を指しているものは同じ意味

\existは、\forallと\lnotの組み合わせで同義を表現できるので、それをやっている

「\exist x.Pxが\forall x.Pxを含意する」というのは、右側の上2つのことを言っている

もしくは、左側の下2つ

参考

周辺の解説もわかりやすい