「素数は無限個存在する」という命題の証明は以下のようになされる。
証明 : 素数の個数は有限であると仮定する。すべての素数を掛け合わせた数に1を足したものはどの素数で割っても1余り、割り切れない。すなわちそれ自体が素数であるか、ここで想定した最大の素数よりも大きい素数でしか割り切れないことを意味する。いずれにしても、すべての素数以外に素数が存在することになり仮定と矛盾する。よって仮定は間違っており、素数は無限に存在することが示された。 数学における命題の証明においては、通常、その正しさの確認は証明の作成者と読者に委ねられている。証明の概念を形式化することによって、その正しさを機械的に判定したり、証明そのものを数学の研究対象とすることもできる。 Aを公理系とし、(P1,...,Pn) を命題の列とする。 任意の i≦n に対し Pi が のいずれかを満たすとき、(P1,...,Pn) を Pn の(公理系 A における)証明と言う。 ある (P1,...,Pn) があって、(P1,...,Pn) が Pn の証明であるとき、Pn は(公理系 A において)証明可能である、もしくは Pn は定理であるという。 証明を記述する際には、証明とそれ以外の部分をはっきりわけて可読性をあげるため、証明の始めと終わりを明確に示す習慣があり、特に初等中等教育などで初めて証明の記述を学ぶ者に対しては厳しく指導される。 始めや終わりを示す記号は書く人の好みによりさまざまであるが、証明の始めには「proof」「prf.」「pf.」「[証明]」「【証】」や、丸で囲んだ「∵」などが使われる。 証明の終わりには「Q.E.D.」「/証明終わり」「[証明終]」「【証終】」「(おわり)」「□」「■」「‖」や、スラッシュと重ねた「?」などが用いられる。学生のノートやレポートでは、中空の正方形をハッチングで塗ったものが使われることが多い。 一般に、一つの内容を一行に収め、上の行から順に下の行に移るに従って、論証が進むように書かれ、その理由や用いた定理を丸カッコ()でくくって書き添えることが多い。複数の行に書かれた内容を使って次の行が得られるときは、複数の行を中カッコ{、}でくくるか、行末に....〇の丸の中に数字を入れたタグを付け、次の行頭に「@,Aより」などと、説明の流れを明らかにする文言を添える。
その他の用語
存在証明 - 解が存在することを示す行為
一意性証明 - (解がもし存在すれば)解の数は1つであることを示す行為
証明の形式的定義
有限集合を1つ固定し、その有限集合の元をアルファベットという。
アルファベットの有限列を語という。
語の集合を言語という。
言語を1つ固定し、その言語に属する語を命題という。
命題の集合を1つ固定し、その集合に属する命題を事前に認められた仮定として採用し、それを公理と呼ぶ。
命題の有限個の組がどのような条件を満たせば、それらの命題から別の命題が導けるのかを決めたルールの組を決め、それらのルールを推論規則という。
公理の集合と推論規則の集合の組を公理系と呼ぶ。
Pi は公理である
Pi は、P1,..., Pi-1 から、許された推論規則によって導くことができる
記述の習慣
脚注[脚注の使い方]
出典^ Heath, T.L. (1908). The Thirteen Books of Euclid's Elements. 1. p. 242
^ https://manabitimes.jp/math/1152
^ https://manabitimes.jp/math/1141
^ https://www.try-it.jp/chapters-5621/sections-5861/lessons-5914/
この項目は、数理論理学に関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。
.mw-parser-output .hlist ul,.mw-parser-output .hlist ol{padding-left:0}.mw-parser-output .hlist li,.mw-parser-output .hlist dd,.mw-parser-output .hlist dt{margin-right:0;display:inline-block;white-space:nowrap}.mw-parser-output .hlist dt:after,.mw-parser-output .hlist dd:after,.mw-parser-output .hlist li:after{white-space:normal}.mw-parser-output .hlist li:after,.mw-parser-output .hlist dd:after{content:" ・\a0 ";font-weight:bold}.mw-parser-output .hlist dt:after{content:": "}.mw-parser-output .hlist-pipe dd:after,.mw-parser-output .hlist-pipe li:after{content:" |\a0 ";font-weight:normal}.mw-parser-output .hlist-hyphen dd:after,.mw-parser-output .hlist-hyphen li:after{content:" -\a0 ";font-weight:normal}.mw-parser-output .hlist-comma dd:after,.mw-parser-output .hlist-comma li:after{content:"、";font-weight:normal}.mw-parser-output .hlist-slash dd:after,.mw-parser-output .hlist-slash li:after{content:" /\a0 ";font-weight:normal}.mw-parser-output .hlist dd:last-child:after,.mw-parser-output .hlist dt:last-child:after,.mw-parser-output .hlist li:last-child:after{content:none}.mw-parser-output .hlist dd dd:first-child:before,.mw-parser-output .hlist dd dt:first-child:before,.mw-parser-output .hlist dd li:first-child:before,.mw-parser-output .hlist dt dd:first-child:before,.mw-parser-output .hlist dt dt:first-child:before,.mw-parser-output .hlist dt li:first-child:before,.mw-parser-output .hlist li dd:first-child:before,.mw-parser-output .hlist li dt:first-child:before,.mw-parser-output .hlist li li:first-child:before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child:after,.mw-parser-output .hlist dd dt:last-child:after,.mw-parser-output .hlist dd li:last-child:after,.mw-parser-output .hlist dt dd:last-child:after,.mw-parser-output .hlist dt dt:last-child:after,.mw-parser-output .hlist dt li:last-child:after,.mw-parser-output .hlist li dd:last-child:after,.mw-parser-output .hlist li dt:last-child:after,.mw-parser-output .hlist li li:last-child:after{content:")\a0 ";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li:before{content:" "counter(listitem)" ";white-space:nowrap}.mw-parser-output .hlist dd ol>li:first-child:before,.mw-parser-output .hlist dt ol>li:first-child:before,.mw-parser-output .hlist li ol>li:first-child:before{content:" ("counter(listitem)" "}.mw-parser-output .navbar{display:inline;font-size:75%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}.mw-parser-output .infobox .navbar{font-size:88%}.mw-parser-output .navbox .navbar{display:block;font-size:88%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}
表示
編集