証明論と構成的数学
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/08 05:41 UTC 版)
詳細は「証明論」を参照 証明論は様々な論理推論体系における形式的証明の研究である。それら形式的証明は形式的な数学的対象であるから、それらの解析は数学的手法を用いて行うことができる。ヒルベルト流の体系、自然演繹の体系、ゲンツェンによって開発されたシークエント計算などを含む、いくつかの推論体系はよく考察される 数理論理学の文脈において、構成的数学の研究は、可述的体系の研究のような、非古典論理の体系の研究を含む。可述主義の初期の支持者はヘルマン・ワイルである。彼は実解析の大部分を可述的な方法だけを用いて展開できることを示した（Weyl 1918）。 形式的証明は完全に有限的なものであるが、構造における真理性はそうでないことから、構成的数学での作業では証明可能性を強調することが多い。古典（または非構成的）体系における証明可能性と直観主義（または構成的）体系での証明可能性との間の関係はとりわけ関心が持たれる。ゲーデル・ゲンツェン変換のような結果は古典論理を直観主義論理に埋め込む（翻訳する）ことが可能であることを示している。直観主義的証明に関するある性質は古典論理の証明に関するそれに逆翻訳できる。 最近の証明論における発展にはUlrich Kohlenbachによるproof miningの研究やMichael Rathjenによる証明論的順序数の研究が含まれる。
※この「証明論と構成的数学」の解説は、「数理論理学」の解説の一部です。
「証明論と構成的数学」を含む「数理論理学」の記事については、「数理論理学」の概要を参照ください。
ウィキペディア小見出し辞書の「証明論と構成的数学」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 証明論と構成的数学のページへのリンク
