ド・モルガンの法則

自然演繹て、少しも”自然”じゃないよな、と。

形式主義vs直観主義。これで本気で喧嘩できる情熱すごい。

数学の哲学において、直観主義（ちょっかんしゅぎ、英: Intuitionism）とは、数学の基礎を数学者の直観におく立場のことを指す。

数学的概念とは数学者の精神の産物であり、その存在はその構成によって示されるべきだという立場から、無限集合において背理法によって非存在の矛盾から存在を示す証明を認めなかった。それゆえ、無限集合において「排中律」、すなわちある命題は真であるか偽であるかのどちらかであるという推論法則を捨てるべきだと主張し、ヒルベルトとの間に有名な論争を引き起こした。ヒルベルトの形式主義は、直接的にはブラウワーからの批判的主張に対し排中律を守り、数学の無矛盾性を示すためのものと考えることができる[1]。

ウィキペディア

ド・モルガンの法則を形式的にやると下のようになります。多分。

正直に言うと、人の感覚に反しているようで気持ちが悪い。そんな風に推論する人はいないだろうと。

[A](仮定)
A∨B(∨導入)
¬(A∨B)(仮定)
⊥(排中律)
¬A(背理法)
[B](仮定)
A∨B(∨導入)
¬(A∨B)(仮定)
⊥(排中律)
¬B(背理法)
¬A∧¬B(∧導入)
¬(A∨B)→¬A∧¬B(→導入)

[A∧B](仮定)
[¬A](仮定)
A(∧除去)
⊥(排中律)
¬A→⊥(→導入)
[¬B](仮定)
B(∧除去)
⊥(排中律)
¬B →⊥(→導入)
[¬A ∨¬B=¬(A∧B)](仮定)
⊥(∨除去)
¬(A∧B)(背理法)
¬A∨¬B →¬(A∧B )(→導入)

¬A∧¬B(仮定)
[A](仮定)
¬A(∧除去)
⊥(排中律)
A→⊥(→導入)
[B] (仮定)
¬B(∧除去)
⊥(排中律)
B→⊥(→導入)
[A∨B](仮定)
⊥(∨除去)
¬(A∨B)(⊥除去)
¬A∧¬B→¬(A∨B)(→導入)

下の方がむしろ”自然に”感じます

(A∪B)^c
(A^c∩B^c)
(A∪B)^c⊂(A^c∩B^c)

口語に直すと「『AまたはB』ではない状態。つまり、Aだけであることはあるし、Bだけであることもある。ただし、その両方であることはあり得ない。よって、Aであり、かつBである」
形式的には強引かもしれませんが僕の感覚では自然。

(A^c∩B^c)
x∉A∧x∉B
x∉(A∨B)
(A∪B)^c

二行目から三行目の変換が強引な感じ否めないので補足。

「Aではい、かつBではない」という主張は、「AまたはBではない」という主張に直接変換できるような気がします。

ブラウワーは、数学的概念とは数学者の精神の産物であり、その存在はその構成によって示されるべきだという立場から、無限集合において背理法によって非存在の矛盾から存在を示す証明を認めなかった。それゆえ、無限集合において「排中律」、すなわちある命題は真であるか偽であるかのどちらかであるという推論法則を捨てるべきだと主張し、ヒルベルトとの間に有名な論争を引き起こした。

ブラウワーは「AであるかAでないかが分からない場合もある」を説明する例として、「円周率の無限小数の中に0が100個続く部分があるかどうか分からない」というものをあげていた。

ある学会でブラウワーがこの話をしたとき、「しかし神なら100個続く部分があるかどうか分かるのでは？」という質問を受けたが、ブラウワーはそれに対し「残念ながら我々は神と交信する方法を知りません」と答えた。

ウィキペディア