Интуиционистская логика - фейк

[kotenok gav]

Давайте запишем доказательство на формальном языке, что ли.

Лемма 1. $\sqrt2^{\sqrt2}\in Q\Rightarrow\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q$
Доказательство: Известно, что $\sqrt2\not\in Q$.
$\sqrt2\not\in Q\wedge\sqrt2^{\sqrt2}\in Q\Rightarrow\sqrt2\not\in Q\wedge\sqrt2\not\in Q\wedge\sqrt2^{\sqrt2}\in Q$. По правилу вывода $(X,X\Rightarrow Y)\Rightarrow Y$ $\sqrt2\not\in Q\wedge\sqrt2\not\in Q\wedge\sqrt2^{\sqrt2}\in Q$. По правилу вывода $X(q, w, e,\ldots)\Rightarrow\exists f, g, h, \ldots: X(f, g, h, \ldots)$ $\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q$.

Лемма 2. $\sqrt2^{\sqrt2}\not\in Q\Rightarrow\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q$
Доказательство: Известно, что $\sqrt2\not\in Q$, $\left(\sqrt2^{\sqrt2}\right)^{\sqrt2}=2$, и $2\in Q$.
$\sqrt2\not\in Q\wedge\sqrt2^{\sqrt2}\not\in Q\wedge\left(\sqrt2^{\sqrt2}\right)^{\sqrt2}=2\wedge2\in Q\Rightarrow\sqrt2^{\sqrt2}\not\in Q\wedge\sqrt2\not\in Q\wedge\left(\sqrt2^{\sqrt2}\right)^{\sqrt2}\in Q$. По правилу вывода $(X,X\Rightarrow Y)\Rightarrow Y$ $\sqrt2^{\sqrt2}\not\in Q\wedge\sqrt2\not\in Q\wedge\left(\sqrt2^{\sqrt2}\right)^{\sqrt2}\in Q$. По правилу вывода $P(q, w, e,\ldots)\Rightarrow\exists f, g, h, \ldots: P(f, g, h, \ldots)$ $\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q$.

Теорема. $\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q$.
Доказательство: По правилу вывода $((X\Rightarrow Y)\wedge(\neg X\Rightarrow Y))\Rightarrow Y$ (следствию закона исключённого третьего), $((\sqrt2^{\sqrt2}\in Q\Rightarrow\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q)\wedge(\sqrt2^{\sqrt2}\not\in Q\Rightarrow\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q))\Rightarrow(\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q)$. По правилу вывода $(X,X\Rightarrow Y)\Rightarrow Y$ и леммам 1 и 2, $\exists a,b:a\not\in Q\wedge b\not\in Q\wedge a^b\in Q$.

Это было непросто написать, да.

[пианист]

К написанному уважаемым kotenok gav можно добавить еще следующее:

Urrod в сообщении #1551480 писал(а):

То есть,автор данного примера намекает на то, что закон исключенного третьего не работает, так как если его не нарушать и доказывать что-либо от обратного, то можно доказать даже то, что возможно не истинно

вовсе нет, утверждение вполне себе истинно, есть и доказательство, не использующее закон исключенного третьего. Только с законом исключенного третьего доказательство элементарное и очень простое, а если без, все наоборот, теорема Гельфонда-Шнайдера etc.
Также хочу заметить, что интуиционистская логика является в определенном смысле естественным объектом, в отличие от классической. Это можно наблюдать, например, в изоморфизме Карри-Говарда.