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)

となる。