Mizar/本体部/量化
表示
∀x F(x) は For all x such that F(x) holds.「任意のxについて、F(x)が成り立つ」 for x st F.x holds
∃x F(x) は There exists x such that F(x) holds.「あるxが存在して、F(x)が成り立つ」 ex x st F.x holds
st (such that)が 域と演算式との区切り文字
従って、上記の式は分かりやすく記述すると以下のような形にもかける。(Mizarの解説書などによる)
(∀x)(F(x)) (∃x)(F(x))
または階層的に記述すると
(∀x(F(x))) (∃x(F(x)))
また、
∀x F(x)→G(x) は For all x such that F(x) holds G(x). 「任意のxについて、F(x)ならばG(x)が成立する」 for x st F(x) holds G(x)
となる。