数理論理学をCoq上でやると いいことがあるかもしれないという話です。
私のCoqの理解が進んできたのでとりあえず整理します。ツッコミ等も歓迎です。教養レベルの数理論理学の知識を前提とします。
1. メタ言語としてのCoq
対象言語とは？: 数理論理学で扱う対象は、構文規則に則った記号列（＝項や論理式）です。使える記号は前もって決めておきます。対象言語を定めるといいます。対象言語を定めることで対象を正確に記述できます。
メタ言語とは？: 一方、論理式同士に成り立つ秩序（例: 推論, 証明, 帰結関係, 理論の各種性質）は、日本語や英語などの自然言語、対象言語の記号、及び、対象言語に含まれない記号を使って定式化されます。対象言語に言及しつつ、その性質を対象言語の外から眺めて読者を納得に導く言語をメタ言語といいます。
メタな論理は自明なのか？: メタ言語でなされる行為や規則には、それを支える論理があります。多くの場合 自明すぎて明示されませんが、問題になることもあります。以下のような疑問を持った人も多いと思います:
- 意味論において集合概念を利用するのは循環的であり、問題はないのか？
- 集合論を基礎づけるための数理論理の説明に、集合論的な概念がでてくるという意味での「循環」です
- 1階述語論理の完全性の証明に 選択公理を使って本当によいのか？
- そもそも、その説明はどのような論理・規則で正当化されているのか？
- 例えば 亀がアキレスに言ったこと-Wikipedia に代表されるように無限後退は生じないのだろうか？
- そもそも、その説明は一意に解釈可能な意味を持っているのか？
- 後期ウィトゲンシュタインの哲学に代表される問題意識を持つ必要はどうしても出てきます。
このように、数理論理学の主戦場であるメタレベルにおける行為は、（人間にとって）誤りやすい、前提や仮定や規則が明示化/一覧化されていない、という側面を持つといってもいいかもしれません。
メタ言語としてのCoq: 証明や推論は規則に従った行為であるので、コンピュータに代行させることも可能です。より正確には、コンピュータにある種の情報処理をさせることができ、人間がその入出力に対して推論や証明をしているという意味付けできます。こうすることで、人間が陥るケアレスミスを防いだり、必要な前提を明確化できるなどのメリットがあります。Coqはそのための道具立てを提供します。
本節のまとめ: 数理論理学における証明や推論といった行為は、コンピュータでも可能です。Coqを使ってコンピュータにやらせることで、ケアレスミスを防止したり、メタレベルでの前提・仮定を明確化できたり、成果物を実行環境ごと保存ができたりして、いいことずくめのような気がします。
2. Coqとは結局何なのか？
Coqとは何か？: CoqとはCIC/Calclus of Inductive Constructionという計算体系をコンピュータ上で実行するための一連の道具立てです。「論理」と「計算」は異なりますが、カリーハワード対応に見られるように 密接な関係もあります。CICはカリーハワード対応を積極的に採用・拡張した体系です。そしてCoq/CICは、（命題や証明のカリーハワード対応物である）型や証明項を扱う型システムであるだけでなく（型システムからみた対応物である）命題を体系に組み込んでいます(Propというimpredicativeなソートが組み込まれています)。その意味で Coq では命題や証明を直接扱っているともいえます。
Coqで論理学を符号化: 上述のようにCoqは、命題や証明を扱えますが、その一方で、Coq/CICは計算体系であり論理そのものではありません。なので、Coq/CIC をメタ言語として採用して数理論理学を展開する、という目的のためには、Coq/CICで組み込まれているPropを使うのではなく、論理学を一から構成する必要があります。例えば、有名なゲーデルの不完全性定理をCoq上で証明した成果 では、1階述語論理およびペアノ算術における対象言語の符号化、及び、それらへのメタな行為（例: 置換、証明、表現可能性）を符号化しています。CICはそれ自体では自然数もブール値も含んでいないので 一から構成しますが、論理学もそれにならうということです。
Coqはどこまで柔軟か？: 数理論理学のメタ言語は日本語・英語などの自然言語ですが、これをCoqで代替できるほどCoqは柔軟で表現力が高い体系なのでしょうか？答えは恐らくYesです。CICはその名前が示すように構成的な道具立てで排中律が成立しないなどの性質もありますが、排中律を計算体系に組み込むこと（≒公理とすること）は簡単にできますし、その他の公理を組み込むことも簡単です（もちろん好き勝手に足すとCICが矛盾をきたすので程々が大事でしょうが・・）。注：ここでの排中律の例はメタ言語としての話です。符号化された古典論理において排中律が成立するかはそのように作ればよいだけの話です。なお、必ず停止するという性質は、こと証明に関して言えば、証明とは有限長であることから好ましい性質です。
3. 最後に
Coq上で論理学を展開することの概念図を書いて、記事を締めます:
<普通の数理論理学>
対象レベル: 対象言語の記号列。例: 0+S0=S0
メタレベル: 自然言語。例: 0+S0=S0は証明可能である
<算術化した数理論理学>
対象レベル: 算術の言語の記号列のゲーデル数
メタレベル: メタレベルの行為/言明のゲーデル数, 及びそれを数項として持つ論理式のゲーデル数（の数項を持つ論理式のゲーデル数（の数項を持つ・・・・）
メタメタレベル: 自然言語 例: ゲーデル数の復号・解釈
<Coqビルトインの論理学>
対象レベル: Propをソートとするobject
メタレベル: タクティックをつかった証明項の構成
<Coqをメタに使った数理論理学>
対象レベル: CICでのデータ型。例: Term型 Formula型
メタレベル: CICでのデータ型・Fixpoint・型つけ。例: SysPrf型（ヒルベルト流証明型）