有界量化を略記として導入することについて
$ \forall_{x \leq n}\lbrack\varphi(x)\rbrack \equiv \forall_{x}\lbrack x \leq n \to \varphi(x)\rbrack
$ \exists_{x \leq n}\lbrack\varphi(x)\rbrack \equiv \exists_{x}\lbrack x \leq n \to \varphi(x)\rbrack
これらは真の意味で有界なのか？別に計算機側にとっては無限に$ xを走査しないか？みたいなことを思う