正式な証明

論理学と数学において、形式的証明または導出は、文の有限列（形式言語に関連して整形式の式と呼ばれる）であり、各文は公理、仮定、または推論規則に従って列内の前の文から従うものである。形式的証明は、厳密で、曖昧さがなく、機械的に検証可能であるという点で自然言語の議論とは異なる。^[1]仮定の集合が空の場合、形式的証明の最後の文は形式体系の定理と呼ばれる。定理の概念は一般に有効であるが、与えられた文の証明を確実に見つける方法や、証明が存在しないと判断する方法がない可能性がある。フィッチスタイルの証明、シーケント計算、自然演繹の概念は、証明の概念の一般化である。 ^{[2] [3]}

定理は、証明の中でその前に現れるすべての整形式の式から得られる構文上の帰結です。整形式の式が証明の一部として適格となるためには、証明シーケンス内の前の整形式の式に演繹装置の規則(何らかの形式体系) を適用した結果でなければなりません。

形式的な証明は、対話型の定理証明（例えば、証明チェッカーや自動定理証明器の使用を通じて）においてコンピュータの助けを借りて構築されることが多い。 ^{[4]重要なのは、これらの証明はコンピュータによっても自動的にチェックできることである。形式的な証明のチェックは通常簡単であるが、証明を}見つける問題（自動定理証明）は、使用されている形式的なシステムに応じて、通常、計算上扱いにくいか、または半分しか決定できない。

形式言語は、有限の記号列の集合です。このような言語は、その表現の意味に関係なく定義できます。つまり、解釈が割り当てられる前、つまり意味を持つ前に存在することができます。形式的な証明は、いくつかの形式言語で表現されます。

形式文法（形成規則とも呼ばれる）は、形式言語の整形式の式を正確に記述したものです。これは、整形式の式を構成する形式言語のアルファベット上の文字列の集合と同義です。ただし、その意味論（つまり、その意味） は記述しません。

形式体系(論理計算または論理システムとも呼ばれる) は、形式言語と演繹装置 (演繹システムとも呼ばれる) から構成されます。演繹装置は、変換規則(推論規則とも呼ばれる)のセットまたは公理のセット、あるいはその両方から構成されます。形式体系は、1 つ以上の他の式から 1 つの式を導出するために使用されます。

形式体系の解釈とは、形式体系の記号に意味を割り当て、文に真理値を割り当てることです。解釈の研究は形式意味論と呼ばれます。解釈を与えることは、モデルを構築することと同義です。

• 公理システム
• 形式検証
• 数学的証明
• 証明アシスタント
• 証明計算
• 証明理論
• 証明（真実）
• デ・ブリュイン要因

• 「形式的証明に関する特別号」。アメリカ数学会の通知。2008 年 12 月。
• 2πix.com: 論理 数学と論理を扱う一連の記事の一部です。
• 形式的証明のアーカイブ
• ミザールホームページ
• Pr∞fWiki、定義:証明システム/形式的証明