論理学において、背理法による証明は、命題が偽であると仮定すると矛盾が生じることを示すことによって命題の真偽または妥当性を確立する証明形式である。数学的証明では自由に使用されているが、数学思想のすべての学派がこの種の非構成的証明を普遍的に妥当であると認めているわけではない。[1]
より広義には、背理法による証明とは、最初の仮定が証明すべき陳述の否定ではない場合でも、矛盾にたどり着くことによって陳述を確立するあらゆる形式の議論のことである。この一般的な意味では、背理法による証明は間接証明、反対を仮定することによる証明、[2]および不可能帰納法としても知られている。[3]
背理法による証明を用いた数学的な証明は、通常次のように進行します。
- 証明すべき命題はPです。
- P が偽であると仮定します。つまり、 ¬Pと仮定します。
- 次に、 ¬P が偽を意味することが示されます。これは通常、相互に矛盾する 2 つの主張Qと¬Q を導き出し、無矛盾律を適用することによって達成されます。
- Pが偽であると仮定すると矛盾が生じるため、 P は実際には真であると結論付けられます。
重要な特殊なケースとして、背理法による存在証明があります。つまり、特定のプロパティを持つオブジェクトが存在することを証明するために、すべてのオブジェクトがそのプロパティの否定を満たすという仮定から矛盾を導き出します。
形式化
この原理は、命題式 ¬¬P ⇒ P、つまり(¬P ⇒ ⊥) ⇒ Pとして正式に表現され、次のように表されます。「P が偽であると仮定すると偽になる場合、Pは真である。」
「が証明されれば、結論付けられる」と書かれています。
シーケント計算では、原理はシーケントによって表現される。
これは、「仮説と は結論またはを導きます。」 と書かれています。
正当化
古典論理では、この原理は命題¬¬P ⇒ Pの真理値表を調べることで正当化され、それがトートロジーであることが証明される。
この原理を正当化する別の方法は、排中律から次のように導くことです。 ¬¬Pを仮定し、 P を証明しようとします。 排中律により、P が成り立つか、そうでないかのどちらかになります。
どちらの場合でも、Pが確立されました。逆に、背理法による証明を使用して排中律を導くことができることがわかります。
古典的なシーケント計算では、LK の背理法による証明は否定の推論規則から導き出されます。
他の証明技術との関係
矛盾による反論
背理法による証明は背理法による反駁に似ており、[4] [5]否定の証明としても知られ、¬Pは次のように証明されると述べています。
- 証明すべき命題は¬Pです。
- Pと仮定します。
- 虚偽を導き出す。
- ¬Pと結論付けます。
対照的に、背理法による証明は次のように進行します。
- 証明すべき命題はPです。
- ¬Pと仮定します。
- 虚偽を導き出す。
- Pと結論付けます。
形式的にはこれらは同じではありません。背理法による反駁は証明すべき命題が否定されている場合にのみ適用されますが、背理法による証明はどのような命題にも適用できます。[6]古典論理では、とが自由に入れ替えられるため、区別はほとんどあいまいです。したがって、数学の実践では、両方の原理は「背理法による証明」と呼ばれます。
排中律
背理法による証明は、アリストテレスによって最初に定式化された排中律と同等であり、主張またはその否定のいずれかが真である、つまりP ∨ ¬P であると述べます。
矛盾律
矛盾律は、アリストテレスによって形而上学的原理として初めて述べられました。これは、命題とその否定が両方とも真であることはできない、または同義語として、命題が真と偽の両方であることはできないと仮定します。正式には矛盾律は¬(P ∧ ¬P)と書かれ、「命題が真と偽の両方であることはない」と読みます。矛盾律は、背理法による証明の原理に従うことも、その原理によって暗示されることもありません。
排中律と無矛盾律を合わせると、Pと¬Pのうち 1 つだけが真であることを意味します。
直観主義論理における背理法による証明
直観主義論理では、背理法による証明は一般的には有効ではありませんが、いくつかの特定の例を導き出すことはできます。対照的に、否定の証明と無矛盾の原理はどちらも直観主義的に有効です。
背理法による証明のブラウワー・ヘイティング・コルモゴロフ解釈は、次のような直観的妥当性条件を与える:命題が偽であることを立証する方法がない場合、命題が真であることを立証する方法が存在する。[明確化]
「方法」をアルゴリズムと解釈すると、条件は受け入れられません。なぜなら、この条件によって停止問題を解決できるからです。それがなぜなのかを知るために、 「チューリングマシンM は停止するか、停止しないか」というステートメントH(M)を考えてみましょう。その否定¬H(M)は、「 M は停止も停止しないでもない」と述べており、これは矛盾律(直観的には有効) によれば誤りです。背理法による証明が直観的に有効であれば、任意のチューリングマシンM が停止するかどうかを決定するアルゴリズムが得られることになり、停止問題の解決不可能性の (直観的には有効な) 証明に違反することになります。
を満たす命題P は、¬¬-安定な命題として知られています。したがって、直観主義論理では背理法による証明は普遍的に有効ではなく、¬¬-安定な命題にのみ適用できます。このような命題の例は決定可能な命題、つまり を満たす命題です。実際、排中律が背理法による証明を意味するという上記の証明は、決定可能な命題が ¬¬-安定であることを示すために再利用できます。決定可能な命題の典型的な例は、「 は素数である」や「 は割り切れる」など、直接計算によって確認できるステートメントです。
背理法による証明の例
ユークリッドの原論
背理法による証明の初期の例としては、ユークリッドの『原論』第1巻第6命題が挙げられる。 [7]
- 三角形において 2 つの角度が等しい場合、等しい角度の反対側の辺もまた互いに等しくなります。
証明は、反対側の辺が等しくないと仮定して進められ、矛盾が導き出されます。
ヒルベルトの無条件条件
影響力のある背理法による証明は、デイヴィト・ヒルベルトによってなされました。彼の 「否定的証明」には次のように記されています。
ヒルベルトはそのような多項式は存在しないと仮定してこの命題を証明し、矛盾を導き出した。[8]
素数の無限
ユークリッドの定理は、素数は無限に存在することを述べている。ユークリッドの『原論』では、この定理は第9巻の命題20に述べられている。[9]
- 素数は、割り当てられた素数の集合よりも多くなります。
上記の文を形式的にどのように書くかによって、通常の証明は背理法による証明か背理法による反証のいずれかの形式をとります。ここでは前者を示します。背理法による反証としてどのように証明が行われるかについては以下を参照してください。
ユークリッドの定理を「すべての自然数にはそれよりも大きい素数が存在する」 と正式に表現すると、次のように背理法による証明が用いられます。
任意の数 が与えられたとき、 より大きい素数が存在することを証明します。逆に、そのようなp は存在しないと仮定します (背理法の応用)。すると、すべての素数は より小さいか等しいので、すべての素数のリストを作成できます。 をすべての素数と の積とします。 はすべての素数より大きいので素数ではなく、したがってそのうちの 1 つ、たとえば で割り切れる必要があります。ここで、 と はどちらも で割り切れるので、それらの差 も割り切れますが、1 はどの素数でも割り切れないため、割り切れません。したがって、矛盾があり、 より大きい素数があります。
矛盾による反論の例
以下の例は一般的に背理法による証明と呼ばれていますが、形式的には背理法による反証を採用しています(したがって直観的に有効です)。[10]
素数の無限
ユークリッドの定理をもう一度見てみましょう。第9巻、命題20:[9]
- 素数は、割り当てられた素数の集合よりも多くなります。
この文は、素数の有限リストごとに、そのリストにない別の素数が存在すると言っていると解釈できます。これは、ユークリッドの元の定式化に近い、同じ精神に基づいたものであると言えます。この場合、ユークリッドの証明は、次のように、1 つのステップで背理法による反駁を適用します。
素数の有限リスト が与えられた場合、このリストにない素数が少なくとも 1 つ追加で存在することが示されます。 を、リストされたすべての素数と の素因数(場合によってはそれ自体)の積とします。は、指定された素数リストに含まれていないと主張します。 逆に、 が含まれていると仮定します (背理法による反証の適用)。 すると、 はと の両方を割り切るため、その差 も割り切れます。 1 を割り切れる素数はないため、これは矛盾を生じます。
2の平方根の無理数
2の平方根が無理数であるという古典的な証明は、背理法による反証である。[11]実際、我々は、比が2の平方根である自然数aとbが存在すると仮定して、否定¬∃a、b∈。a /b = √ 2 を証明しようと試み、矛盾を導いた。
無限降下法による証明
無限降下による証明は、次のように、望ましい特性を持つ最小のオブジェクトが存在しないことを示す証明方法です。
- 望ましい特性を持つ最小のオブジェクトがあると仮定します。
- 望ましい特性を持つさらに小さなオブジェクトが存在することを実証し、それによって矛盾を導き出します。
このような証明もまた、背理法による反証である。典型的な例は、「最小の正の有理数は存在しない」という命題の証明である。最小の正の有理数qが存在すると仮定し、次のことを観察して矛盾を導く。q/2 はqよりもさらに小さく、それでも正です。
ラッセルのパラドックス
ラッセルのパラドックスは、集合論的に「それ自体を含まない集合を要素とする集合は存在しない」と述べられており、通常は背理法による反駁によって証明される否定文である。
表記
背理法による証明は「矛盾!」という言葉で終わることがある。 アイザック・バローとベールマンは、QEDに倣って「 quod est absurdum 」(「これは不合理である」)の略である QEA という表記法を使用したが、この表記法は現在ではほとんど使用されていない。[12]矛盾を表すために時々使用される図記号は、下向きのジグザグ矢印の「稲妻」記号(U+21AF: ↯)であり、例えばデイビーとプリーストリーが使用している。[13] 他に時々使用される記号には、一対の反対向きの矢印([引用が必要]または)、[引用が必要]取り消し線の矢印()、[引用が必要]ハッシュの様式化された形式(U+2A33: ⨳ など)、[引用が必要]または「参照マーク」(U+203B: ※)、[引用が必要]または がある。[14] [15]
ハーディの見解
GHハーディは背理法による証明を「数学者の最も優れた武器の一つ」と表現し、「それはチェスのどの賭けよりもはるかに優れた賭けである。チェスのプレイヤーはポーンや駒さえも犠牲にするかもしれないが、数学者はゲームそのものを犠牲にするのだ」と述べた。[16]
自動定理証明
自動定理証明では、解決方法は背理法による証明に基づいています。つまり、与えられた命題が与えられた仮説によって導かれることを示すために、自動証明器は仮説と命題の否定を仮定し、矛盾を導き出そうとします。[17]
参照
参考文献
- ^ ビショップ、エレット 1967. 構成的分析の基礎、ニューヨーク:アカデミックプレス。ISBN 4-87187-714-0
- ^ 「Proof By Contradiction」www2.edc.org . 2023年6月12日閲覧。
- ^ 「Reductio ad absurdum | 論理」ブリタニカ百科事典。 2019年10月25日閲覧。
- ^ 「背理法による証明」nLab . 2022年10月7日閲覧。
- ^ Richard Hammack、『Book of Proof』、第3版、2022年、ISBN 978-0-9894721-2-8、「第9章:反証」を参照。
- ^ Bauer, Andrej (2010年3月29日). 「否定の証明と背理法による証明」.数学と計算. 2021年10月26日閲覧。
- ^ 「ユークリッド原論、第6巻、命題1」。2022年10月2日閲覧。
- ^ デイヴィッド、ヒルベルト(1893)。「Ueber die vollen Invariantensysteme」。数学アンナレン。42 (3): 313–373。土井:10.1007/BF01444162。
- ^ ab 「ユークリッド原論、第9巻、命題20」。2022年10月2日閲覧。
- ^ Bauer, Andrej (2017). 「構成的数学を受け入れるための5つの段階」アメリカ数学会報54 (3): 481–498. doi : 10.1090/bull/1556 .
- ^ Alfeld, Peter (1996 年 8 月 16 日)。「なぜ 2 の平方根は無理数なのか?」数学を理解するための学習ガイド。ユタ大学数学部。2013年2 月 6 日閲覧。
- ^ 「数学フォーラムのディスカッション」。
- ^ B. Davey および HA Priestley、「Introduction to Lattices and Order」、Cambridge University Press、2002 年。「Notation Index」の 286 ページを参照。
- ^ ゲイリー・ハーディグリー『様相論理入門』第 2 章、pg. II–2。https://web.archive.org/web/20110607061046/http://people.umass.edu/gmhwww/511/pdf/c02.pdf
- ^ 包括的な LaTeX シンボル リスト、20 ページ。http://www.ctan.org/tex-archive/info/symbols/comprehensive/symbols-a4.pdf
- ^ GH Hardy、 『数学者の謝罪』、ケンブリッジ大学出版局、1992年。ISBN 9780521427067。PDF p.19 Archived 2021-02-16 at the Wayback Machine。
- ^ 「線形解決」、From Logic to Logic Programming、MIT Press、pp. 93–120、1994、doi :10.7551/mitpress/3133.003.0007、ISBN 978-0-262-28847-7、 2023年12月21日閲覧
参考文献と外部リンク
- フランクリン、ジェームズ、ダウド、アルバート(2011)。数学の証明:入門。第6章:キュー。ISBN 978-0-646-54509-7。
{{cite book}}: CS1 maint: location (link) - ラリー・W・カシックの「証明の書き方」より、背理法による証明
- Reductio ad Absurdum インターネット哲学百科事典。 ISSN 2161-0002
