直観論理とは

Coq は直観論理で許される推論規則で演繹を行う。 直観論理の説明はWikipediaにある。

簡単に説明すると、私達が普通に数学で用いている論理は古典論理で、直観論理は古典論理から排中律を除いたものである。 排中律を除くことで二重否定の除去など、古典論理では証明できるが直観論理では証明できないものがある。 Coq ではClassicalというライブラリを Import すると古典論理を使えるようになる。 詳しい説明は情報科学における論理を読むと良い。

この記事では、直感論理と古典論理の微妙な違いを集めて遊ぼうと思います。

直感論理で示せる命題

二重否定をつける

Lemma PPNN : forall p : Prop, p -> ~~p.
Proof.
  intros.
  intro.
  apply H0.
  trivial.
Qed.

三重否定を否定にする

Lemma NNN : forall p : Prop, ~~~ p -> ~p.
Proof.
  intros.
  intro.
  apply H.
  intro.
  contradiction.
Qed.

対偶の片方

Lemma Cont : forall p q : Prop, (p -> q) -> (~q -> ~p).
Proof.
  intros.
  intro.
  apply H0.
  apply H.
  trivial.
Qed.

古典論理で示せる命題

古典論理で示せる命題と真理値表を用いて恒真になる命題は一致します。(命題論理の完全性と健全性で検索)

排中律を入れる。

Section Classical.
  Axiom classic : forall P : Prop, P \/ ~P.
  (* ここにコードを書く *)
End Classical.

二重否定の除去

Lemma NNPP : forall p : Prop, ~~ p -> p.
Proof.
  intros.
  specialize (classic p).
  intros.
  destruct H0.
  trivial.
  contradiction.
Qed.

対偶のもう片方

Lemma Cont2 : forall p q : Prop, (~p -> ~q) -> (q -> p).
Proof.
  intros.
  specialize (classic p).
  intros.
  destruct H1.
  trivial.
  specialize (H H1).
  contradiction.
Qed.

背理法

apply NNPP; intros.

を実行することは背理法を行うことである。 示すべき命題の否定を仮定に追加して矛盾を導くことだからである。

感想

  • 情報科学における論理にいろいろ書いてあった。
  • Require Import Classical.することで古典論理を扱うことができる。Classical
  • 直感論理を考えることはなんかの役に立つのかな。