Σn述語 - mrsekut-p

Σn述語

存在量化子∃から始まる量化子が交互の述語

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

定義

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

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

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

存在量化子∃から交互に$ n個なので、偶奇によって決まる

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

定理

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

つまり、$ A,A'が共に$ \Sigma_n述語だとすると、$ A(\vec{x})\land A'(\vec{x})も$ \Sigma_n述語

$ Aが$ \Sigma_nならば、

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

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

https://gyazo.com/57f4f3b3bb2797340d3e297dac7f1443

例えば$ A(\vec{x})\iff (\exist y_1)(\forall y_2)(B(\vec{x},y_1,y_2))で$ Bが計算可能なとき、$ Aは$ \Sigma_2述語である

このとき以下が成り立つ

$ A(\vec{x})\iff (\exist y_1)(\forall y_2)(\exist z)(B(\vec{x},y_1,y_2)\land(z=z))

$ A(\vec{x})\iff (\forall z)(\exist y_1)(\forall y_2)(B(\vec{x},y_1,y_2)\land(z=z))　

右辺の(B() \land ())の部分は計算可能なので、これは$ \Sigma_3述語である

具体例

haltは$ \Sigma_1述語

$ \mathrm{Halt}(p,x)\iff (\exist t)(\mathrm{Executable}(p,x)\land\mathrm{HaltBefore}(p,x,t))