\exist

なんちゃらが、少なくとも1つは存在する

全称量化子∀と否定で同義を表現できる

\exist xPx⊨⫤\lnot\forall x\lnot Px

\lnot\exist xPx⊨⫤\forall x\lnot Px

\exist!は「唯一つ存在する」を意味する

例えば ref pp.116-117

\forall x. Gxを

全ての人間は善人である とすると、

\forall x.\lnot Gxは、

\lnot\forall x.Gxは、

→ 悪人が少なくとも一人は存在する

\lnot\forall x.\lnot Gxは、

→ 善人が少なくとも一人は存在する

=\exist x. Gx