一意存在量化
Def
$ x
を自由変項とする任意の論理式
$ \varphi(x)
に対し，
$ \Sigma_1
論理式
$ {\exists!}_x \varphi(x)
を↓の略記とする．
$ {\exists!}_x \varphi(x) \equiv \exists_x\lbrack \varphi(x) \land \forall_{y,y'}\lbrack\varphi(y) \land \varphi(y') \to y = y\rbrack \rbrack