2020-11-17 ■ 後期授業第六回目は、直観主義論理のモデルの話です。排中律など直観主義論理で証明できない命題が、直観主義論理で本当に証明できないことを証明するのは大変です。そこで今回は、証明できない命題の「反例モデル」を構成することによって証明不可能性を証明する方法を学びます。この方法は「証明できないことの証明」を非常に楽にします。 この際使われる「クリプキ・モデル」は直観主義論理を提唱したブラウアーの「数学は精神的な構成である」という立場のモデルでもあり、応用範囲も広い、有用なものです。 前回の復習 クリプキ・モデル(命題論理) 健全性と完全性