意味論

この章を読むか、読書案内と依存マップで別のルートを選べます。

対象言語は記号とその組み合わせの規則からなり、現時点で記号は何も表示しません。∈̇ や _≐_ を読めるようにするには、何を供給しなければならないのでしょうか。構造は、変数が何の上を動くかと、二つの原始的な述語がそこで何を意味するかを決めます。解釈は各定数記号に台の要素を割り当て、環境は利用できる各変数位置に現在の値を与えます。これらのデータが固定されると、構造的再帰によってすべての項に台の要素が、すべての論理式に命題が割り当てられます。本章を貫くのは、記号とその表示という一つの区別です。記号 ∈̇ は構文に属し、それが意味するようになるのは構造の関係 ∈ˢ であり、両者は異なる層に住んでいます。

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

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

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

一つの構造 𝒮 : ZFStructure ℓ を固定します。これは前章のモデル論的データ、すなわち h-集合である台 S と、二つの台の要素を hProp ℓ の命題に送る等号 ≈ˢ と所属 ∈ˢ です。すべての論理式の解釈はこの同じ命題の宇宙に着地します。したがって集合についての主張は、文字どおり、証明を要素として持つ命題になります。これらのフィールド以外に、構造の内容は使いません。ZFStructure というレコード自体は集合論の公理を含まず、意味論の定義にも集合論の公理は要りません。

open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

open ZFStructure 𝒮

レコードのフィールドは今や固有の名前でスコープに入っています。S が台を、∈ˢ と ≈ˢ が二つの関係を表し、したがって x ∈ˢ y は x と y についての構造の所属命題と読みます。対象言語の構成子もスコープにあり、各種の記号には意味論の側に明確な対応物があります。定数記号には台の要素が一つ必要であり、定数域から S への関数によって一度に固定されます。変数の位置には、使用のたびに変わりうる値が必要で、それを供給するのが環境です。原子論理式には二つの関係のいずれかが必要です。結合子と量化子には集合論はまったく要らず、「基礎語彙」の命題上の論理演算 ⊓、⊔、⇒、∀[ x ] P x、∃[ x ] P x がそこに収まります。解釈は合成的です。項や論理式の意味は、その構成子と、直接の構成部分の意味から定まります。

環境

アリティ n の項は位置 0 から n - 1 までを参照でき、環境 γ はその各位置に台の要素を一つ割り当てます。S ^ 2 の環境には二つの成分があり、var zero と var (suc zero) が参照できますが、個々の項や論理式はその一方だけ、両方、あるいはどちらも使わないこともあります。したがって長さ n が定めるのは利用できる位置の範囲であって、実際に現れる変数の個数ではありません。束縛も同じ原理で働きます。量化子が台からの候補を取り上げるとき、環境はその要素を先頭に置いて拡張され、本体は位置 zero でそれを読みます。

環境の型は S ^ n と表記し、伝統的な上付きの $S^n$ に対応させます。_^_ は「冪」と読みますが、単なる記法です。その定義は Vec A n、すなわち長さが型の一部になっている順序付きベクトルです。ここでは依存型が実際の仕事を担っています。論理式のアリティと環境の長さは食い違いようがなく、不一致ならそもそも正しい組み合わせが成立しません。演算 lookup は Fin n の位置にある成分を返し、x ∷ γ は先頭に一つ成分を付け加え、それまでの成分を後続の位置へ移します。

infixl 30 _^_

_^_ : ∀ {ℓ''} → Type ℓ'' → ℕ → Type ℓ''
A ^ n = Vec A n

評価と充足

意味論を運ぶのは二つの判断です。⟦ t ⟧ γ は項 t が環境 γ のもとで表示する台の要素を、γ ⊨ φ は論理式 φ が γ のもとで成立することを述べる命題を表します。どちらも固定された定数解釈 ι : K → S に対して定義されます。定数は ι から値を得て、変数は γ とともに変わり続けます。量化子が現れると、この分離がただちに効いてきます。束縛は変数の値を変えますが、定数記号の表示は変わりません。

解釈と環境は、互いに異なる二つの問いに答えます。定数 con k はどの環境を与えても ι k を表示し、変数 var i はどの解釈を固定しても lookup i γ を表示します。したがって環境が項の評価に関わるのは変数の場合だけで、定数記号の意味はつねに ι が固定します。この二つの場合で項の評価は尽くされます。

定数域 K と解釈 ι : K → S を固定します。この解釈のもとで、項の評価は項と環境を S の要素へ送り、充足関係は論理式と環境を命題へ送ります。充足関係は論理式の構造に沿って再帰的に定まります。原子式は構造の二つの関係を、結合子は「基礎語彙」の命題演算を、偽は空命題を用い、量化子は台の上を動きます。有界量化子では、限界の表示が、量化される要素の満たすべき所属条件を定めます。

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

この節を支えるのは二つの定義で、その型が何であるかを物語っています。評価 ⟦_⟧ は項と環境を台の要素へ写します。充足 _⊨_ は環境と論理式を hProp ℓ の命題、すなわち任意の二要素が等しい型へ写します。そのような型の要素は証明です。したがって充足は単なる判定ではなく命題であり、定義は各式と各環境に対して、意味される命題がちょうどどれであるかを計算します。アリティ n は両方の型に現れるため、長さの合う環境だけが論理式に適用できます。論理式と環境の間の規律は、今や型そのものが強制します。

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

  infix 6 _⊨_

  _⊨_ : ∀ {n} → S ^ n → Formula K n → hProp ℓ

原子的な所属は二つの項を評価し、それらを構造に渡します。主張は、二つの表示についての構造の所属命題になります。等号の原子は ≈ˢ について同様です。ここで、点付きの記号がついに意味を持ちます。∈̇ は ∈ˢ として読まれ、構文より一つ下の層に降ります。命題的な三つの節は完全にホストの側にとどまります。連言は ⊓ で、選言は ⊔ で、含意は ⇒ で解釈され、いずれも命題上の演算です。連言の証明は証明の対であり、含意の証明は前件の証明を後件の証明へ変える関数です。この三つの節に集合論はまったく現れず、ホストの命題論理が部分公式の表示する命題に施されるだけです。

  γ ⊨ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
  γ ⊨ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
  γ ⊨ (φ ∧̇ ψ)  = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
  γ ⊨ (φ ∨̇ ψ)  = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
  γ ⊨ (φ ⇒̇ ψ)  = (γ ⊨ φ) ⇒ (γ ⊨ ψ)

偽には環境は不要です。⊥̇ は空命題 ⊥ として読まれます。量化子は、台がついに登場する場所です。非有界の ∃̇ φ は台の上の存在量化を表します。すなわち、S のある要素 x が拡張環境 x ∷ γ のもとで本体を成立させる、という命題です。対になる ∀̇ φ は全称量化を表し、その証明は各 x : S に x ∷ γ のもとでの本体の証明を割り当てる関数です。本体の内側では位置 zero が候補 x を保持し、γ の成分は後続の位置へ移っています。外側の論理式で自由だった変数は末尾から読まれます。命題的切り詰めにより、存在量化はそのような要素が存在することを記録するだけで、要素そのものをデータとして運びません。

有界の形はもう一つの成分を加えます。限界の表示への所属です。∀̇∈ t φ は、⟦ t ⟧ γ への所属が本体を含意することを要求します。したがって ⟦ t ⟧ γ のすべての元が φ を満たします。∃̇∈ t φ は、元でありかつ本体を満たす要素を求めます。それぞれの環境がどこで使われるかに注意してください。限界 t は新しい束縛の外側にあり、元の γ で評価されます。拡張 x ∷ γ を見るのは本体だけです。この二つの節こそ、「t のすべての元が φ を満たす」「t のある元が φ を満たす」という読みの意味論的内容です。

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

まとめ

意味は合成的に与えられます。項は台の要素を表示し、それを決めるのは定数解釈と環境です。アリティ n の論理式は、利用できる位置を使い切るかどうかにかかわらず、S ^ n → hProp ℓ 型の関数を定めます。原子式は構造の二つの関係に問い合わせ、結合子はホストの命題演算を適用します。量化子は先頭に置かれた新しい位置を台の上に動かし、有界の形は拡張の外で限界の表示への所属を確かめ、拡張の内で本体を解釈します。どの節も構造的再帰の一段です。構成が使うのは台 S と二つの関係 ∈ˢ、≈ˢ であり、証明 isSetS も集合論の公理も使いません。