対象言語

集合について何かを述べれば、ふつうはそれが成り立つかを問う。本章では真偽をひとまず脇に置き、主張をどう書き、どう組み合わせるかを考える。書かれた形そのものを数学の対象として扱うために、対象言語を作る。

まず対象の指し方を定め、それを使って主張を書き、最後に「どの対象についても」「ある対象について」を表す形を加える。Agda のコードは、その都度どんな式を書けるかを定める。それらが何を指し、主張が成り立つかどうかは、後で考える。

以下の定義には、初めは不思議に思える選択もある。対象の名前をあらかじめ用意し、対象を入れる場所を数字で表すのはなぜか。意味より先に書き方を定め、論理記号の一部を基本形として、ほかをそこから定義するのはなぜか。どれも大切な問いだが、本章で一度に答える必要はない。対象言語の定義に、数学的に唯一の標準形があるわけではない。よく使われる方法は、書き方が違っても表現力はおおむね同じだと証明できる場合が多いが、使い勝手にはそれぞれ長所がある。本書では確立された方法の一つを採り、後で扱う集合論に最も適した形になるよう、そうした長所の間でバランスを取っている。後で式の意味を定め、実際に使うにつれて、個々の選択の理由も見えてくる。

項

ある対象が別の対象に属すると書くには、まず両者を指す表現が要る。名前をあらかじめ決めてもよいし、番号付きの場所を残しておき、式を使うときに対象を割り当ててもよい。こうして一つの対象を指す表現を項と呼ぶ。

あらかじめ決める名前を型 K に集め、その元を定数名、K を定数域と呼ぶ。一方、自然数 n は、今使える番号付きの場所の数を表す。場所全体が文脈で、一つひとつが変数位置である。「基礎語彙」で導入した Fin n は、0 から n の一つ手前までの位置をちょうど含む。Term K n は、この二通りで作られる項の型である。ただし、名前や位置が実際に何を指すかはまだ決めない。

定義 (Term) 宇宙レベル ℓ、型 K : Type ℓ、自然数 n : ℕ に対し、帰納型 Term K n : Type ℓ を定める。

data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where

各 k : K に対して項 con k : Term K n を、各 i : Fin n に対して項 var i : Term K n を定める。

  con : K → Term K n
  var : Fin n → Term K n

この二つの構成子が作るのは対象の指し方であり、対象そのものではない。名前 k : K から項 con k を、位置 i : Fin n から項 var i を作れる。文脈の長さが二なら使える位置は 0 と 1 だけで、2 は含まれない。一方、con で作る項は位置をまったく使わないので、Term K 2 型にも属する。以下、項を t、u、位置を i、j と書く。

論理式

項があれば、対象についての主張を書ける。書かれた主張を論理式と呼び、以下では φ、ψ、θ と書く。最も単純なのは、二つの項について所属か等しさを述べる原子論理式である。そこから「かつ」「または」「もし…ならば…」を組み立て、さらに後で「どの対象についても」「ある対象について」という形を加える。

括弧を省いても読み違えないよう、先に結び付きの強さを決める。所属と等号が最も強く、次が後で定義する「でない」、その次が「かつ」「または」、最後が「もし…ならば…」である。最後の形は右側からまとまるので、φ ⇒̇ ψ ⇒̇ θ は φ ⇒̇ (ψ ⇒̇ θ) と読む。以下の優先順位宣言が変えるのは論理式の読み方であり、作れる論理式は変わらない。

infix   _≐_ _∈̇_
infixr  _∧̇_ _∨̇_
infixr  _⇒̇_
infix   ¬̇_

∈̇ や ∧̇ などに付く点は、対象言語に書かれた主張を、Agda で対象について直接述べる命題と区別する。たとえば t ∈̇ u は所属を述べる形を記録するだけである。t と u が何を指し、その所属が成り立つかは、まだ決まっていない。

定義 (Formula) 宇宙レベル ℓ、型 K : Type ℓ、自然数 n : ℕ に対し、帰納型 Formula K n : Type ℓ を定める。

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where

構成子 _∈̇_ と _≐_ はそれぞれ Term K n の項を二つ取り、一つの論理式を作る。_∧̇_、_∨̇_、_⇒̇_ はそれぞれ Formula K n の論理式を二つ取り、新たな論理式を作る。⊥̇ は引数を取らない。

  _∈̇_ _≐_     : Term K n → Term K n → Formula K n
  _∧̇_ _∨̇_ _⇒̇_ : Formula K n → Formula K n → Formula K n
  ⊥̇           : Formula K n

構成子 ∃̇_ と ∀̇_ はそれぞれ Formula K (suc n) の論理式を一つ取り、Formula K n の論理式を作る。∀̇∈ と ∃̇∈ は、さらに Term K n の項を一つ取る。

  ∃̇_ ∀̇_       : Formula K (suc n) → Formula K n
  ∀̇∈ ∃̇∈       : Term K n → Formula K (suc n) → Formula K n

⊥̇ は、常に偽となる主張を表すものとして用意する。今はどの論理式を書けるかを定めるだけで、真偽はまだ判定しない。「または」の _∨̇_ と「もし…ならば…」の _⇒̇_ には、それぞれ構成子を用意する。「でない」を表す ¬̇_ や「かつ」を表す _∧̇_ で書き換えて済ませると、まだ仮定していない論理の規則が必要になる場合がある。形を分けておけば、後でそれぞれの意味を直接与えられる。

∀̇_ は「どの対象についても」、∃̇_ は「ある対象について」を表す。これらは、できあがった主張を二つつなぐだけでは書けない。後に続く主張には、新たに取り上げる対象を指す場所が要る。そこで量化子は、後続の論理式に位置を一つ加える。次の図は、もともと一つ位置がある場合に番号がどう変わるかを示す。

新しい 0 番の位置が、この量化子の束縛変数に当たる。もとの位置にある変数は、この量化子から見れば自由変数のままで、番号だけが一つ後ろへずれる。したがって量化子の内側の論理式は Formula K (suc n) 型、全体は Formula K n 型になる。内側で新しい位置を使わなくてもよい。名前を保存せず、位置で参照を記録する方法が de Bruijn 添字である。名前の衝突を避けるための付け替えが要らず、使える範囲の外を参照する式も作れない。

∀̇∈ と ∃̇∈ は、項 t が指す集合の元に範囲を限る形である。t は新しい位置を加える前に書くため、外側の Term K n 型のままである。拡張された文脈を使うのは、量化子の内側の論理式だけである。これらを有界量化子という独立の構成子にしておけば、後で有界量化子だけを使う論理式を見分けられる。

定義 (¬̇_) ここまでの構成子で論理式の基本形はそろっており、否定のために別の構成子を加える必要はない。¬̇ φ を φ ⇒̇ ⊥̇ と定める。そのため、論理式を再帰的に調べるときは含意の場合を扱えば足り、否定の場合を増やさずに済む。後で意味を与えると、この含意は φ の否定を表す。

¬̇_ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n → Formula K n
¬̇ φ = φ ⇒̇ ⊥̇

定義 (⊤̇) 真も構成子を増やさず、⊤̇ を ⊥̇ ⇒̇ ⊥̇ と定める。したがって後では含意と偽を解釈すれば、否定と真にも意味が定まる。どちらの定義も、定数域や文脈の長さを選ばずに使える。

⊤̇ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n
⊤̇ = ⊥̇ ⇒̇ ⊥̇

項と論理式の作り方は、定数域 K の選び方によらず同じである。ある構造の台を K にすれば、その元を定数で名指せる。名前を付ける対象を一部に限れば、使える定数も減る。空型 ⊥* を選べば、使える定数はない。変数位置の数は n で独立に決める。

文とパラメータを持たない論理式

定数名と変数位置は、それぞれ独立に使わないようにできる。文は自由変数を持たない。文脈の長さをゼロにした Formula K 0 だが、定数は使える。一方、パラメータを持たない論理式は定数を持たない。定数域を空型 ⊥* にした Formula ⊥* n だが、自由変数は使える。どちらのためにも別のデータ型やコード名は要らない。

空型から任意の K への写像がある。そこで後の定数写像を使えば、パラメータを持たない論理式をどの定数域にも移せる。構造の元を先に列挙しなくても、この種の論理式なら列挙できる。ただし、符号化できるのはこれだけではない。後の章では、台の元を定数として使う論理式も符号化する。

まとめ

本章で決めたのは、項と論理式の書き方である。定数と変数位置で対象を指し、量化子で新しい位置の作用域を定める。それらが何を指し、論理式がいつ成り立つかは、まだ決めていない。次は、その記号を解釈するための構造を用意する。