Brouwer-Heyting-Kolmogorov解釈
BHK解釈とも言う．というか普通はそう呼ぶ．
#証明論
直観主義論理の意味づけに用いられる
論理式と論理演算子の意味づけは証明の有無あるいは方法及び存在で解釈される
L. E. J. Brouwer，Heyting，Andrei Kolmogorovが独立に発見したためこう呼ばれる．
Def
論理式$ 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: 証明がない