一様な充足関係の内部グラフ

W を構成可能集合とし、論理式の定数が値を取るアルファベットと、環境の各成分が値を取る範囲の両方に用います。一様な充足関係の構成は、AllCodes W の各論理式符号に、その論理式を満たす環境の集合を割り当てます。本章では、この割り当て自身が L の内部にグラフを持つことを証明します。その要素は、論理式符号と対応する充足集合の順序対です。数学的な要点は置換公理です。一様なグラフ論理式は各符号の上で一意な値を持つので、集合 AllCodes W 上の像を一つの集合に集められます。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.SatisfactionGraphSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

このような構成可能集合 W を固定し、符号化に必要な命題のレベルで排中律を仮定します。順序対は周囲の階層で構成されますが、定義域、値、グラフはいずれも構成可能な論域 S に属します。

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

定義域 AllCodes W は、W のアルファベット上の整形式な論理式符号からなる構成可能集合です。論理式の構文がグラフ論理式の型を与え、依存対の外延性が後に、解とその充足証明からなる依存対の一意性を示します。

open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )

open import FOL.Syntax using ( Formula )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( _∷_; [] )

累積階層の所属は切り詰められた存在を表すため、任意のグラフ要素の最終的な特徴づけも切り詰められた形になります。論域 S は構成可能構造 𝒮ʟ のもので、その各要素は周囲の集合と構成可能性の証明からなります。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

open hPropStructure 𝒮ʟ using ( S )

ここで使う充足関係は、制限構造 𝒮ᵥ ↾ isL、すなわち構成可能構造 𝒮ʟ 上の内側の意味論です。定数はその論域上の恒等写像で解釈されます。したがって _⊨_ は、論理式が L で満たされることを直接に表し、本章では周囲の意味論との比較定理を使いません。

module AbsSF = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsSF using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

固定した W に対し、一様な構成の二つのパラメータをこの同じ集合で具体化します。したがって、符号のアルファベットと環境の値域はいずれも W です。Table.graph W W は AllCodes W のすべての要素に一様に適用される二項論理式であり、値の関係を記述します。Table.val W W x mx は、特定の符号 x におけるその一意な値です。

open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to MapGraph )

module SatGraph (W : S) where

論理式符号 x とその所属証明 mx に対し、この一意な値を valOf x mx と書きます。等式 valOf≡ は、それを定義上 Table.val W W x mx と同一視します。この記法により、グラフを集める対象の数学的な関数、すなわち定義域の要素をその充足集合へ送る関数が明確になります。

  opaque
    valOf : (x : S) → ⟨ fst x ∈ fst (AllCodes W) ⟩ → S
    valOf x mx = Table.val W W x mx

    valOf≡ : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → valOf x mx ≡ Table.val W W x mx
    valOf≡ x mx = refl

gr を一つの二項論理式 Table.graph W W とします。第一の自由な位置には充足集合の候補が、第二の位置には論理式符号が入ります。したがって、この論理式が定める関係は、符号と値の間のグラフ関係の候補です。

  private
    opaque
      unfolding valOf
      gr : Formula S 
      gr = Table.graph W W

二つの事実により gr は関数的になります。存在性は、表の値とその論理式符号について gr が成り立つことを述べ、証人は Table.funct から得ます。一意性は、同じグラフ論理式を満たす任意の y が valOf x mx に等しいことを述べ、表の一意性定理を対称にして得ます。

      defines' : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ (valOf x mx ∷ x ∷ []) ⊨ gr ⟩
      defines' x mx = Table.funct W W x mx .fst .snd

      only' : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ gr ⟩ → y ≡ valOf x mx
      only' x mx y h = sym (Table.val-uniq W W x mx y h)

各論理式符号について、gr の解の型は可縮です。その中心は、値 valOf x mx と、この値が gr を満たす証明 defines' からなる依存対です。別の解 (y , h) があれば、only' がまず二つの値を同一視します。残る成分は同じ命題の証明なので、Σ≡Prop が値の等しさを完全な依存対の等しさへ持ち上げます。この可縮性こそ、置換に必要な関数性の前提です。

    M : Recursion
    M = record
      { dom = AllCodes W ; graph = gr
      ; funct = λ x mx → (valOf x mx , defines' x mx)
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ gr)) (sym (only' x mx y h)) } }

これで、構成可能集合 AllCodes W 上の関数的関係 gr に置換を適用できます。順序対 pr (fst x) (fst (valOf x mx)) が一つの構成可能集合に集められ、これを pairs と書きます。したがってグラフは L の内部にあります。定義域と各値が構成可能であり、置換がそれらの対関係を一つの集合にするからです。

    module G = MapGraph M using ( F; F-in; pair-out )

  opaque
    pairs : S
    pairs = G.F

AllCodes W の各論理式符号は、グラフの順序対を一つ与えます。具体的に pairs-in は、基礎となる符号と基礎となる充足集合の順序対が pairs に属することを証明します。

    pairs-in : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ pr (fst x) (fst (valOf x mx)) ∈ fst pairs ⟩
    pairs-in = G.F-in

逆に、順序対 pr (fst x) (fst y) が pairs に属すると仮定します。置換像のファイバーは命題値なので、切り詰められた証人を、x が AllCodes W に属し、y がそこでの一意な値に等しいことを述べる依存対へ消去できます。これが pairs-out の切り詰めなしの結論です。

    pairs-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst pairs ⟩
              → Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst y ≡ fst (valOf x mx))
    pairs-out = G.pair-out

pairs の任意の要素が、最初から順序対として表示されているとは限りません。そのため、一般の像定理が与える特徴づけは切り詰められています。すなわち、論理式符号 x、所属証明 mx、その要素を x と値の順序対として表示する等式が単に存在します。これが pairs-shape であり、切り詰めは置換像への所属から受け継がれます。

    pairs-shape : (e : S) → ⟨ fst e ∈ fst pairs ⟩
                → ∥ Σ[ x ∈ S ] Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst e ≡ pr (fst x) (fst (valOf x mx))) ∥₁
    pairs-shape e h = MapGraph.F-out M (fst e) h

したがって pairs は、論理式の定数と環境の値がともに W から取られる一様な充足関係の内部グラフです。一様な値の存在と一意性が関係を関数的にし、置換がその関係を L の集合にし、三つの所属定理が、表示された順序対と任意の要素の両方についてこの集合を特徴づけます。