Πn述語
否定はΣ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が入る
全称量化子∀から交互に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}でもある
具体例
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)))