>>238

1.論理式ψが古典論理で証明可能で、
　直観主義論理で証明不可能。

2.論理式ψが古典論理で証明可能で、
　直観主義論理に論理式ψを公理
　として加えた論理で、排中律が
　証明可能。

この２条件は同値ではありません。
反例：ψ = (p→q)∨(q→p)

(p→q)∨(q→p)を直観主義論理に公理として加えたら
直観主義論理と古典論理の間に位置する「中間論理」になります。
中間論理は他にもたくさんあります（非可算無限個あります）。
たとえば鹿島亮の数理論理学には中間論理や
「論理式（たとえば(p→q)∨(q→p)）が直観主義論理で証明不可能なこと」
をクリプケモデルを構成して示すことが載っているので、
その辺りを勉強するとよいのでは。