形式的論証と数学的論証

ウィキペディア小見出し辞書

形式的論証と数学的論証

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/05/15 06:56 UTC 版)

「論証」の記事における「形式的論証と数学的論証」の解説

数学においては、論証のそれぞれの文を一階ペアノ算術のような形式言語で書くことで形式化されることが多い。形式化された論証は、次のような属性を持つ。 前提はそのままで明確に識別される。 推論はその論証が書かれた形式言語の推論規則に基づいて正当化される。 結論はそのような推論の最終的結果として現れる。 したがって、形式的論証の妥当性の検証は単純であり、これら3つの属性を持つかどうかは容易に検証可能である。 数学における多くの論証は、厳密な意味では形式的ではない。厳密に形式的な証明は、自明で簡単なものを除いては極めて退屈な作業であり、コンピュータの補助なしではそれほど長続きしない。自動定理証明は、そのような問題の解決策としても使われる。 一般に数学的論証は、その理論内で形式化可能な範囲内で形式的であると言える。このような性質を指して、数学的論証は「厳密; rigorous」であると称する。数学者は、必要なら形式的な推論の連鎖を構築できると確信しているため、そのような連鎖を形式化によって1つの推論にまとめたがる傾向がある。 いずれにしても、論証を形式化する利点は、証明理論のような妥当な数学的論証に関する理論を構築できる可能性にある。証明理論は数学全体の妥当な論証のクラスを調査し、健全な数学的論証の結論としてどのような文が出てくるのかをはっきりさせる。ゲーデルの不完全性定理は証明理論の成果であり、全ての真なる数学的文は形式化された健全な数学的論証から生み出されるという事実を明らかにした。実際には、全ての真なる数学的文が証明可能というわけではない。