定数の改名

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

一階の論理式はある定数域 K からの定数記号を運びますが、記号そのものは不活性です。記号が何を指すかを決めるのは解釈関数だけです。この章では、関数 f : K → K' がすべての定数記号を改名するとき何が起こるかを調べます。この作用は mapFo f と書かれます。ここで答える問いは二つです。第一に、改名後の ι の下での充足が、改名前の合成解釈 ι ∘ f の下での充足と一致するという精密な意味で、意味は改名を生き延びるのか。第二に、Lévy 階層における論理式の構文的分類は生き延びるのか、すなわち Δ₀ の証人、より一般に Σₙ/Πₙ の証人は f に沿って運べるのか。答えはいずれも「はい」であり、両方の証明は構文の構成子に対応する構成的なものです。

定数域 K 上の論理式を取り、その定数を関数 f : K → K' に沿って改名してみます。論理式が何を述べるかは、どの解釈がそれを読むかで決まります。目標の解釈 ι : K' → S を改名後の論理式に適用するか、合成 ι ∘ f を元の論理式に適用するかです。本章の意味論的な半分は、この二つの読み方が常に一致するかを問い、構文論的な半分は、Lévy 階層における論理式の分類が改名を生き延びるかを問います。いずれも構文の構成子に対応する構造帰納法で示されます。

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

module FOL.Manipulation.Relabelling where

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

問題の作用は、項には mapTm f、論理式には mapFo f と書かれます。関数 f : K → K' は各定数 con k を con (f k) へ改名し、変数はそのまま残します。定数にだけ作用するため、すべての結合子とすべての量化子 (有界かどうかにかかわらず) は元の位置を保ち、これが Lévy 分類が生き延びるはずだと期待できる理由です。分類そのものは帰納的な証人で与えられます。Δ₀ φ の元は φ のすべての量化子が有界であることを証明する明示的なデータであり、許容される形ごとに一つの構成子を持ち、Σₙ k φ と Πₙ k φ は交互に現れる非有界の列を記録します。

open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo; embed )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈

意味論の側では、台 S を持つ構造 𝒮 が解釈 ι : K → S を通して K 上の論理式を読み、充足関係 _⊨_ と項の評価 ⟦_⟧ を与えます。したがって比較すべき二つの読み方は同じ構文を共有し、解釈だけが異なります。以下の証明では、両者を並行して扱いながら区別を保ちます。

  ; Σₙ; σ-Δ₀; σ-Π; σ-∃; Πₙ; π-Δ₀; π-Σ; π-∀ )
import FOL.Semantics
import Cubical.Data.Empty as Empty

意味の水準

定数の改名は純粋に構文的な操作なので、意味を乱さないことを確認しなければなりません。正確な主張は可換性です。任意の定数域の写像 f : K → K' と対象域の任意の解釈 ι : K' → S に対し、改名後の論理式を ι の下で評価した命題は、元の論理式を合成解釈 ι ∘ f の下で評価した命題と一致します。証明は構造帰納法で進み、基底の場合は項の評価が担い、残りは論理演算の合同性が担います。

台 S をもつ命題値の ZF 構造 𝒮、改名 f : K → K'、そして対象域の解釈 ι : K' → S を固定します。合成 ι ∘ f は源の域の正当な解釈でもあるので、同じ論理式に二つの読み方が得られます。改名後の論理式を ι の下で読むか、元の論理式を ι ∘ f の下で読むかです。可換の問題とは、この二つの読み方が等しい命題を与えるかを問うことです。

module _ {ℓ} (𝒮 : ZFStructure ℓ) where

  open ZFStructure 𝒮
  open FOL.Semantics 𝒮 using ( module At; _^_ )

  module _ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K') (ι : K' → S) where

原子論理式の場合が、二つの読み方がなぜ一致しなければならないかをすでに示しています。論理式 t ∈̇ u を考えると、第一の読み方はこれを ⟦ mapTm f t ⟧ γ ∈ˢ ⟦ mapTm f u ⟧ γ と評価し、第二の読み方は ⟦ t ⟧∘ γ ∈ˢ ⟦ u ⟧∘ γ と評価します。項の補題 ⟦⟧-map はすべての項に対して ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ を与え、その二つの場合はどちらも refl で成立します。改名された定数 con (f k) の評価値は ι (f k) であり、これは合成の読み方が計算するものそのものだからです。変数は定数にまったく関与しません。

    open At K' ι using ( _⊨_; ⟦_⟧ )
    open At K (λ k → ι (f k)) using () renaming ( _⊨_ to _⊨∘_ ; ⟦_⟧ to ⟦_⟧∘ )

    ⟦⟧-map : ∀ {n} (t : Term K n) (γ : S ^ n)
           → ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ
    ⟦⟧-map (con k) γ = refl

充足の補題 ⊨-map はこの一致を項から論理式へ持ち上げ、命題の間の経路 (γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ) を与えます。原子論理式 t ∈̇ u の場合は、⟦⟧-map からの二つの項の経路を cong₂ _∈ˢ_ によって所属関係に入れ、この主張の二つの読み方の間の経路を作ります。等号の原子も ≈ˢ を通じてまったく同様に扱われます。

    ⟦⟧-map (var i) γ = refl

    ⊨-map : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ)
    ⊨-map (t ∈̇ u)  γ = cong₂ _∈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)
    ⊨-map (t ≐ u)  γ = cong₂ _≈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)

命題結合子も同様に合同で処理されます。構造はこれらを対応する論理演算で解釈するからです。φ の二つの読み方の間の経路と ψ のそれとが、⊓ を通して φ ∧̇ ψ の経路に合成され、選言や含意も同様です。偽 ⊥̇ は定数をまったく含まないので、二つの読み方は同じ値となり、経路は refl です。

    ⊨-map (φ ∧̇ ψ)  γ = cong₂ _⊓_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ∨̇ ψ)  γ = cong₂ _⊔_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ⇒̇ ψ)  γ = cong₂ _⇒_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map ⊥̇        γ = refl

量化子は、環境の先頭に一つの要素 x を加えます。非有界量化子では、帰納法の仮定がすべての x : S に対して経路を与えます。関数外延性がそれらの各点での経路を関数の経路にまとめ、cong がそれに沿って存在量化または全称量化を移します。

    ⊨-map (∃̇ φ)    γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → ⊨-map φ (x ∷ γ)))
    ⊨-map (∀̇ φ)    γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → ⊨-map φ (x ∷ γ)))

有界量化子には、さらに一つの成分があります。⟦⟧-map が限定項の二つの解釈を同一視し、帰納法の仮定が量化子の本体の二つの解釈を同一視します。含意または連言の合同性で両者を組み合わせた後、外側の量化を移します。

    ⊨-map (∀̇∈ t φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
      cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))
    ⊨-map (∃̇∈ t φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
      cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))

可換の補題はすでに無パラメータの場合を含んでおり、下の系はそれを読み出すだけです。無パラメータ論理式とは定数域が空型 ⊥* である論理式のことです。解釈すべき定数記号がないため、embed によって任意の域 K 上の論理式へ埋め込め、その意味の二つの読み方は K と ι が何であれ一致しなければなりません。

内側のモジュールは任意の対象域 K と解釈 ι : K → S を固定し、充足関係を二度開きます。一度は通常どおり K 上の論理式に対して、もう一度は名前 _⊨∅_ で空の定数域上の論理式に対してです。後者の解釈は関数 λ b → ι (Empty.rec* b) です。これが正当なのは、Empty.rec* が空型の消去子だからです。⊥* の元があれば任意の型 (S を含む) の元を作れるので、この解釈が実際に値を必要とすることは決してありません。

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

    open At K ι using ( _⊨_ )
    open At (⊥* {ℓe}) (λ b → ι (Empty.rec* b)) using () renaming ( _⊨_ to _⊨∅_ )

    embed-⊨ : ∀ {n} (φ : Formula (⊥* {ℓe}) n) (γ : S ^ n)
            → (γ ⊨ embed φ) ≡ (γ ⊨∅ φ)

系 embed-⊨ は、f を関数 ⊥* → K と見なした空の消去子 Empty.rec* として ⊨-map の直接の実例です。すべての無パラメータ論理式 φ と環境 γ に対し、embed φ を ι の下で充足することと、∅ 標識の読み方で φ を充足することとの間に経路があります。つまり、無パラメータ論理式をより豊かな定数域へ埋め込んでも、その述べる内容は変わりません。

    embed-⊨ = ⊨-map Empty.rec* ι

Lévy 証人の水準

意味は物語の半分にすぎません。Lévy 階層は量化子の構造によって論理式を分類し、その分類は帰納的な証人で表されます。Δ₀ φ は φ のすべての量化子が有界であることを証明する明示的なデータであり、Σₙ k φ と Πₙ k φ は交互に現れる非有界の列を記録します。定数の改名は定数記号を置き換えるだけで、結合子と量化子 (有界かどうかにかかわらず) をすべて元の位置に保つため、証人は生き延びるはずです。mapΔ₀ はまず Δ₀ の水準でこれを示し、その後の相互帰納法が上方へ拡張します。

定数の改名は定数記号を置き換えるだけで、すべての量化子 (有界かどうかにかかわらず) を元の位置に保つため、論理式の量化子の形は mapFo f の下で不変です。Lévy の証人が記録するのはまさにその形なので、任意の f に沿って輸送できるはずです。mapΔ₀ の型は基底の水準でこれを述べます。φ に対する Δ₀ の証人から mapFo f φ に対する Δ₀ の証人を作るのです。原子論理式の場合は直ちに得られます。t ∈̇ u の証人 δ-∈ は引数を取りません。原子論理式には束縛すべき量化子がないからです。mapFo f はこの論理式を同じ形の別の原子論理式へ送るため、再び δ-∈ がそれを証明します。≐ も同様です。

mapΔ₀ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
        {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (mapFo f φ)
mapΔ₀ f δ-∈ = δ-∈
mapΔ₀ f δ-≐ = δ-≐
mapΔ₀ f (δ-∧ c d) = δ-∧ (mapΔ₀ f c) (mapΔ₀ f d)

Δ₀ の残りの構成子は、結合子、偽、そして有界量化子です。それぞれが部分論理式の証人を束ねており、各再帰呼び出しは構造的に小さい証人を輸送し、その構成子が改名後の論理式の上で束を組み立て直します。決定的なのは、Δ₀ には非有界な量化子 ∃̇ と ∀̇ の構成子がなく、有界な ∀̇∈ と ∃̇∈ の構成子だけがあることで、この二つの場合の再帰は結合子とまったく同じです。mapFo f が有界量化子を非有界量化子に変えることはないので、証人の入力には必ず場合が対応し、これが定義を全域的にする理由です。

mapΔ₀ f (δ-∨ c d) = δ-∨ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f (δ-⇒ c d) = δ-⇒ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f δ-⊥ = δ-⊥
mapΔ₀ f (δ-∀∈ c) = δ-∀∈ (mapΔ₀ f c)
mapΔ₀ f (δ-∃∈ c) = δ-∃∈ (mapΔ₀ f c)

Δ₀ の水準は、帰納的に定義された階層の基底です。Σₙ の証人は、Δ₀ の証人か、一段下の Π の証人か、非有界な存在量化の列の証人のいずれかであり、Πₙ はその双対です。Σₙ と Πₙ は互いに定義し合うため、両者に対する改名の補題は mutual ブロックで一度に証明しなければなりません。

Δ₀ の上では、Σₙ の証人は Δ₀ の証人か、一段下の Π の証人か、非有界な存在量化の列の証人のいずれかであり、Πₙ はその双対です。二つの形式は互いに定義し合うため、輸送の補題は mutual ブロックで一度に証明されます。その形は mapΔ₀ と同じで、φ の Σₙ (それぞれ Πₙ) の証人から、同じ水準 k の mapFo f φ の証人を作ります。証人 σ-Δ₀ d は Δ₀ の証人を包み、mapΔ₀ f d が葉でそれを輸送します。証人 σ-Π p は交互の一段回を記録するもので、Π の補題を呼び出して処理します。両方の証明が相互再帰でなければならないのはまさにこのためです。

mutual
  mapΣₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Σₙ k φ → Σₙ k (mapFo f φ)
  mapΣₙ f (σ-Δ₀ d) = σ-Δ₀ (mapΔ₀ f d)
  mapΣₙ f (σ-Π p)  = σ-Π (mapΠₙ f p)

Σ の残りの場合 σ-∃ s は非有界な存在量化の列を扱います。mapFo f の下でも列は列のままだから、下位の証人 s は mapΣₙ 自身への再帰呼び出しで輸送されます。Π の側は正確な双対で、π-Δ₀ は mapΔ₀ に委ね、π-Σ は交互の回に対して mapΣₙ を呼びます。

  mapΣₙ f (σ-∃ s)  = σ-∃ (mapΣₙ f s)

  mapΠₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Πₙ k φ → Πₙ k (mapFo f φ)
  mapΠₙ f (π-Δ₀ d) = π-Δ₀ (mapΔ₀ f d)
  mapΠₙ f (π-Σ s)  = π-Σ (mapΣₙ f s)

最後の場合 π-∀ p は σ-Π と鏡像をなし、Π の側で交互の回を輸送します。停止性はここでは追加の議論ではなく構造的事実です。各再帰呼び出しは証人の構造的に小さい成分に適用され、mapΔ₀ が両方の再帰の葉にあります。得られるのは、有限の Lévy 階層全体に対する一つの輸送原理です。帰納的な証人によって記録された論理式の等級は、定数の改名の下で不変です。

  mapΠₙ f (π-∀ p)  = π-∀ (mapΠₙ f p)

まとめ

この章では、定数の改名の作用 mapFo f に関する二つの不変性を確立しました。意味論的には、⊨-map が定数の改名と充足関係の可換性を主張します。正確には、改名後の ι の下での評価は、改名前の ι ∘ f の下での評価と等しいということです。無パラメータの埋め込み embed-⊨ は、源の定数域が空である特別な場合として従います。構文的には、mapΔ₀、mapΣₙ、mapΠₙ が、論理式の量化子構造を証明する Lévy の証人が任意の改名に沿って輸送できることを主張します。合わせて、論理式はその意味と複雑さの証人を伴ったまま定数域の間を移動でき、これは後の章が空の定数域と構成可能階層の諸域との間を移るときに依拠する事実です。