背理法と排中律（下記）

https://ja.wikipedia.org/wiki/%E6%8E%92%E4%B8%AD%E5%BE%8B
排中律（英: Law of excluded middle、仏: Principe du tiers exclu）とは、論理学において、任意の命題 P に対し「P であるか、または P でない」という命題は常に成り立つという原理である。
直観主義論理においては排中律は公理として採用されておらず、また排中律は直観主義論理の定理ではない（すなわち、排中律は直観主義論理において証明できない）。ただし、排中律の二重否定 ¬¬(P ∨ ¬P) [注釈 1]や三重否定除去 ¬¬¬P → ¬P [注釈 2]などは直観主義論理においても証明可能であり、すなわち排中律が否定されているわけでもない。

例
排中律に依存した論証の例を次に示す。これは、よく知られた例である[7][8]。
『a と b ２つの無理数からなるabが有理数となる a 、 bが存在する』
√2 が無理数であることは知られている。そこで、次のような数を考える。
√2^√2
排中律に基づくと、明らかにこの数は有理数か無理数かのどちらかである。これが有理数なら証明が完了する。もし無理数なら、次のような数を考える。
a=√2^√2
および
b=√2
すると、
a^b=(√2^√2)^√2
=(√2)^(√2・√2)
=(√2)^2
=2
2 は明らかに有理数である。従って証明が完了する。
この論証において、「この数（√2^√2）は有理数か無理数かのどちらかである」という主張は排中律に基づいている。直観主義では、aが
√2であるのか
√2^√2 であるのか特定されていないような上記の論法、あるいは
√2^√2 について何らかの証拠（数・実数としての存在可能性、あるいは有理数であるか無理数であるかといった具体的な証明）がない限り、このような主張を認めない。この変形として、ある数が無理数（あるいは有理数）であることの証明や、ある数が有理数かどうかを判定する有限なアルゴリズムなどが考えられる。

無限に関する非構成的証明
上記の例は直観主義では許されない「非構成的; non-constructive」証明の例である。
「この証明は、定理を満足する a と b という数を特定せずに可能性だけで論じているため、非構成的である。実際には
a=√2^√2 は無理数だが[注釈 3]、これを簡単に示す証明は知られていない」(Davis 2000:220)　
（なお、上記の設題に関して別の数を用いれば、特定の構成的な証明を行うのは困難な事ではない。例えば
a=√2 及び
b=log2 (9)
は共に無理数であることは容易に証明でき、
a^b=3。これは直感主義で認められる証明方法の１つである[9]。）

Davis は「構成的」について「実際に一定の条件を満たす数学的実体が存在するという証明は、明示的に問題の実体を表す方法を提供する必要があるだろう」(p. 85) としている。そのような証明は全体の完全性の存在を前提としており、それは直観主義者にとっては、決して完全ではない「無限」に拡張することは許されない

つづく