BHK解釈とも言う．というか普通はそう呼ぶ．

直観主義論理の意味づけに用いられる

論理式と論理演算子の意味づけは証明の有無あるいは方法及び存在で解釈される

L. E. J. Brouwer，Heyting，Andrei Kolmogorovが独立に発見したためこう呼ばれる．

論理式A,Bにおいて

A \land B:Aの証明とBの証明が両方あることで証明される

A \lor B: Aの証明とBの証明のどちらか一方さえあるなら証明される

A \to B:Aの証明があればBが証明できるという方法の存在

\forall x.A(x): 任意の対象dをA(d)の証明に変換するような方法の存在

\exists x.A(x): 対象dの構成の仕方とA(d)の証明があるなら証明される

\bot: 証明がない