例：自然数による実現可能性
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/03/29 03:57 UTC 版)
「実現可能性 (論理学)」の記事における「例：自然数による実現可能性」の解説
クリーネによるオリジナル版の実現可能性の定義は、ハイティング算術（英語版）の論理式の実現子として自然数を用いる。自然数 n と式 Aの間の関係「n がA を実現する」を、ハイティング算術の言語で定義する。 ただし以下において、順序対 (n, m) はある固定された有効な対関数を使うことで単一の数値として扱う。また、各自然数 n に対して φn はインデックス n の計算可能関数（すなわち、何らかの方法で列挙された計算可能関数の列 { φ n } n ∈ N {\displaystyle \{\varphi _{n}\}_{n\in \mathbb {N} }} における n 番目の関数）である。 自然数 n が原子論理式 s = t を実現するとは、 s = t が真であることと同値。 従って、任意の自然数は恒真な等式を実現し、また矛盾した等式を実現する自然数はない。 順序対 (n, m) が論理式 A ∧ B {\displaystyle A\land B} を実現するとは、n が A を実現して、かつ m が B を実現することと同値。つまり、連言の実現子とはそれを構成する各式の実現子の対である。 順序対 (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 が証明できる。
※この「例：自然数による実現可能性」の解説は、「実現可能性 (論理学)」の解説の一部です。
「例：自然数による実現可能性」を含む「実現可能性 (論理学)」の記事については、「実現可能性 (論理学)」の概要を参照ください。
- 例：自然数による実現可能性のページへのリンク
