論理式上の再帰による充足関係

module _ (B : S) where

cond : ∀ {n} → Formula S n → Formula S 

基礎集合 B を固定する。各論理式は、B 上の符号化された環境について一項の条件を定める。その条件を満たす環境を分出すると、その論理式の充足集合が得られる。

Sat : ∀ {n} → Formula S n → S
Sat {n} φ = sep (envSet B n) (cond φ)

論理式を充足する環境の集合は、その論理式のアリティの環境の集合全体から、条件を満たす環境を分出したものである。

Sat-mem : ∀ {n} (φ : Formula S n) (x : S)
        → (x ∈ˢ Sat φ) ≡ ((x ∈ˢ envSet B n) ⊓ ((x ∷ []) ⊨ cond φ))
Sat-mem {n} φ = sep-mem (envSet B n) (cond φ)

その所属の等式が記録するのは二つの要件である。環境が正しいアリティと値をもち、かつその論理式固有の条件を満たすことである。

cond (t ∈̇ u) =
  (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero))
        ∧̇ ( tmIs u zero (suc (suc zero))
        ∧̇ (var (suc zero) ∈̇ var zero) ))))

所属の原子式は二つの項目を束縛し、対象言語の所属を主張する。スロット suc zero で読まれる t の値が、スロット zero で読まれる u の値に属するというものである。どちらの値も環境のスロットに対して読まれる。

cond (t ≐ u) =
  (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero))
        ∧̇ ( tmIs u zero (suc (suc zero))
        ∧̇ (var (suc zero) ≐ var zero) ))))

相等の原子式は同じ形をし、所属の代わりに相等が置かれる。

cond (a ∧̇ b) =
  ((var zero ∈̇ con (Sat a)) ∧̇ (var zero ∈̇ con (Sat b)))

連言の条件は、その環境が二つの部分式の集合のどちらにも属すことを求める。どちらの集合も定数として名指される。

cond (a ∨̇ b) =
  ((var zero ∈̇ con (Sat a)) ∨̇ (var zero ∈̇ con (Sat b)))

選言の条件は、二つのうち少なくとも一方への所属を求める。

cond (a ⇒̇ b) =
  ((var zero ∈̇ con (Sat a)) ⇒̇ (var zero ∈̇ con (Sat b)))

含意の条件は、前件の集合への所属が後件の集合への所属を導くと言う。

cond ⊥̇ = ⊥̇

偽の条件は偽そのものである。これを満たす環境はない。

cond (∃̇ a) =
  (∃̇∈ (con B) (∃̇ ( consAtL zero (suc zero) (suc (suc zero))
                ∧̇ (var zero ∈̇ con (Sat a)) )))

非有界の存在量化子は台の上を動く。B のある要素 x が環境を拡張し、拡張の節が新しい列が環境であることを証明し、拡張された環境が部分式の集合に属する。

cond (∀̇ a) =
  (∀̇∈ (con B) (∀̇ ( consAtL zero (suc zero) (suc (suc zero))
                ⇒̇ (var zero ∈̇ con (Sat a)) )))

非有界の全称はその双対である。台の各要素は、加えられさえすれば、拡張された環境を部分式の集合の中へ落とし入れる。

cond (∀̇∈ t a) =
  (∀̇ ( tmIs t zero (suc zero)
    ⇒̇ ∀̇∈ (con B) ( (var zero ∈̇ var (suc zero))
                 ⇒̇ ∀̇ ( consAtL zero (suc zero) (suc (suc (suc zero)))
                     ⇒̇ (var zero ∈̇ con (Sat a)) ) ) ))

有界の全称は三層にわたって量化する。最も外側で、界の項の値 w をみずからのスロットから読み、そのような各 w の上で、台の要素 x が x ∈ B と x ∈ w の二つの守りつきで量化され、さらに各 x について、x で環境を拡張した e' が拡張の節の証明のもとで部分式の集合に属すことが要求される。ここで w は境界の補助のスロットにすぎず、部分式 a の環境は e' であり、環境にちょうど一つの項目を加えたものである。

cond (∃̇∈ t a) =
  (∃̇ ( tmIs t zero (suc zero)
    ∧̇ ∃̇∈ (con B) ( (var zero ∈̇ var (suc zero))
                 ∧̇ ∃̇ ( consAtL zero (suc zero) (suc (suc (suc zero)))
                     ∧̇ (var zero ∈̇ con (Sat a)) ) ) ))

有界の存在量化は、同じ三層を存在の主張として組み合わせる。まず界の項の値が読まれ、証人は台のうちその値に属する要素であり、その拡張された環境が部分式の集合に属することまで要求される。基礎と境界の二つの守りがともに保たれる。

条件の読み取り

一般の等式 Sat-mem は、環境集合への所属と条件の充足を分ける。連言、選言、含意、偽は cond の定義によって直接簡約され、補助的な同値は要らない。以下の補題が扱うのは残りの場合である。二つの原子の存在式と存在量化子に隠れた証人を展開し、あるいは全称量化子が与える関数を読み取る。これらは cond φ の充足だけを扱い、環境集合の連言は Sat-mem に残る。

CondAtom : ∀ {n} → Term S n → Term S n
         → (S → S → Type (ℓ-suc ℓ)) → S → Type (ℓ-suc ℓ)
CondAtom t u R z = Σ[ v ∶ S ] (Σ[ w ∶ S ]
  (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs t (suc zero) (suc (suc zero)) ⟩
   × (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs u zero (suc (suc zero)) ⟩ × R v w)))

二つの原子式では、条件は存在の主張であり、その展開された形が Σ 型の CondAtom である。t の値 v と u の値 w が、それぞれ項の読みを通して z の環境に対して読まれ、さらに二つの基底集合の間の関係 R が伴う。この型そのものは切り詰めを帯びず、切り詰められた形は後の補題に現れる。

cond∈-in : ∀ {n} (t u : Term S n) (z : S)
         → ∥ CondAtom t u (λ v w → ⟨ v .fst ∈ w .fst ⟩) z ∥₁
         → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩
cond∈-in t u z = map₁ (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })

所属の内向きの写しは、切り詰められた三つ組を、二つの量化子が期待する入れ子の証人の形に組み直す。消去が正当なのは、目標である外側の切り詰めそれ自体が命題だからで、内側の関係の性質のためではない。

cond∈-out : ∀ {n} (t u : Term S n) (z : S)
          → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩
          → ∥ CondAtom t u (λ v w → ⟨ v .fst ∈ w .fst ⟩) z ∥₁
cond∈-out t u z = rec₁ squash₁
  (λ { (v , hv) → map₁ (λ { (w , r) → v , (w , r) }) hv })

外向きの写しは、入れ子の証人を三つ組へと平らに戻す。議論の全体が切り詰めの内側にとどまる。

cond≐-in : ∀ {n} (t u : Term S n) (z : S)
         → ∥ CondAtom t u (λ v w → v .fst ≡ w .fst) z ∥₁
         → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩
cond≐-in t u z = map₁ (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })

相等の原子式が運ぶ関係は v .fst ≡ w .fst、すなわち基底集合の相等であり、その内向きの写しは所属の場合と一言一句変わらない。

cond≐-out : ∀ {n} (t u : Term S n) (z : S)
          → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩
          → ∥ CondAtom t u (λ v w → v .fst ≡ w .fst) z ∥₁
cond≐-out t u z = rec₁ squash₁
  (λ { (v , hv) → map₁ (λ { (w , r) → v , (w , r) }) hv })

その外向きの写しも所属の場合と同じで、関係を取り替えただけである。

CondQuant : ∀ {n} → Formula S (suc n) → S → Type (ℓ-suc ℓ)
CondQuant a z = Σ[ x ∶ S ] (⟨ x .fst ∈ B .fst ⟩
  × (Σ[ e' ∶ S ] (⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
                  × ⟨ e' .fst ∈ (Sat a) .fst ⟩)))

非有界の存在量化子では、展開された条件は Σ 型の CondQuant である。基礎の要素 x、拡張の節によって環境 z に x を加えた拡張であると証明される項目 e'、そして e' の部分式の集合への所属である。ここでも型は切り詰めを帯びず、切り詰めは補題で加えられる。

cond∃-in : ∀ {n} (a : Formula S (suc n)) (z : S)
         → ∥ CondQuant a z ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩
cond∃-in a z = map₁ (λ { (x , (x∈ , (e' , r))) → x , (x∈ , ∣ e' , r ∣₁) })

内向きの写しは、拡張のデータを、存在量化子自身が与える一つの切り詰められた証人へ折りたたむ。

cond∃-out : ∀ {n} (a : Formula S (suc n)) (z : S)
          → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ → ∥ CondQuant a z ∥₁
cond∃-out a z = rec₁ squash₁
  (λ { (x , (x∈ , hv)) → map₁ (λ { (e' , r) → x , (x∈ , (e' , r)) }) hv })

外向きには、入れ子になった二つの切り詰められた証人を順に展開する。どちらの目標も切り詰め、したがって命題なので、展開は正当である。

cond∀-in : ∀ {n} (a : Formula S (suc n)) (z : S)
         → ((x e' : S) → ⟨ x .fst ∈ B .fst ⟩
            → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩

許された各値と証明された拡張について、前提はその拡張が部分式の充足集合に属すことを与える。

            → ⟨ e' .fst ∈ (Sat a) .fst ⟩)
         → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩
cond∀-in a z k x x∈ e' hc = k x e' x∈ hc

非有界の全称では、展開された条件は関数である。基礎の各要素とその拡張に対して、その拡張での部分式の真理値を割り当てる。内向きと外向きは、量化子の二つの向きで読んだ同じ関数である。

cond∀-out : ∀ {n} (a : Formula S (suc n)) (z : S)
          → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩
          → ((x e' : S) → ⟨ x .fst ∈ B .fst ⟩

条件を外向きに読むとき、B から取った値と、それを付け加えて得た環境を保つ。

             → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
             → ⟨ e' .fst ∈ (Sat a) .fst ⟩)
cond∀-out a z h x e' x∈ hc = h x x∈ e' hc

ここに切り詰めは現れない。全称の充足は検証者を与えることで確かめられ、二つの方向はともにまさにそれを行うからである。

CondBnd : ∀ {n} → Formula S (suc n) → S → S → Type (ℓ-suc ℓ)
CondBnd a z w = Σ[ x ∶ S ] ((⟨ x .fst ∈ B .fst ⟩ × ⟨ x .fst ∈ w .fst ⟩)
  × (Σ[ e' ∶ S ]
      (⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
       × ⟨ e' .fst ∈ (Sat a) .fst ⟩)))

有界の量化子は一層加わる。条件が順に量化するのは、界の項の値 w、w の内側にある基礎の要素 x、そして環境 z に x を加えた拡張 e' である。e' は拡張の節が証明し、部分式の集合に属することが要求される。w の役割は補助である。境界の値を運ぶのは w であり、部分式の環境は e'、すなわち環境 z に要素 x をちょうど一つ加えたものである。

cond∃∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
          → ∥ (Σ[ w ∶ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
                           × ∥ CondBnd a z w ∥₁)) ∥₁
          → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩

有界の存在量化は証人を重ねる。外側の切り詰めは界の項の値 w の上にあり、その内側に CondBnd a z w の内側の切り詰め、すなわち台の要素とその拡張が収まる。

cond∃∈-in t a z = map₁
  (λ { (w , (hw , hx)) → w , (hw , map₁
    (λ { (x , ((x∈B , x∈w) , (e' , r))) → x , (x∈B , (x∈w , ∣ e' , r ∣₁)) })
    hx) })

最初の map₁ が w の上の外側の切り詰めを消去し、入れ子の map₁ が CondBnd の内側の切り詰めを消去して、要素と拡張を存在量化子自身の量化の中へ折りたたむ。どちらの目標も切り詰め、したがって命題なので、二つの消去が正当な理由は同じである。

cond∃∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
           → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩
           → ∥ (Σ[ w ∶ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
                            × ∥ CondBnd a z w ∥₁)) ∥₁

外向きの主張は、同じ二層の形をそのまま見せる。外側に境界の値、その内側に切り詰められた、台の要素とその拡張の記録である。

cond∃∈-out t a z = map₁
  (λ { (w , (hw , hx)) → w , (hw , rec₁ squash₁
    (λ { (x , (x∈B , (x∈w , hv))) → map₁
      (λ { (e' , r) → x , ((x∈B , x∈w) , (e' , r)) }) hv })
    hx) })

その証明はこの二層を順に展開する。行程のすべてが切り詰めの内側にとどまる。

cond∀∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
          → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
             → (x e' : S) → ⟨ x .fst ∈ B .fst ⟩ → ⟨ x .fst ∈ w .fst ⟩

二つの条件は、x が基礎集合 B と境界項の値 w の両方に属すことを要求する。

             → ⟨ (e' ∷ x ∷ w ∷ z ∷ [])
                  ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
             → ⟨ e' .fst ∈ (Sat a) .fst ⟩)
          → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩
cond∀∈-in t a z k w hw x x∈B x∈w e' hc = k w hw x e' x∈B x∈w hc

有界の全称の条件は、三層に量化された関数である。界の項の値 w のそれぞれに対して、w の内側の基礎の各要素 x と、環境 z に x を加えた拡張であると証明された各 e' について、e' での部分式の真理値を割り当てる。内向きの写しは、その関数を適用した姿である。

cond∀∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
           → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩
           → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩

結論は、同じ境界の値、基礎集合の要素、証明された一項の拡張にわたって量化する。

              → (x e' : S) → ⟨ x .fst ∈ B .fst ⟩ → ⟨ x .fst ∈ w .fst ⟩
              → ⟨ (e' ∷ x ∷ w ∷ z ∷ [])
                   ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
              → ⟨ e' .fst ∈ (Sat a) .fst ⟩)
cond∀∈-out t a z h w hw x e' x∈B x∈w hc = h w hw x x∈B x∈w e' hc