古典論理の意味論がブール代数によって議論できるように，直観主義論理の意味論はハイティング代数によって考えることができる．ハイティング代数とは，冪で閉じている有界束であり，ブール代数もハイティング代数になる．

というわけで結構題材になるハイティング代数だが，巷でハイティング代数に関しての資料が少なかったりするので，自分のために諸々備忘録を残しておく．

Continue reading