証明の形式的定義

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

証明の形式的定義

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/06/24 16:03 UTC 版)

「証明 (数学)」の記事における「証明の形式的定義」の解説

数学における命題の証明においては、通常、その正しさの確認は証明の作成者と読者に委ねられている。証明の概念を形式化することによって、その正しさを機械的に判定したり、証明そのものを数学の研究対象とすることもできる。 有限集合を1つ固定し、その有限集合の元をアルファベットという。 アルファベットの有限列を語という。 語の集合を言語という。 言語を1つ固定し、その言語に属する語を命題という。 命題の集合を1つ固定し、その集合に属する命題を事前に認められた仮定として採用し、それを公理と呼ぶ。 命題の有限個の組がどのような条件を満たせば、それらの命題から別の命題が導けるのかを決めたルールの組を決め、それらのルールを推論規則という。 公理の集合と推論規則の集合の組を公理系と呼ぶ。 Aを公理系とし、(P1,...,Pn) を命題の列とする。 任意の i≦n に対し Pi が Pi は公理である Pi は、P1,..., Pi-1 から、許された推論規則によって導くことができる のいずれかを満たすとき、(P1,...,Pn) を Pn の（公理系 A における）証明と言う。 ある (P1,...,Pn) があって、(P1,...,Pn) が Pn の証明であるとき、Pn は（公理系 A において）証明可能である、もしくは Pn は定理であると言う。