スマリヤン先生の著書『Godel's Incompleteness Theorems』の冒頭に、不完全性定理を背景としたちょっとした論理パズルがあります。それを紹介するとともにCoqで形式化して証明してみます。
論理パズルの内容
プリンタと印字: ここに一台のプリンタがあります。プリンタは時々刻々と「表現」を印字し続けます。表現とは5種類の記号――つまりP,N,(,),~――の有限列です。例えば 時刻0 に PPN)(~ を印字し、時刻1 に NPP) を印字するといった具合です。プリンタは同じ表現を重複して印字することもあります。印字を止めることはありません。
文という表現: 特定の4つのパターンに属する表現を文と呼びましょう。パターンは P(e), PN(e), ~P(e), ~PN(e) です。 e の部分は任意の表現が入ります。例えば以下はすべて文です: P(~~), P(P), PN(~(), ~PN(PP()P)
文のBool値: プリンタの動作に基づいて文にBool値を割り当てます。
-
P(e)が true ⇔ いつかeを印字する -
~P(e)が true ⇔eを絶対に印字しない -
PN(e)が true ⇔ いつかe(e)を印字する -
~PN(e)が true ⇔e(e)を絶対に印字しない
すべての表現が文というわけではないので、すべての表現にBool値を割り当てることはできません。ある特定の文がtrueであることを確かめるには根気よくプリンタの出力をながめて、その文が印字されるのを待っていればよいです。ある特定の文が false であることを確かめるのは難しい問題です。
かしこいプリンタ: これまでは任意なプリンタを想定していましたが、これからは「かしこい」プリンタを想定しましょう。このプリンタは「文を印字するならそれは全てtrueである」⇔「falseとなる文は絶対に印字しない」という自身の挙動を考慮しながら印字します。例えば P(~~~) を印字したら、過去か未来かに ~~~ を印字します（逆は必ずしも成立しません）。同様に PN(~P~) を印字したら、過去か未来かに ~P~(~P~) を印字します。
ここで問題: すべての true な文を印字するような、かしこいプリンタはあるでしょうか？それとも、どんなかしこいプリンタであっても印字できない trueな文はあるのでしょうか？
答え: 答えは後者です。どんなにかしこいプリンタを選んでも ~PN(~PN) という文G はtrueだけれども印字できません。なぜか？Gを印字すると仮定しましょう。するとプリンタのかしこさから、この文はtrueでなければなりませんが、それはすなわち ~PN(~PN) すなわち G を絶対に印字しないことを意味します。したがって矛盾です。よって印字はできないのです。そして ~PN(~PN)が印字できないという事実は、この文が true であることを意味します。
Coq での証明
Require Import Bool List.
Import ListNotations.
Section GoedelPuzzle1.
Inductive gsym := | P | N | RP | LP | Neg.
Definition gexp := list gsym.
Definition printer:= nat -> gexp.
Definition Printable (p:printer) (e:gexp) := exists n, p n = e.
Inductive evalR (p:printer) (s:gexp): bool->Prop :=
| tP1 : forall e, s = [P;LP]++e++[RP] -> Printable p e -> evalR p s true
| tP2 : forall e, s = [P;LP]++e++[RP] -> ~Printable p e -> evalR p s false
| tPN1 : forall e, s = [P;N;LP]++e++[RP] -> Printable p (e++LP::e++[RP]) -> evalR p s true
| tPN2 : forall e, s = [P;N;LP]++e++[RP] -> ~Printable p (e++LP::e++[RP]) -> evalR p s false
| tnP1 : forall e, s = [Neg;P;LP]++e++[RP] -> Printable p e -> evalR p s false
| tnP2 : forall e, s = [Neg;P;LP]++e++[RP] -> ~Printable p e -> evalR p s true
| tnPN1: forall e, s = [Neg;P;N;LP]++e++[RP] -> Printable p (e++LP::e++[RP]) -> evalR p s false
| tnPN2: forall e, s = [Neg;P;N;LP]++e++[RP] -> ~Printable p (e++LP::e++[RP]) -> evalR p s true
.
Definition correct_printer p := forall n, ~evalR p (p n) false.
Definition G:= [Neg;P;N;LP;Neg;P;N;RP].
Lemma G_true_unprintable: forall p,
correct_printer p -> ~Printable p G /\ evalR p G true.
Proof. split;intros.
- intros H0. case H0;intros. destruct (H x). rewrite H1.
change G with ([Neg;P;N;LP]++[Neg;P;N]++[RP]).
eapply tnPN1. reflexivity. simpl. assumption.
- change G with ([Neg;P;N;LP]++[Neg;P;N]++[RP]).
eapply tnPN2. reflexivity. simpl. fold G. intro.
case H0; intros. specialize (H x). rewrite H1 in H. destruct H.
change G with ([Neg;P;N;LP]++[Neg;P;N]++[RP]).
eapply tnPN1. reflexivity. simpl. fold G. assumption.
Qed.
Theorem printer_imcompleteness: forall p,
correct_printer p -> exists s, ~Printable p s /\ evalR p s true.
Proof. intros. exists G. now apply G_true_unprintable. Qed.
End GoedelPuzzle1.
何のアナロジー？
- プリンタ → 証明系による定理の枚挙
-
P(e)→ eをゲーデル数とする論理式 f が証明できるという述語 -
~PN(~PN)→ ゲーデル文「私は証明できない」
補足
~PN(~PN) がtrueなので PN(~PN) はfalseとなり、つまり印字されません。Negを否定と読むと、 PN(~PN) と ~PN(~PN) との両方が印字されないので決定不能命題を構成したことに対応します。
Definition G0 := [P;N;LP;Neg;P;N;RP].
Lemma aux: forall p e,
correct_printer p ->
evalR p (Neg::e) true ->
evalR p e false.
Proof. intros. inversion H0; try discriminate.
inversion H1;subst. eapply tP2. reflexivity. trivial.
inversion H1;subst. eapply tPN2. reflexivity. trivial. Qed.
Lemma G_implies_undecidability: forall p,
correct_printer p -> ~Printable p G0 /\ ~Printable p (Neg::G0).
Proof. intros;pose proof (G_true_unprintable p) as H1;split.
- apply H1 in H as H'. destruct H' as [_ H'].
intros H0. case H0;intros. destruct (H x). apply aux. trivial. rewrite H2. assumption.
- apply H1 in H. destruct H. assumption.
Qed.
もう一つの論理パズル
ゲーデル数化を組み込んだより本質に近づいたバージョンのパズルも掲載されています。Coqで紹介します:
Require Import Bool List.
Import ListNotations.
Section GoedelPuzzle2.
Inductive gsym := | P | N | A | B | Neg.
Definition gexp := list gsym.
Fixpoint encode s := match s with
| [] => []
| a::s' => let c := match a with
| Neg =>[A;B]
| P => [A;B;B]
| N => [A;B;B;B]
| A => [A;B;B;B;B]
| B => [A;B;B;B;B;B]
end in c ++ (encode s')
end.
Fixpoint decode (s:gexp): gexp := match s with
| [] => []
| A::B::B::B::B::B::s' => B:: (decode s')
| A::B::B::B::B::s' => A:: (decode s')
| A::B::B::B::s' => N:: (decode s')
| A::B::B::s' => P:: (decode s')
| A::B::s' => Neg:: (decode s')
| _ => []
end.
Definition printer:= nat -> gexp.
Definition Printable (p:printer) (e:gexp) := exists n, p n = e.
Inductive nexp: list gsym ->Prop :=
| na: nexp [A]
| nb: nexp [B]
| nca s : nexp s -> nexp (A::s)
| ncb s : nexp s -> nexp (B::s).
Inductive evalR p s: bool->Prop:=
| ep1: forall e, s=[P]++e -> nexp e -> decode e <> [] -> Printable p (decode e) -> evalR p s true
| ep2: forall e, s=[P]++e -> nexp e -> decode e <> [] -> ~Printable p (decode e) -> evalR p s false
| ep3: forall e, s=[Neg;P]++e -> nexp e -> decode e <> [] -> Printable p (decode e) -> evalR p s false
| ep4: forall e, s=[Neg;P]++e -> nexp e -> decode e <> [] -> ~Printable p (decode e) -> evalR p s true
| enp1: forall e, s=[P;N]++e -> nexp e -> decode e <> [] -> Printable p ((decode e)++e) -> evalR p s true
| enp2: forall e, s=[P;N]++e -> nexp e -> decode e <> [] -> ~Printable p ((decode e)++e) -> evalR p s false
| enp3: forall e, s=[Neg;P;N]++e -> nexp e -> decode e <> [] -> Printable p ((decode e)++e) -> evalR p s false
| enp4: forall e, s=[Neg;P;N]++e -> nexp e -> decode e <> [] -> ~Printable p ((decode e)++e) -> evalR p s true
.
Definition correct_printer p := forall n, ~evalR p (p n) false.
Definition G:= [Neg;P;N;A;B;A;B;B;A;B;B;B].
Lemma G_true_unprintable: forall p,
correct_printer p -> ~Printable p G /\ evalR p G true.
Proof. split;intros.
- intros H0. case H0;intros. destruct (H x). rewrite H1.
change G with ([Neg;P;N]++[A;B;A;B;B;A;B;B;B]).
eapply enp3. reflexivity. repeat constructor. discriminate. simpl. assumption.
- change G with ([Neg;P;N]++[A;B;A;B;B;A;B;B;B]).
eapply enp4. reflexivity. repeat constructor. discriminate. simpl. intro.
case H0; intros. specialize (H x). rewrite H1 in H. destruct H.
change G with ([Neg;P;N]++[A;B;A;B;B;A;B;B;B]).
eapply enp3. reflexivity. repeat constructor. discriminate. assumption. Qed.
Theorem printer_imcompleteness: forall p,
correct_printer p -> exists s, ~Printable p s /\ evalR p s true.
Proof. intros. exists G. now apply G_true_unprintable. Qed.
(* some check *)
Fact encode_starts_with_a: forall a s, exists s', encode (a::s) = A::s'.
Proof. intros. destruct a;simpl.
exists (B::B::encode s); reflexivity.
exists (B::B::B::encode s); reflexivity.
exists (B::B::B::B::encode s); reflexivity.
exists (B::B::B::B::B::encode s); reflexivity.
exists (B::encode s); reflexivity. Qed.
Lemma enc_dec_ident: forall e, decode (encode e) = e.
Proof. induction e as [|a [|b ]]. trivial. destruct a; trivial.
pose proof (encode_starts_with_a b l) as H. destruct H.
rewrite H in IHe. simpl in H.
destruct a; simpl; rewrite H; f_equal; assumption. Qed.
End GoedelPuzzle2.