直観主義的論理では$P \lor \lnot P$は一般には成り立たないというのはよく知られていますが、これは$P \lor \lnot P$に反例があるという意味ではありません。
ただし、「直観主義的論理においても命題の真偽が定まらないことはない」ことは言えます。
これに関して、古典論理的な命題を直観主義的論理の中で理解する方法を説明した上で、古典論理的な排中律が直観主義的論理の中で成り立つことを示します。
直観主義的論理の中で$P \lor Q$という命題は「$P$または$Q$」と読まれますが、これは古典論理の意味の「$P$または$Q$」よりも強い（あるいは狭い）意味を持ちます。
直観主義的論理の中で$P \lor Q$の証明を与える場合、その証明を読めば$P$が成り立つのか$Q$が成り立つのかが明らかになっていなくてはなりません。これは選言特性として知られています。
この事実を象徴するのが直観主義的論理におけるド・モルガンの法則です。
以下の命題は直観主義的論理においても常に成り立ちます。
しかし、$\lnot (P \land Q) \implies \lnot P \lor \lnot Q$は直観主義的論理においては必ずしも成り立つとは限りません。
これは$P \land Q$が成り立つと仮定して矛盾が生じたとしても、$\lnot P$と$\lnot Q$のどちらが成り立つのかが分からない、すなわち選言特性を言えないからです。
ただし、結論を二重否定した命題
$$ \lnot (P \land Q) \implies \lnot\lnot(\lnot P \lor \lnot Q) $$
は直観主義的論理においても成り立ちます。
$\lnot\lnot X$というのは、「$X$が成り立たないということはない」という意味で、これは$X$が反証不可能であることを指し示しています。
古典論理は結局のところ、"反証不可能性まで"の論理です。
何らかの命題$P$が真であることを示すには、$P$に反例がないことを示せば十分であるというのが古典論理の考え方です。
一方で、直観主義的論理で何らかの命題$P$が真であることを示すには、その証明を実際に構成して見せなければなりません。つまり、選言特性や存在特性を保ったまま、実証して見せるということです。
ここでは、"選言特性や存在特性を保ったまま"証明できるという意味で、これを構成的に実証可能と言うことにします。（今回の説明のために導入する便宜的な用語であり、他で通用する一般的な用語では無いことを断っておきます。）
さて、上記の意味での「反証不可能性」と「実証可能性」が重要なキーワードになります。
古典論理は実証可能性に頓着しません。
しかし、直観主義的論理では反証不可能性と実証可能性の違いを区別します。それは否定$\lnot$の数によって判別できます。
直観主義的論理ではデフォルトで実証可能性を議論するので、「$P$が成り立つ」ことを示せば実証可能性を示したことになります。
直観主義的論理の中で「$P$は反証不可能である」を示すには、その二重否定を考えればよいです。つまり、「$\lnot \lnot P$が成り立つ」を示せばよいです。
以上の観察から、直観主義的論理の中で古典論理的に命題を考えたいときは、その二重否定を考えれば良いことが窺い知れます。
このように理解すると、直観主義的論理において二重否定の除去規則$\lnot \lnot P \implies P$が必ずしも成り立たないことに納得が行くと思います。
$P$が反証不可能であったとしても、$P$が実証可能であるとは限りません。
一方で、二重否定の導入規則$P \implies \lnot \lnot P$は常に成り立ちます。
$P$が実証可能であれば、$P$は常に反証不可能です。
なお、$\lnot P$と$\lnot\lnot\lnot P$は同値です。
なぜならば、直観主義的論理において$\lnot P$の成立を示すとき、$P$が実証可能であることを仮定して矛盾を導けば十分だからです。この意味で、$\lnot P$の実証可能性と反証不可能性は同値です。
古典論理における命題$P \lor Q$を、直観主義的論理の中で解釈してみましょう。
これは『「$P$は反証不可能である」または「$Q$は反証不可能である」』は反証不可能であると解釈できます。
したがって、直観主義的論理の中では$\lnot \lnot (\lnot \lnot P \lor \lnot \lnot Q)$で表せます。
これは$\lnot\lnot(P \lor Q)$と同値です。
$$ \lnot \lnot (\lnot \lnot P \lor \lnot \lnot Q) \iff \lnot\lnot(P \lor Q) $$
$$ \lnot \lnot (\lnot \lnot P \lor \lnot \lnot Q) \iff \lnot \lnot \lnot (\lnot P \land \lnot Q) \iff \lnot \lnot \lnot \lnot (P \lor Q) \iff \lnot \lnot (P \lor Q) \space\square $$
したがって、古典論理の意味での「$P \lor Q$」（この$\lor$は選言特性を尊重しない）は、直観主義的論理の中で「$P \lor Q$は反証不可能である」（この$\lor$は選言特性を尊重する）と同値であると言えるでしょう。
選言特性や反証不可能性を考えると、直観主義的論理における排中律$P \lor \lnot P$は、古典論理におけるそれと比べると主張が強すぎることが分かります。
「$P$か$\lnot P$のどちらが成り立つか分かる」という主張をする気が古典論理にはそもそも無いからです。古典論理が言いたいのは反証不可能性までであって、直観主義的論理に付き合って選言特性を尊重する義理はありません。
では、排中律を反証不可能性の観点から理解するとどうなるでしょうか。
古典論理における排中律$P \lor \lnot P$を直観主義的論理の中で解釈すると、それは先ほど示した通り、$\lnot \lnot (P \lor \lnot P)$と同値になります。
最後に、直観主義的論理では$P \lor \lnot P$は反証不可能です。
$$ \lnot \lnot (P \lor \lnot P) $$
$\lnot (P \lor \lnot P)$が成り立つ (A)と仮定して矛盾を導けばよい。
矛盾を導くために、(A)の仮定の下で$P \lor \lnot P$が成り立つ (B)ことを示す。
$\lnot P$が成り立つことを示すため、$P$が成り立つと仮定する。
これは(A)に矛盾する。したがって(A)の仮定の下で$\lnot P$が成り立つ。
つまり、(A)の仮定の下で(B)が成り立つことになるが、これは矛盾である。
よって$\lnot \lnot (P \lor \lnot P)$が成り立つ。$\square$
つまり、直観主義的論理においては$P \lor \lnot P$は構成的に実証可能とは限りませんが、少なくとも反証不可能であることは言えます。
反例はあり得ません。直観主義的論理においても$\lnot (P \lor \lnot P)$を仮定すれば矛盾します。
また、以上の観察から分かる通り、直観主義的論理で古典論理を展開するために排中律を無条件に仮定する必要は全くなく、単に直観主義的論理の中でその反証不可能性を示せば良いだけということも窺い知れます。
ここで示した事実は、『任意の命題$P$について「$P\lor\lnot P$は反証不可能である」』ということだけです。
『「任意の命題$P$について$P\lor\lnot P$が成り立つ」が反証不可能である』を示したわけではありません。
直観主義で排中律に反例が与えられるとすれば、それは後者に対する反例です。