Πn述語 - mrsekut-p

Πn述語

全称量化子∀から始まる量化子が交互の述語

$ Aが$ \Pi_n述語のとき、$ \lnot Aは$ \Sigma_n述語

定義

$ k変数述語$ Aに対して、ある$ (k+n)変数計算可能述語$ Cが存在して

$ A(\vec{x})\iff (\forall y_1\in\mathbb{N})(\exist y_2\in\mathbb{N})(\forall y_3\in\mathbb{N})(\exist y_4\in\mathbb{N})\cdots(\square y_n\in\mathbb{N}) C(\vec{x},\vec{y})

$ \squareには$ \existか$ \forallが入るmrsekut.icon

全称量化子∀から交互に$ n個なので、偶奇によって決まる

となるとき、$ Aは$ \Pi_n述語である、という

ちなみに$ \forall\exist\exist\exist \forall\existのように

$ \forall,\existが交互でなく重複している場合は一つとみなせる

$ \forall\exist\exist\exist \forall\existは$ \forall\exist\forall\existに変形できるので、これは$ \Pi_4になる

例えば、$ A(\vec{x})\iff\exist y\exist z\; B(x,y,z)だとすると

$ \iff \exist w\; B(x, \mathrm{left}(w),\mathrm{right}(w))とすることで

$ \iff \exist w\; B'(x, w)と変形できる

left, rightは自然数にコード化するpair関数のようなものを使えばいい

定理

$ Π_n述語同士を論理積や論理和でつなげたものも$ Π_n述語

つまり、$ A,A'が共に$ \Pi_n述語だとすると、

$ A(\vec{x})\land A'(\vec{x})も$ A(\vec{x})\lor A'(\vec{x})も$ \Pi_n述語

$ Aが$ \Pi_nならば、

$ Aは、$ \Sigma_{n+1}でもある

$ Aは、$ \Pi_{n+1}でもある

https://gyazo.com/1e1206086485e330a1f8970682495537

具体例

Total(p)は$ \Pi_2述語

$ \mathrm{Total}(p)\iff(\forall x)(\exist t)(\mathrm{IsCode}(p)\land(\mathrm{Executable}(p,x)\Rightarrow\mathrm{HaltBefore}(p,x,t)))