IsabelleのHOLはどのような体系か
Isabelle のHOLは、依存型のない型付きHOL: Higher-order logic (高階述語論理) で、論理式の導出により証明を行う体系です。
HOLは、量化に制限のない体系です。ある集合$A$に属するすべての集合$B$に属するすべての集合$C$に属するある集合$D$が存在して…といった量化子を入れ子に繋げた命題が許されます。
次に、型付き論理とは何かについて述べます。まず、素朴集合論におけるRusselのパラドックスを回避するためには、いくつかの方法があります。
- 集合の公理を変更し、集合の構成方法を限定する方法
- 集合に何らかのマークをつけ、自己言及的な命題を除外する方法
一番目の方法は、ZF公理系を採用するなどの方法があり、後者の方法にはStratificationを採用する、型付き論理を採用するなどの方法があります。型付き論理では、対象に型とよばれるタグをつけることを強制します。そして、集合を構成する公理において、AとAの集合に別の型をつけることで、自己言及的な命題を排除することができます。
型付き論理は単にRusselのパラドックスを回避できるだけではなく、数学的構造を保ち、意味のある適切な命題のみが取り扱われるように制約を付ける効果があります。型がない場合、「整数点 $(a, b)$ と 有理数 $q$ のベクトル和が…」といった、下部構造と数学的意味付けとの対応が壊れたナンセンスな命題が出現する可能性があります。このため、ZF公理系を採用する場合においても型をつけることは一般的です。（型システムを導入せずに、数学的構造の定義を変更して、このようなナンセンスを防ぐための機構を理論の内部に導入すること（プログラミング言語における動的型付けのような設計手法の採用）は可能ではあるとは思いますが、煩雑になるため独立した型システムとして理論の外部に置く方が自然であると思います。）
最後に、「論理式による導出」という点について述べます。Coq や Agda においては、Curry-Howard 同型を利用して、命題を型として表し、その型をもつ値（典型的には関数）を構成して示すことで、命題の正しさを証明します。一方で、Isabelleにおいては、型システムはあくまでさきほど述べたような型付き論理を実現するために導入されているだけであるので、示すべき結論をもつ導出木を構成して示すことで、命題の正しさを証明します。これには、型と論理を分別し、論理の誤りと比べて単純である（本来の意味での）型の誤りを明確に指摘することができるという利点があるように思います。
Curry-Howard 同型を利用した証明体系の場合、普通の型システムでは表現力が不足し、意味のある命題をほとんど述べることができないため、値に型が依存する依存型システムを採用することがほとんど必須となっています。一方で、Isabelleにはそのような必要性がないので、依存型は採用されていません。（論理的には、Curry-Howard 同型を利用しない体系においても依存型を採用することは可能であると思いますが、実質的な証明を型と論理式の二か所で行う書き方が許されてしまい、混乱を招くと考えられます。）
Isabelle/HOL における群の定義
recordによるデータ型の定義
Isabelle/HOLでは具体的な構造がどのように定義されているかを見るために、群を定義する標準ライブラリ HOL-Algebra.Group を見てみます。
（このライブラリは、以下の記述でインポートすることができ、これによりどのように使用できるかを確かめられます。）
theory Scratch
imports "HOL-Algebra.Group"
begin
HOL-Algebra.Groupは以下の記述から始まります。
record 'a monoid = "'a partial_object" +
mult :: "['a, 'a] ⇒ 'a" (infixl "⊗ı" 70)
one :: 'a ("𝟭ı")
recordは、名前付きの直積型を定義するキーワードです。これにより定義される型はシステム組み込みの型として直接MLで定義されており、その基本的な性質であるタプルとの同値性はHOL.Recordによって証明されています。レコードの要素につけられた名前は、そのまま（プログラミング言語でいうところの）アクセス関数(getter)として利用可能です。
まず、左辺を見ると'a monoidと書かれています。これは定義される型が型パラメータ'aを与えることによって決まることを表しています。これはプログラミング言語の型システムにおけるC++テンプレートやC#ジェネリクスといった仕組みと同じです。Isabelleには依存型は存在しないので、'aは値ではなく、必ず何らかの型が入ります。
レコードは（クラスベースプログラミング言語でいうところの）継承可能なオブジェクトです。"'a partial_object" + ...という表現は、'a monoidが"'a partial_object"を拡張したレコードであることを表しています。
次に、この定義における'aの実質的な意味とpartial_objectについて考えていきましょう。partial_objectの定義は以下の通りです。
record 'a partial_object =
carrier :: "'a set"
これだけです。したがって、先ほどのモノイドの定義は以下とほぼ同じことです。
record 'a monoid =
carrier :: "'a set"
mult :: "['a, 'a] ⇒ 'a" (infixl "⊗ı" 70)
one :: 'a ("𝟭ı")
モノイド は、モノイドの集合 carrier, 演算 mult, 単位元 one の三つ組みで構成されるというのがこの宣言の意味です。一般的な数学の教科書では、この三つ組みと集合carrier Mを同一視していると思いますが、Isabelleではこのように明確に区別されます。
次に'aという型の意味についてです。これは集合の要素の型を表しており、carrier M が 'a 型の値の集合であることを表しています。ここで重要なことは、型と集合は異なるということです。例えば、数学の教科書では、変数 $k$ が整数であることを $k \in Z$という仮定で表すのが普通だと思いますが、変数 $k$ のもつ数学的構造を整数として解釈すべきであるという内容は、 $k \in Z$という論理式のレベルの議論ではなく、そもそも論理式が命題として適切であるのかというレベルの議論であるため、k :: intと型で表現します。この方式では、整数全体の集合 Z :: "int set"は、$Z = \set{k \mid \mathbf{true}}$であるといえます。なぜならば、型チェックを通過した時点で、$k \in Z$は必ず言えるからです。この$Z$を上位の型（例えば、"rat set") に埋め込んだ場合に初めて、$q \notin Z$ が成り立つ可能性が生じます。