形式的証明

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

形式的証明

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/03/31 01:46 UTC 版)

「ケプラー予想」の記事における「形式的証明」の解説

2003年1月、ヘイルズはケプラー予想の完全な形式的証明を求める共同プロジェクトを開始した。その目標は、証明の妥当性に一切の疑問を残さないため、HOL LightやIsabelleなどの自動証明検証（英語版）[訳語疑問点]プログラムにかけられるような形式的証明を構築することであった。プロジェクトは「Flyspeck」と名付けられた。そのうちの3文字、F、P、Kは「Formal Proof of Kepler」（ケプラーの形式的証明）から取ったものである。ヘイルズは完全な形式的証明を構築するのには20年ほどの作業が必要だと見積もっていた。2014年8月10日にプロジェクトの終結が発表された。2015年1月、ヘイルズと21人の共同研究者は「ケプラー予想の形式的証明」と題された論文を公開した。

形式的証明

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/04/24 18:27 UTC 版)

「形式体系」の記事における「形式的証明」の解説

形式的証明は整式の連なりである。証明を構成する整式は、公理かまたは証明内の前の整式に推論規則を適用して導出されたものである。一連の整式の最後の整式が定理と認識される。 このような観点を総じて、数学は「形式主義」的であると称する。ダフィット・ヒルベルトは形式体系を論じる学問分野として超数学を起こした。形式体系を論じるために使われる言語を「メタ言語」と呼ぶ。メタ言語は自然言語そのものである場合もあるし、何らかの形式化がなされている場合もある。しかし、一般に研究対象である形式体系を構成する形式言語ほどには形式化されていない。 ある形式体系が与えられたとき、定理群を定義でき、それらをその形式体系内で証明できる。形式体系は証明が存在する全ての整式で構成される。すなわち全ての公理は定理とみなされる。公理や既に存在する定理に推論規則を適用して得られる整式も定理に含まれる。整式の文法とは異なり、ある整式が定理であるか否かを決定する手順は必ずしも存在しない。ここでいう定理は「形式体系についての定理」ではなく、混同をさけるため後者をメタ定理（英語版）とも呼ぶ。

形式的証明

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:48 UTC 版)

「一階述語論理」の記事における「形式的証明」の解説

命題論理においては、論理公理 (logical axiom) と呼ぶ論理式の集合と、ある論理式たちから新たな論理式を導出する規則（推論規則）を導入し、論理公理から推論規則の有限回の適用によって得られる論理式全体とトートロジー全体が一致するようにすることができる（命題論理の健全性と完全性）。一階述語論理においても、適切に論理公理と推論規則を導入することで、論理公理から推論規則を使って導出される論理式全体と恒真論理式全体が一致するようにできる。 形式的証明の定義の仕方はひとつではなく、様々な異なる（等価な）方法がある。ここで述べる定義はヒルベルト流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。ゲンツェン流の形式的証明では逆に、公理を少なくして推論規則を多く用いている。ここで述べるものと異なる証明可能性の定義については「自然演繹」「シークエント計算」などを参照。