対象言語

集合論は集合について語ります。しかし集合論そのものについて定理を証明するには、その文が、明示的な規則で組み立てられる式として、それ自体の数学的対象でなければなりません。この章ではその対象言語を定義し、利用できる定数名、参照できる変数位置、そして項と論理式の形成規則を定めます。本章の中心となる決定は作用域をめぐるものです。式の自由変数文脈の長さはその式自身の型の一部であり、その文脈を超える参照は、禁じられているというより、そもそも書けません。

{-# OPTIONS --cubical --safe --guardedness #-}

各論理式は有限の自由変数文脈の上に書かれ、その長さにあたる自然数 n は論理式自身の型の一部です。変数は Fin n の元、つまり位置 0 から n - 1 までです。量化子を形成すると、この設計がそのまま現れます。量化子の本体には、量化して得られる論理式より利用できる変数位置が一つ多いため、添字は n から suc n へ進みます。したがって項は文脈の外の変数に言及できません。そのような位置は存在しないからです。

module FOL.Syntax where

変数は論理式が何を参照できるかを決め、定数は何を名指せるかを決めます。文脈の長さ n のほかに、論理式は任意の定数記号の型 K、すなわち定数域の上で述べられます。K は言語全体に対して一度だけ選ばれるため、一つの論理式の中で使える名前が変わることはありません。この二つの選択は独立です。K は名指せるパラメータを、n は使える変数位置の個数を定め、一方を広げても他方は変わりません。

open import Base.Prelude

項と論理式

項は論理式が語る対象を名指し、論理式はその対象について断言します。そこでまず項から始めます。項は、K から取った名前である定数か、利用可能な n 個の位置から取った変数のいずれかです。論理式はこのような項から組み立てられます。出発点は項の間の所属と等号という二つの原子式で、そこへ命題結合子と、有界・非有界の量化子が加わります。

本書を通して、t と u は項を、φ と ψ は論理式を、n と m は文脈の長さを、i と j は変数の添字を表します。

ここで Term は型の族です。型 K と数 n を選ぶと型 Term K n が得られ、項がこの二つなしに現れることはありません。項は K の元である名前か n 未満の数にすぎないので、族全体は K と同じ宇宙レベル ℓ に置かれます。

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

構成子 con は K の元 c を受け取り、それを純粋に名前として扱います。名前はまだ何も意味しておらず、何を指示するかが分かるのは解釈が与えられてからです。構成子 var i は Fin n から位置 i を選びます。n = 2 のとき、var 0、var 1、con c はいずれも Term K 2 の項ですが、var 2 は書けません。Fin 2 に 2 という名の元は存在しないので、これは後の検査で退けられる項ではなく、形成できない式です。

自然数 n が定めるのは、どの位置を名指せるかであって、位置が何回使われるかではありません。con c も var 0 も二つの変数に言及しないまま型 Term K 2 を持ち、論理式が一つの位置を何度も使ってもかまいません。論理式はこの種の項から組み立てられます。

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

項が名前であるのに対し、論理式は断言です。最小の断言が原子式 _∈̇_ と _≐_ です。ある項が別の項に属すること、あるいは二つの項が等しいことを述べます。結合子 ∧̇ ∨̇ ⇒̇ ¬̇ ⊤̇ ⊥̇ は原子式から複合的な主張を組み立て、量化子 ∃̇ ∀̇ はすべての対象にわたります。並んで、∀̇∈ と ∃̇∈ は有界量化子で、それぞれ「…のすべての元について」「…のある元について」と読みます。これらの記号はみな小さな上付きの点を帯びます。点は層の印です。∈̇ が述べるのは対象言語のいう所属であり、周囲の理論の所属関係から一層だけ離れています。点付きの記号はつねに構文であって、意味ではありません。

量化子は変数を束縛します。構文はこの事実を添字に記録します。本体には、量化して得られる論理式より一つ多い利用可能な変数位置があり、本体における位置 0 が今束縛された変数です。どの出現が量化子の支配下にあるかは、位置だけで定まります。これが de Bruijn 方式です。論理式の内部に名前は保存されないので、この形成規則には α 改名や同名の変数を区別する約束が要りません。その余分な位置が実際に使われるかどうかを、論理式は記録しません。

複合論理式を一行に書けば、読む順序を取り決めておく必要があります。この 4 行がそれを一度に定め、対象レイヤー全体に及びます。原子式と否定が最も強く結合し、その水準は 18 と 13 です。連言と選言は中央の水準 12、含意は最も弱い水準 10 で、二組の対はいずれも右結合です。したがって φ ⇒̇ ψ ⇒̇ θ は φ ⇒̇ (ψ ⇒̇ θ) と読まれ、これは反復含意の通常のグループ化です。これらは構文解析上の約束であって、言語への追加ではありません。おかげで入れ子の論理式は普通の数学の文章と同じように読め、括弧は異なるグループ化を意図するときにだけ現れます。対象レイヤーの読みの水準を宣言するのは、本書でここ一度きりです。

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

Formula 族は Term とまったく同じやり方で、定数域 K と利用可能な変数位置の個数 n で添字づけられます。原子式 _∈̇_ と _≐_ は Term K n の二つの項を受け取り、それらの間の所属か等号を断言します。命題的な構成子は、論理式から論理式を作ります。_∧̇_、_∨̇_、_⇒̇_ は連言、選言、含意を構成し、⊥̇ は偽そのものです。どれも変数を束縛も解放もしません。だから添字はずっと n のままであり、量化子が変数を束縛するときにだけ、この添字が変わります。

結合子を略語ではなく構成子とするのは、意味論的な理由のある決定です。論理式は最終的にホストの命題の型 hProp の中で読まれ、各結合子はそこで対応する直接的な演算によって解釈されます。他の記号への還元ではありません。古典的な教科書は φ ∨̇ ψ を ¬̇ (¬̇ φ ∧̇ ¬̇ ψ)、∀̇ を ¬̇ ∃̇ ¬̇、φ ⇒̇ ψ を ¬̇ φ ∨̇ ψ と書き替えて済ませられます。古典論理では二重否定が消えるからです。構成的にはこの消去は一般には使えないので、書き替えた形は望ましい意味を持ちません。そこで本書は ∨̇、⇒̇、そして量化子を、そのまま構成子として採ります。

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where
  _∈̇_ _≐_     : 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) の本体を受け取り、n 個の位置の上の論理式を返します。本体にはもう一つの利用できる位置、すなわち位置 0 があり、これこそ量化子が束縛する変数です。この余分な位置は利用できるだけで、使う義務はありません。それに触れない本体も正当な論理式です。有界の形 ∀̇∈ と ∃̇∈ は、それぞれ「…のすべての元について」「…のある元について」と読みます。限界 t は外側の文脈の項、すなわち Term K n の項であり、量化は t の元にわたって行われます。本体はやはり Formula K (suc n) です。

有界量化子は普通の量化子で書き表せるのに、構成子として保つのは第二の決定です。今度の理由は構文そのものに関わります。もし ∀̇∈ t φ が略語なら、「φ のすべての量化子が有界である」は φ がたまたまどう書かれているかについての事実となり、φ の形の上を計算する何物からも見えません。構成子としてなら、有界性は形に属します。後の章では、構成子ごとに場合を一つ持つデータ型で論理式を分類し、∃̇ と ∀̇ には場合をまったく持たないデータ型によって「量化子はすべて有界」を証明します。そのような証明が可能なのは、有界の形が独立に与えられているからです。この形の論理式は構造を越えてよく振る舞い、この系はモデルの章が受け取り、構成可能宇宙の章へと引き継がれます。

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

否定は構成子ではなく、定義された記号です。¬̇ φ とは定義により φ ⇒̇ ⊥̇ のことです。この定義には計算上の帰結があります。論理式に対して場合分けする関数が出会うのは否定そのものではなく、後件が ⊥̇ である含意です。_⇒̇_ のために用意した場合がすでにこれを取り扱います。したがって否定のための独立した場合が今後必要になることはなく、意味論においても同様です。

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

真も同じ仕方で定義されます。⊤̇ とは ⊥̇ ⇒̇ ⊥̇、すなわち矛盾から矛盾への含意です。構文のほかには何も仮定せず、本章はこれらの記号の今後の読み方に法則を課しません。定義は構成子へと展開されるので、解釈は _⇒̇_ のための既存の場合によってそれらを扱い、特別な用意は要りません。構成子と同じく、¬̇_ と ⊤̇ は宇宙レベルと K を暗黙の引数として受け取り、同じ二つの記号がすべての定数域とすべての変数の個数で働きます。

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

一つの構文が本書のあらゆる用途に仕えます。自由度は、定数域 K の選び方にあります：

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

文には自由変数がなく、パラメータを持たない論理式には定数がありません。この二つの制限は独立であり、論理式をモデルの内部で符号化して評価する段階になると、この違いが決定的になります。

文とは、自由変数を持たない論理式のことです。作用域が内在的であるため、これは追加条件ではなく型 Formula K 0 そのものであり、本書は別の名前を与えません。パラメータを持たない論理式は、別の軸に沿った制限です。定数域を空型 ⊥* とすれば、名指せるパラメータは一つもなく、自由変数はそのまま残ります。これも単なる型 Formula ⊥* n であって、独自の名前は持ちません。空型からの関数は任意の K に対して存在するので、パラメータを持たない論理式はどんな定数域の上でも読むことができ、その映射を与えるのが定数の改名の道具立てです。周囲の集合を先に列挙せず構文を列挙したいとき、パラメータを持たない論理式が役立ち、パラメータは環境から与えられます。ただし、符号化できる論理式がこれだけというわけではありません。後の符号化は、台 S から取る定数を含む Formula S n も直接扱います。

まとめ

項と論理式は、作用域を形成規則そのものに組み込みます。定数域 K は名指せるパラメータを定め、n は利用できる自由変数位置を定めます。どちらも名前が実際に現れる回数を表すものではありません。量化子が変えるのは本体の文脈の長さだけであり、de Bruijn 位置によって、名前を使わずに束縛される変数が定まります。n と K のどちらを空の場合にするかによって、文とパラメータを持たない論理式がそれぞれ得られ、二つの制限は明確に独立したままです。