Truth values

公式求值的结果必须落脚在某处：一个真值类型。本书要去的两个地方对此想要不同的答案：通往可构造宇宙的旅程，以命题 (hProp) 作真值即可；力迫部分则要求真值住在完备布尔代数里。所以这个答案不被焊死：语义值域是一个参数，称为真值代数，其上构建的一切两程通用。

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

module Base.Truth where

open import Base.Prelude
import Cubical.Functions.Logic as Logic
  using ( _⊓_; _⊔_; _⇒_; ¬_; ⊤; ∃[]-syntax; ∀[]-syntax )

接口

下面的 record 是纯运算签名：只索要八个运算，对它们不要求任何定律 (不要结合律、分配律，也不要任何格公理)。接口里的每条定律都是每个实例必须偿付的债务，而这里根本无人收账：框架核心在 Ω 上构建的一切都把这些运算当黑箱，只需要同余 (输入相等则输出相等，即序章的 cong)，而同余对任意运算都成立。定律只有后面关于具体模型的定理才需要，而那些定理本来就在具体实例上进行，届时定律是实例上的定理而非接口上的假设。零定律因此毫无代价，换来的是廉价的入场券：一个语义要加入本书，交出八个运算即可，不欠任何证明。

record TruthAlgebra (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Ω      : Type ℓ'
    isSetΩ : isSet Ω
    _⊓_ _⊔_ _⇒_ : Ω → Ω → Ω
    ¬_     : Ω → Ω
    ⊤ ⊥    : Ω
    ⋀ ⋁    : (A : Type ℓ) → (A → Ω) → Ω

  infixr 12 _⊓_ _⊔_
  infixr 10 _⇒_
  infix  13 ¬_

逐个符号：⊓ 读「且」(交)，⊔ 读「或」(并)，⇒ 读「蕴含」，¬ 读「非」，⊤ 读「真」，⊥ 读「假」；⋀ 与其对偶 ⋁ 是按任意小类型索引的交与并，量词语义正由它们给出。这里的优先级刻意与之后引入的对象语言联结词同级，跨层的混合表达式因此读法一致。

本书逻辑符号的作用域纪律在此立下：这八个符号是全书仅有的逻辑记号，序章刻意不导出其中任何一个，于是它们进入作用域的唯一方式就是打开某个真值代数 (open TruthAlgebra 𝕋)。一章打开哪个代数，它的逻辑符号就是那个代数的运算：任一作用域中，没有符号会有两种读法。泛型章节打开抽象的 𝕋；命题侧的章节打开下面的典范实例。

典范实例：hProp

命题构成一个真值代数。这句话的全部内容都站在 univalence 上：hProp 是集合、下列运算在其上良定义，这些在 cubical 库里都是定理而非假设。

hPropAlgebra : ∀ ℓ → TruthAlgebra ℓ (ℓ-suc ℓ)
hPropAlgebra ℓ = record
  { Ω      = hProp ℓ
  ; isSetΩ = isSetHProp
  ; _⊓_    = Logic._⊓_
  ; _⊔_    = Logic._⊔_
  ; _⇒_    = Logic._⇒_
  ; ¬_     = Logic.¬_
  ; ⊤      = Logic.⊤
  ; ⊥      = ⊥* , isProp⊥*
  ; ⋀      = λ A P → Logic.∀[]-syntax P
  ; ⋁      = λ A P → Logic.∃[]-syntax P }

三个值得记住的要点：

抽象零成本。record 投影在具体实例上按定义计算，所以 TruthAlgebra._⊓_ (hPropAlgebra ℓ) 定义性地就是库的 _⊓_。在 hProp 实例上工作与从未抽象过完全一样：凡此前由 refl 成立的等式，如今照旧由 refl 成立。
⊥ 字段取层级多态的对 (⊥* , isProp⊥*)，因为库的假固定在最底层宇宙。这也是两个符号之间的全部关系：真值 ⊥ 就是宿主类型 ⊥* 连同其命题性打包而成，故 ⟨ ⊥ ⟩ 就是 ⊥*。要真值的位置写 ⊥，要类型的位置写 ⊥*；两个位置不可互换，分工由类型检查器把守。
⋁ 是命题截断的存在量词，⋀ 是货真价实的 Π 类型：这正是构造性语义的形态。hProp 侧的章节仍可直接从库中取用证明手段 (∃[ x ] … 糖衣、截断消去子)：它们与本实例的字段定义性相同，不构成第二套含义。

为力迫预留的席位

本书的力迫部分将给出第二个实例：力迫偏序的正则开代数布尔完备化，Ω 是完备布尔代数。上面的 record 届时原样承接，符号族 ∈ᴮ ≈ᴮ 已为那一天预留。

小结

真值是一个参数：只含运算的 record TruthAlgebra，其八个符号就是全书的全部逻辑记号；hPropAlgebra 是典范且定义性透明的实例。接下来：非直谓性的尺寸词汇，与随后赎回它的那唯一经典原理。