実現可能性 (論理学)
順序対 (n, m) が論理式 A ∨ B {\displaystyle A\lor B} を実現するとは、n が 0 または 1 で、かつ n が 0 ならば m は A を実現して、n が 1 ならば m は B を実現することと同値。従って、選言の実現子はそれを構成する式のどちらかを明示的に(n で)指してその実現子を(m で)提供するものである。
自然数 n が論理式 A → B {\displaystyle A\to B} を実現するとは、A を実現する任意の m について φn(m) が B を実現することと同値である。従って、含意の実現子は仮定となる式の実現子を引数に取って帰結となる式の実現子を返す計算可能関数とみなせる。
順序対 (n, m) が論理式 ∃ x . A ( x ) {\displaystyle \exists x.A(x)} を実現するとは、m が A(n) の実現子であることと同値である。すなわち、存在文の実現子はその存在量化についての明示的な証拠を、それに裏打ちされた論理式の実現子と共に提供する。
自然数 n が論理式 ∀ x . A ( x ) {\displaystyle \forall x.
A(x)} を実現するとは、任意の m について φn(m) が定義されていて、かつ φn(m) が A(m) を実現することと同値である。従って、全称文の実現子は自然数 m に対してそれによるインスタンスの実現子を提供する計算可能関数とみなせる。
この定義により、次の定理が得られる:
A をハイティング算術 (HA) の文とする。HAで A が証明できるならば、HAで A を実現するような自然数 n が存在することが証明できる。
一方で、実現されるがHAで証明可能でない論理式が存在する。この事実はローズによって初めて示された。
このメソッドのさらなる解析は、HAが選言文特性と存在文特性(英語: Disjunction and existence properties)を持つことの証明に使われる。
もしHAで ∃ x . A ( x ) {\displaystyle \exists x.A(x)} が証明できるなら、 HAで A(n) が証明できるような自然数 n が存在する。
HAで A ∨ B {\displaystyle A\lor B} が証明できるなら、HAで A が証明できるか、またはHAで B が証明できる。