Automatic Theorem Proving の分野で例題として使われている Dreadbury Mansion という問題があります。そのお屋敷で殺されたアガサおばさんが自殺だったという命題を証明するものです:
Someone who lives in Dreadbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadbury Mansion, and are the only people who live therein. A killer always hates his victim, and is never richer than his victim. Charles hates no one that Aunt Agatha hates. Agatha hates everyone except the butler. The butler hates everyone not richer than Aunt Agatha. The butler hates everyone Aunt Agatha hates. No one hates everyone. Agatha is not the butler. Therefore : Agatha killed herself.
元々の形は "Seventy-five problems for testing automatic theorem provers" で紹介されています。上は TPTP の PUZ001+1 の問題から抜粋しました。
この証明を Coq で書いてみると、1つの疑問が浮かんできます。
Coq 8.4pl4 で確認した以下の証明は排中律を使っています(classical という Axiom を仮定していることに注意)。このためこれは古典論理での証明になっています。果たして、直観主義論理での証明が可能でしょうか?
もし不可能なら、どの公理を少し(admissible に)強めれば直観主義論理での証明が可能になるでしょうか?
Section dreadbury_mansion.
(* problem description *)
Parameter agatha : Type.
Parameter butler : Type.
Parameter charles : Type.
Parameter lives : Type -> Prop.
Parameter hates : Type -> Type -> Prop.
Parameter killed : Type -> Type -> Prop.
Parameter richer : Type -> Type -> Prop.
Axiom pel55_1:
exists X : Type, lives X /\ killed X agatha.
Axiom pel55_2_1:
lives agatha.
Axiom pel55_2_2:
lives butler.
Axiom pel55_2_3:
lives charles.
Axiom pel55_3:
forall X : Type, lives X -> (X = agatha \/ X = butler \/ X = charles).
Axiom pel55_4:
forall X1 X2 : Type, killed X1 X2 -> hates X1 X2.
Axiom pel55_5:
forall X1 X2 : Type, killed X1 X2 -> ~ richer X1 X2.
Axiom pel55_6:
forall X : Type, hates agatha X -> ~ hates charles X.
Axiom pel55_7:
forall X : Type, X <> butler -> hates agatha X.
Axiom pel55_8:
forall X : Type, ~ richer X agatha -> hates butler X.
Axiom pel55_9:
forall X : Type, hates agatha X -> hates butler X.
Axiom pel55_10:
forall X1 : Type, exists X2 : Type, ~ hates X1 X2.
Axiom pel55_11:
agatha <> butler.
Axiom classical:
forall P : Prop, P \/ ~ P.
(* answer *)
Lemma agatha_hates_herself:
hates agatha agatha.
Proof.
apply pel55_7.
apply pel55_11.
Qed.
Lemma charles_does_not_hate_agatha:
~ hates charles agatha.
Proof.
apply pel55_6.
apply agatha_hates_herself.
Qed.
Lemma butler_does_not_hate_himself:
~ hates butler butler.
Proof.
intro H.
cut (exists X : Type, ~ hates butler X).
intro G.
elim G.
intro X.
cut (X = butler \/ X <> butler).
intro F.
destruct F as [F0 | F1].
rewrite F0.
intro E.
apply E.
exact H.
intro E.
apply E.
apply pel55_9.
apply pel55_7.
exact F1.
apply classical.
apply pel55_10.
Qed.
Lemma butler_is_richer_than_agatha:
~ ~ richer butler agatha.
Proof.
intro H.
apply butler_does_not_hate_himself.
apply pel55_8.
exact H.
Qed.
Lemma charles_did_not_kill_agatha:
~ killed charles agatha.
Proof.
intro H.
cut (hates charles agatha).
apply charles_does_not_hate_agatha.
apply pel55_4.
assumption.
Qed.
Lemma butler_did_not_kill_agatha:
~ killed butler agatha.
Proof.
intro H.
cut (~ richer butler agatha).
apply butler_is_richer_than_agatha.
apply pel55_5.
assumption.
Qed.
Theorem agatha_committed_suicide:
killed agatha agatha.
Proof.
elim pel55_1.
intro X.
intro H.
decompose [and] H.
cut (X = agatha \/ X = butler \/ X = charles).
intro G.
destruct G as [G0 | G1].
rewrite G0 in H1.
assumption.
destruct G1 as [G10 | G11].
rewrite G10 in H1.
exfalso.
apply butler_did_not_kill_agatha.
assumption.
rewrite G11 in H1.
exfalso.
apply charles_did_not_kill_agatha.
assumption.
apply pel55_3.
assumption.
Qed.
End dreadbury_mansion.