定数の改名

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

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

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

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

意味の水準

定数の改名は純粋に構文的な操作なので、意味を乱さないことを確認しなければならない。正確な主張は可換性である。任意の定数域の写像 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

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

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

⟦⟧-map (var i) γ = refl

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

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

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

⊨-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 ∷ γ))))

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

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

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

embed-⊨ = ⊨-map ⊥*-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 の証人が任意の改名に沿って輸送できることを主張する。合わせて、論理式はその意味と複雑さの証人を伴ったまま定数域の間を移動でき、これは後の章が空の定数域と構成可能階層の諸域との間を移るときに依拠する事実である。