この章を読むか、対話型目次と依存グラフで別のルートを選べます。

命題値構造 𝒮 : ZFStructureₕ ℓ を固定する。その台の要素を議論の対象とし、二つの関係で等号と所属を解釈する。

module FOL.Semantics {ℓ} (𝒮 : ZFStructureₕ ℓ) where

主張を書くための言語と、それを解釈するための構造がそろった。本章では両者を結び付ける。まず名前や番号付きの位置がどの対象を指すかを定め、次に各論理式を、それらの対象についての命題として解釈する。主張に意味を与えることと、その主張が成り立つかを判定することは別である。最後の節で、判定に排中律がどう使われるかを説明する。

固定した構造を開き、台 S と関係 ≈ˢ、∈ˢ を直接使えるようにする。集合論の公理は仮定しない。

open ZFStructure 𝒮

環境

変数位置は値を取り出す場所を示すが、具体的な対象までは指定しない。文脈内で利用できる各位置に台の要素を割り当てたものを環境という。長さ n の文脈に対しては、この割当をベクトル γ : Vec S n で表す。位置 i : Fin n の成分が、対応する変数の値である。

たとえば環境 a ∷ b ∷ [] では、0 番の位置に a、1 番の位置に b が入る。論理式は一方の位置だけを使っても、同じ位置を何度参照しても、どちらも使わなくてもよい。環境が記録するのは論理式の解釈で参照できる値であり、変数の出現ごとに値を一つずつ並べるわけではない。その長さは文脈の長さと一致し、変数の出現回数とは異なる。

項と論理式の解釈

定数名にも値を与える必要がある。各名前に台の要素を割り当てる関数 ι : K → S を定数解釈という。変数の値とは異なり、量化子によって環境が拡張されても、定数の値は変わらない。部分モジュール At で K : Type ℓc と ι : K → S を固定し、以下の定義で共通に使う。

module At {ℓc} (K : Type ℓc) (ι : K → S) where

項の評価

定義 (⟦_⟧) 項の評価は、項 t : Term K n と環境 γ : Vec S n に台の要素 ⟦ t ⟧ γ : S を対応させる。「γ のもとでの t の値」と読む。定数の値は ι から、変数の値は γ から得る。

⟦_⟧ : ∀ {n} → Term K n → Vec S n → S
⟦ con k ⟧ γ = ι k
⟦ var i ⟧ γ = lookup i γ

共通の添字 n により、環境の長さは項が必要とする文脈の長さと一致する。定数域を台そのものに取れば、ι = id として各要素を自分自身の名前にできる。定数域が空なら定数の場合は生じないが、変数の値は引き続き環境から得る。どちらの選択も文脈の長さとは独立である。

充足関係

定義 (_⊨_) 充足関係は、環境 γ : Vec S n と論理式 φ : Formula K n に命題 γ ⊨ φ : hProp ℓ を対応させる。「γ は φ を満たす」と読み、⟨ γ ⊨ φ ⟩ の要素は、その割当のもとで式が成り立つことの証明である。この命題を、論理式の構成に沿って次のように再帰的に定める。

infix 4 _⊨_
_⊨_ : ∀ {n} → Vec S n → Formula K n → hProp ℓ

原子論理式では、まず二つの項を評価し、構造の対応する関係を適用する。∈̇ には ∈ˢ、≐ には ≈ˢ を使う。

γ ⊨ t ∈̇ u = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
γ ⊨ t ≐ u = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ

連言・選言・含意では、二つの部分式を同じ環境で解釈し、得られた命題を「基礎語彙」の対応する演算で組み合わせる。

γ ⊨ φ ∧̇ ψ = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
γ ⊨ φ ∨̇ ψ = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
γ ⊨ φ ⇒̇ ψ = (γ ⊨ φ) ⇒ (γ ⊨ ψ)

偽は常に ⊥ と解釈する。非有界量化子では x : S を動かし、その値を先頭に加えた x ∷ γ のもとで本体を解釈する。存在量化子はそのような値が単に存在することを述べ、全称量化子はどの値でも本体が成り立つことを求める。

γ ⊨ ⊥̇   = ⊥
γ ⊨ ∃̇ φ = ∃[ x ∶ S ] x ∷ γ ⊨ φ
γ ⊨ ∀̇ φ = ∀[ x ∶ S ] x ∷ γ ⊨ φ

有界量化子では、限界を表す項 t をもとの環境で評価する。全称の場合は、その値に属するならば本体が成り立つことを求める。存在の場合は、所属と本体がともに成り立つことを求める。拡張した環境を使うのは本体だけである。

γ ⊨ ∀̇∈ t φ = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ (x ∷ γ ⊨ φ)
γ ⊨ ∃̇∈ t φ = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ (x ∷ γ ⊨ φ)

これらの節は各論理式に意味を与えるが、その真偽を判定するわけではない。等号の節が使うのは与えられた関係 ≈ˢ であり、Agda のパスによる等しさとは限らない。選言と存在量化は命題的切り詰めを使うため、その証明から分岐や証人をデータとして取り出せるとは一般にはいえない。ここまでの定義に排中律は要らない。

量化された論理式を読む

量化子の本体に増やした位置にも、これで値が入る。外側の環境を γ = a ∷ [] とすると、先頭に x を加えた環境は x ∷ a ∷ [] になる。もとの値はそのままで、番号だけが一つ後ろへずれる。次の図は「対象言語」と同じ位置の規則を、環境が与える値とともに示している。

拡張した環境では、量化する値が 0 番に入り、もとの値は 1 番に残る

具体的に、本体を var zero ∈̇ var (suc zero) とすると、拡張した環境での意味は x ∈ˢ a になる。前に ∀̇ を付ければ、台のどの要素も a に属するという命題になり、∃̇ を付ければ、a に属する台の要素が存在するという命題になる。どちらかが成り立つと主張しているのではなく、それぞれの式が表す命題を確かめている。

有界量化子の限界は、もとの環境で解釈する。∀̇∈ (var zero) φ の限界は a を指すが、φ の内部の先頭位置は x を指す。このためコードでは、もとの環境で限界の値を求める。なお、否定と真には別の節を設けなくてよい。対象言語での定義を展開すると、含意と偽になるからである。

論理式によって表示される述語

ここまでは論理式から出発し、それが表す命題を求めてきた。逆に、述語 predicate : A → hProp ℓ を先に与え、その論理式による表示を用意することもできる。A は考察する場合の添字の型であり、台と同じでなくてもよい。一つの論理式を固定し、各 a : A に環境を与える。

定義 (FormulaPredicate) A、K、ι、predicate を与える。その論理式による表示は、アリティ、そのアリティの論理式、各添字に対応する環境、および各添字で論理式の意味が与えられた述語と等しいことの証明からなる。構成子を presented とする。

record FormulaPredicate {ℓa ℓc} (A : Type ℓa) (K : Type ℓc)
                        (ι : K → S) (predicate : A → hProp ℓ)
    : Type (ℓ-max ℓa (ℓ-max ℓc (ℓ-suc ℓ))) where
  constructor presented

次の四つのフィールドが、これらのデータを順に記録する。アリティ arity は、これまでの添字 n と同じく、使える変数位置の数を表す。reading 内の局所的なモジュール名 I は解釈 At K ι を指定する。したがって environment a I.⊨ formula は、a に割り当てた環境での論理式の意味である。

  field
    arity       : ℕ
    formula     : Formula K arity
    environment : A → Vec S arity
    reading     : (a : A) → let module I = At K ι in predicate a ≡ (environment a I.⊨ formula)

たとえば a : S を固定し、述語 λ x → x ∈ˢ a を考える。論理式 var zero ∈̇ var (suc zero) を使い、各 x に環境 x ∷ a ∷ [] を与えれば、この述語を表示できる。述語の引数は一つだが、論理式のアリティは二である。環境が、変化する引数と固定した対象の両方を与えるからである。論理式を解釈するとそのまま元の述語が得られるので、reading は refl で証明できる。

表示する述語と定数解釈はパラメータであり、追加のフィールドではない。reading は二つの hProp ℓ の値を結ぶパスを与える。それに沿って、与えられた述語の証明を充足の証明に移すことも、その逆もできる。論理式や環境の一意性は要求しない。

排中律による判定

論理式を解釈して得られるのは命題であり、その証明や反証が自動的に得られるわけではない。ただし lem : LEM ℓ が与えられれば、その命題に排中律を適用できる。この仮定を使うのはここからであり、それまでの意味の定義には必要ない。

補題 (decideSatisfaction) 定数解釈・環境・論理式が与えられたとき、LEM ℓ から対応する充足命題の判定が得られる。

証明 At でその命題を定め、lem を適用する。論理式と環境を引数に残すことで、どの命題を判定しているかが明確になる。

decideSatisfaction : ∀ {ℓc n} {K : Type ℓc} (ι : K → S)
                   → LEM ℓ → (γ : Vec S n) → (φ : Formula K n)
                   → let module I = At K ι in Dec ⟨ γ I.⊨ φ ⟩
decideSatisfaction ι lem γ φ = lem (γ I.⊨ φ)
  where module I = At _ ι

二つの原子的な場合で、この対応を具体的に確かめる。どちらの式にも定数名は要らないので、空の定数域 ⊥* {ℓ} を取り、空型の除去関数を解釈に使う。環境 x ∷ y ∷ [] が二つの対象をそれぞれの位置に割り当てる。

系 (decideMembership) LEM ℓ により、台の任意の二要素の所属関係を判定できる。

証明所属の原子論理式に補題を適用する。二つの変数の値はそれぞれ x と y なので、その意味はちょうど x ∈ˢ y である。

decideMembership : LEM ℓ → (x y : S) → Dec ⟨ x ∈ˢ y ⟩
decideMembership lem x y =
  decideSatisfaction {K = ⊥* {ℓ}} (⊥*-rec {A = S}) lem
    (x ∷ y ∷ []) (var zero ∈̇ var (suc zero))

系 (decideEquality) LEM ℓ により、台の任意の二要素について、構造が指定する等号の関係を判定できる。

証明定数域と環境はそのままに、等号の原子論理式を使う。その意味は x ≈ˢ y であり、Agda のパスによる等しさについての主張ではない。

decideEquality : LEM ℓ → (x y : S) → Dec ⟨ x ≈ˢ y ⟩
decideEquality lem x y =
  decideSatisfaction {K = ⊥* {ℓ}} (⊥*-rec {A = S}) lem
    (x ∷ y ∷ []) (var zero ≐ var (suc zero))

まとめ

定数解釈と環境が項の値を定め、構造の関係と命題の演算が論理式の意味を定める。量化子は新しく加えた先頭の値を動かし、外側の割当は保つ。FormulaPredicate は与えられた述語の論理式による表示を記録し、排中律はそれとは別に充足命題の判定を与える。意味を定義すること自体には、排中律も集合論の公理も要らない。次章では論理式の書き方に戻り、量化子の組み立て方に応じて分類する。

意味論

環境