Bool型を使った古典命題論理の埋め込み?

昼ごろ起床.昼夜逆転を半回転させるのに成功した.

んで,本題.Coq というか Gallina の if-then-else を使った証明が扱いにくくて悩ましいが,if の後の bool 値は,中身の構造に立ち入らなくても, true だった場合と false だった場合に場合分けしてしまえばそれで済んでしまうということも多いことに気づいた.

そういうと,あれ排中律っぽいが,はてな,ということになる.というのも, Coq は基本的に CC というか,要するに higher-order な直観主義論理をベースにしていると理解している.なので以下の命題を証明することができない(多分).実際,tauto すると弾かれる.

Proposition law_of_excluded_middle :
  forall P : Prop, P \/ ~ P.

けんども,しかし以下の命題は簡単に証明することができるというオチ.

Proposition law_of_excluded_middle_b :
  forall p : bool, orb p (negb p) = true.
Proof.
  intros p ; induction p.
  - simpl.
    reflexivity.
  - simpl.
    reflexivity.
Qed.

なので簡単にいける.これをどう理解したら良いのかよくわからないが,Coq ぐらい表現力のある論理だと,Bool 型を使って古典命題論理が埋め込めるということだろうか? 多分それで良い気がするが,では一階述語論理を内部で形式化しようと思うとどうだろう,とか,疑問は尽きない.Coq というか定理証明支援系自体の論理体系としての性質の研究とかあるんだろうけんども,どういう論文があるのかすらよくわかっていない.今後の課題ということで.