メタ論理における論理をCoqでコードにしてみた

「そもそも論理とは何か？」に関する 哲学のような本を読んで刺激を受けたので、Coqに落とし込んで明確化しました。興味を持つ人は非常に限られているとは思いますが共有します。

参考書:

• 本橋『新・論理考究』幻冬舎

はじめに

論理学では、対象を記述するための対象言語を厳密に定めます。一方、帰結関係や推論規則といった命題同士の関係は 対象言語の外から論じます。論じる手段をメタ言語といい、多くの場合日本語などの自然言語で展開されます。

この観点からみると「推論とは何か？」「推論の正しさはどうやって決まるのか？」という問いは、メタ言語における規則・秩序に関する問いであり、 メタ言語を支える論理 に繋がります。

この問いは、通常意識されることはありません。例えば「P, P->Q から Q を導くのは正しい推論だ」というメタな言明は、予め作成された推論規則のリストに記載されているから正しいのであって、それ以上でもそれ以下でもありません。それでも推論や証明を実行できますし、困ることもありません。ただ「リストに載る資格とは何か？リストに載っている規則に共通する性質とは何か？」は手つかずのままです。

というわけで、論理を論理たらしめている秩序は何か？その秩序はどのような体系をなすか？ に対して正面からぶつかるのは刺激的な課題というわけです。

アウトライン

冒頭の参考書の第一章前半をCoqに落とし込んで理解しました。第一章の前半は文の内部構造に踏み込まないため比較的理解しやすく、またコンパクトにまとまるので、Coqに落とし込みやすいです。

議論の概要を示します:

• 論理とは 文集合と文との二項関係である
• ただし、それだけで論理とは言わない。「論理として働く」という性質を持たねばならない
  • すなわち根拠型を持たねばならない
• 論理の具体例は、根拠関係「文集合Γ は 文φの根拠になる」だ
  • 数理論理学における論理的帰結関係をより一般化したもの
• よって正しい根拠関係とは、それが論理として働いているか？というテストにパスしたものだ、というように応えることができる
• それでは「仮定Γから 結論φを導いてよい」という推論に対して正しさを与えるものは何であろうか？
  • 根拠関係における「論理として働く」のような判定基準はあるだろうか？
• 言語論的に、根拠関係と推論関係は密接な繋がりがある。この繋がりを明確化することで、根拠関係と推論関係とは相互変換できる。
• 上記の原理をつかって、推論関係の正しさを、それに対応する根拠関係の正しさに還元することで、「正しい推論とは何か？」に対する判定基準を立てることができる（推論定理）
• 上記の判定基準に則って正しい推論を作ることで、数理論理学を構築できる

コメント付きコード

参考書は全て日本語で書かれており、数式すら登場しないので、コードの文責は完全に私にあります。疑問や指摘は歓迎です。

Section metalogic.

From Coq Require Import Setoid. (*iff に reflexivity/rewrite できるようにインポートしておく*)

(* 基本的な型の定義 *)
Variable sentence human: Type. (* 文と人を基本型として要請する *)
Definition sentences := sentence->Prop. (* 文集合にエイリアスを付ける *)
Definition confirm := human->sentence->Prop. (* 個々の文を個々の人が正否の判断をする。その関係の型 *)
Definition logic := sentences->sentence->Prop. (* 論理の型(後述) *)
Inductive contractF:Type := contractF_of: logic->contractF. (* logicを定める約束の型(後述) *)
Definition inference := (sentences*sentence)%type. (* 推論の型。便宜的に直積としたが必須ではない *)
Inductive contractD := contractD_of: (inference->Prop)->contractD. (* 推論を定める約束の型 *)
(* 上記の型に関連するユーティリティ *)
Definition logic_of cf := match cf with contractF_of x => x end. (* Fな約束からlogicを取り出す手続き *)
Definition inference_of cd := match cd with contractD_of x => x end. (* Dな約束から推論の集合を取り出す手続き *)
(* 約束Fと約束Dに関する等値性の定義。外延が等しければ同じ約束とみなす *)
Definition eq_cf (cf cf':contractF) := forall pre con, (logic_of cf) pre con <-> (logic_of cf') pre con.
Definition eq_cd (cd cd':contractD) := forall s, (inference_of cd) s <-> (inference_of cd') s.

(* 論理とは sentences->sentence->Prop な関係であるが
     そのような関係すべてを論理と呼ぶことはない。それが論理と呼ばれるのは
    その関係が強制力を持った存在として働いているときである。つまり
 『その関係が成立し,  かつその関係の第一項である文集合の全てを正と判断するような
  個人は必ず 第二項である文を正と判断することになる』 そのような時である
  このような状況を表す型を 論理として働く型と呼ぶ *)
Inductive logical (R:logic): Type :=
  gl_intro: forall pre con,
    R pre con -> (forall (c:confirm) (h:human), (forall s, pre s -> c h s) -> c h con)
    -> logical R.

(* 論理の一例として根拠関係「・は・の根拠である」がある（むしろ 根拠関係を一般化したものこそが論理である）。
    まず 根拠型を定義する。教科書より引用:
     > 約束事Fで決まる「根拠となる」という関係が、幾つかの文と1つの文の間で
     > 成り立つことが確認され、さらに、その幾つかの文を全部正しいと認めた時は
     > 常に、その1つの文も正しいと認めざるを得なくなる。
    すると、以下の根拠定理が成立し、論理の一例であることが確かめられる:
     >『Fで決まる関係「根拠になる」が論理として機能する』⇔『Fが根拠型を満たす』 *)
Inductive reasonF (cf:contractF):Type :=
  rf_intro: forall pre con,
    (logic_of cf) pre con -> (forall (c:confirm) h, (forall s, pre s -> c h s) -> c h con)
    -> reasonF cf.
Theorem reasonF_logical: forall cf (_:reasonF cf), logical (logic_of cf).
Proof. intros. inversion X. econstructor. eassumption. assumption. Qed.
Theorem logical_reasonF: forall l:logic, logical l -> reasonF (contractF_of l).
Proof. intros. inversion X. econstructor. eassumption. assumption. Qed.

(* 続いて推論型の定義。教科書より引用:
    > 約束事Dで決まる「正しい推論」になることが確認され、その推論の仮定を
    > 全部正しいと認めた時は、常に、結論も正しいと認めざるを得なくなる。*)
Inductive reasonD (cd:contractD):Type :=
  | rd_intro : forall (s:inference),
    (inference_of cd) s ->
    (forall (c:confirm) h, (forall p, (fst s) p -> c h p) -> c h (snd s)) ->
    reasonD cd.

(* 根拠型と推論型には言語使用上 暗黙のつながり(変換公式)がある。つまり:
    > 1.『推論sが約束Dで決まる「正しい推論」になる』
            ⇔『sの仮定と結論の間に約束Fで決まる「根拠となる」という関係が成り立つ』
     > 2. 『文集合pと文qの間に約束Fで決まる「根拠となる」という関係が成り立つ』
            ⇔『pを仮定, qを結論とする推論が、約束Dで決まる「正しい推論」になる
    別の言い方をすれば、約束Fと約束Dになんらかの相互変換手続きが存在する。
    変換手続きを「*」で表すと変換手続きに関して、上記公式から以下の仕様が要求される:
     > 1'.『推論sが約束F*で決まる「正しい推論」になる』
          ⇔『sの仮定と結論の間に約束Fで決まる「根拠となる」という関係が成り立つ』
     > 2'. 『文集合pと文qの間に約束D*で決まる「根拠となる」という関係が成り立つ』
          ⇔『pを仮定, qを結論とする推論が、約束Dで決まる「正しい推論」になる *)

(* 変換手続きの仕様 *)
Definition f2d_spec (xf: contractF->contractD) :=
  forall cf (s:inference) , inference_of (xf cf) s <-> logic_of cf (fst s) (snd s).
Definition d2f_spec (xf: contractD->contractF) :=
  forall cd p q, logic_of (xf cd) p q <->  inference_of cd (p,q).
(* 変換手続きの実装 *)
Definition contractDbyF (cf: contractF): contractD :=
  contractD_of (fun (s:inference) => logic_of cf (fst s) (snd s)).
Definition contractFbyD (cd: contractD): contractF :=
  contractF_of (fun pre con => inference_of cd (pre, con)).
(* 仕様を満たしていることの確認 *)
Theorem impl_is_correct1: f2d_spec contractDbyF.
Proof. unfold f2d_spec, contractDbyF. reflexivity. Qed.
Theorem impl_is_correct2: d2f_spec contractFbyD.
Proof. unfold d2f_spec, contractFbyD. reflexivity. Qed.

(* F=F' なら F*=F'* となる *)
Theorem f_f'_fstar_f'star: forall cf cf', eq_cf cf cf' -> eq_cd (contractDbyF cf) (contractDbyF cf').
Proof. unfold eq_cf, eq_cd. intros. destruct s as [pre con]. simpl. apply H. Qed.
(* D=D' なら D*=D'* となる *)
Theorem d_d'_dstar_d'star: forall cd cd', eq_cd cd cd' -> eq_cf (contractFbyD cd) (contractFbyD cd').
Proof. unfold eq_cf, eq_cd. intros. simpl. rewrite H. reflexivity. Qed.  
(* F**=F となる *)
Theorem f_fstarstar: forall cf (pre:sentences) (con:sentence), eq_cf cf (contractFbyD (contractDbyF cf)).
Proof. unfold eq_cf, eq_cd. simpl. reflexivity. Qed.
(* D**=D となる *)
Theorem d_dstarstar: forall cd (s:inference), eq_cd cd (contractDbyF (contractFbyD cd)).
Proof. unfold eq_cf, eq_cd. intros. simpl. destruct s0. reflexivity. Qed.

(* F根拠型に関しては根拠公式という形で論理として働くことを証明できたけれども
     D根拠型に関しても似た形で 正しい推論が論理として働くことを示したい
     そのため上記の変換公式を利用して以下のように定義する:
     > 約束Dで決まる「正しい推論」という性質が論理として機能するとは、
        D* で決まる「根拠となる」という関係が論理として機能する *)
Definition inference_logical cd :=
 logical (logic_of (contractFbyD cd)).

(* すると以下の定理が成立する:
     > 『約束Fで決まる「根拠となる」という性質が論理として機能する』
          ⇔ 『約束F*で決まる「正しい推論」という関係が論理として機能する』
 *)
Theorem cf_good_cd_good: forall cf, logical (logic_of cf) -> inference_logical (contractDbyF cf).
Proof. intros. inversion X. econstructor. simpl. eassumption. assumption. Qed.
Theorem cd_good_cf_good: forall cf, inference_logical (contractDbyF cf) -> logical (logic_of cf).
Proof. intros. inversion X. econstructor. simpl. eassumption. assumption. Qed.

(* さらに以下のシンプルな事実も成立する 
     > 1. 『Fが根拠型を満たす』⇔『F*が推論型を満たす』
     > 2. 『Dが推論型を満たす』⇔『D*が根拠型を満たす』 *)
Theorem f_reason_fstar_reason: forall cf (_:reasonF cf), reasonD (contractDbyF cf).
Proof. intros cf X. inversion X. remember (pre, con) as s. econstructor. simpl.
  assert (logic_of cf (fst s) (snd s)) by (subst;assumption). eassumption. subst. assumption. Qed.
Theorem fstar_reason_f_reason: forall cf (_:reasonD (contractDbyF cf)), reasonF cf.
Proof. intros cf X. inversion X. destruct s as [pre con]. simpl in H0. econstructor. simpl in H. eassumption. assumption. Qed.
Theorem d_reason_dstar_reason: forall cd (_:reasonD cd), reasonF (contractFbyD cd).
Proof. intros cd X. inversion X. destruct s as [pre con]. econstructor. simpl. eassumption. assumption. Qed.
Theorem dstar_reason_d_reason: forall cd (_:reasonF (contractFbyD cd)), reasonD cd.
Proof. intros cd X. inversion X. econstructor. simpl in H. eassumption. assumption. Qed.

(* これによってひとまずのゴールである正しい推論についての定理(推論定理)が得られる:
     > 『Dで決まる性質「正しい推論」が論理として機能する』⇔『Dが推論型を満たす』 *)
Theorem inference_logical_reasonable: forall cd, inference_logical cd -> reasonD cd.
Proof. intros. inversion X. econstructor. simpl in H. eassumption. assumption. Qed.
Theorem reasonable_inference_logical: forall cd (_:reasonD cd), inference_logical cd.
Proof. intros. inversion X. destruct s as [pre con]. econstructor. simpl. eassumption. assumption. Qed.