形式数学への応用
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/12/22 09:30 UTC 版)
ある形式理論のゲーデル数化が確立されると、その理論の各推論規則は自然数についての関数として表される。f がゲーデル写像で、数式 A と B から推論規則 r によって数式 C が得られるとする。 A , B ⊢ r C {\displaystyle A,B\vdash _{r}C\ } すると、次のようになる自然数についての算術関数 gr が存在するはずである。 g r ( f ( A ) , f ( B ) ) = f ( C ) {\displaystyle g_{r}(f(A),f(B))=f(C)\ } これはゲーデルの用いたゲーデル数化においては真であり、符号化された数式がそのゲーデル数から算術的に復元可能な他のゲーデル数化方式でも成り立つ。 従って、ペアノの公理のような形式理論を使えば数の間の算術的関係を示すことができるが、ゲーデル数化を使えば間接的にそういった理論自体に関する文を作ることができる。このような技法によってゲーデルは形式体系の属性の一貫性と完全性についての証明を行った。
※この「形式数学への応用」の解説は、「ゲーデル数」の解説の一部です。
「形式数学への応用」を含む「ゲーデル数」の記事については、「ゲーデル数」の概要を参照ください。
ウィキペディア小見出し辞書の「形式数学への応用」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 形式数学への応用のページへのリンク
