Truth values

When a formula is evaluated, the result has to live somewhere: a type of truth values. This book travels to two places that want different answers. On the road to the constructible universe, propositions (hProp) serve as truth values; in the forcing part, truth values live in a complete Boolean algebra instead. So the answer is not hard-wired: the semantic codomain is a parameter, called a truth algebra, and everything built over it serves both journeys.

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

module Base.Truth where

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

The interface

The record below is a pure operation signature: it asks for eight operations and not a single law about them (no associativity, no distributivity, no lattice axioms). A law in an interface is a debt every instance must pay, and here nobody would ever collect it: everything the framework core builds over Ω treats the operations as black boxes, needing only congruence (equal inputs give equal outputs: the cong of the Prelude), which holds for any operations whatsoever. Laws are needed only by later theorems about particular models, and those work at a concrete instance, where the laws are theorems rather than assumptions. Staying law-free therefore costs nothing, and buys a cheap ticket of admission: a semantics joins the book by handing over eight operations, owing no proofs.

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

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

Symbol by symbol: ⊓ reads "and" (meet), ⊔ reads "or" (join), ⇒ reads "implies", ¬ reads "not", ⊤ reads "true", ⊥ reads "false"; ⋀ and its dual ⋁ are meet and join indexed by an arbitrary small type, and quantifier semantics will be given by exactly them. The fixity levels here deliberately match the object-language connectives introduced later, so mixed expressions read the same across layers.

Here the book's scope discipline for logic is laid down: these eight symbols are the book's only logic notation, and the Prelude deliberately exports none of them, so the only way they enter scope is by opening a truth algebra (open TruthAlgebra 𝕋). Whichever algebra a chapter opens, that is what its logic symbols mean: no symbol ever has two readings in one scope. Generic chapters open an abstract 𝕋; chapters on the propositional side open the canonical instance below.

The canonical instance: hProp

Propositions form a truth algebra. Everything in this sentence stands on univalence: that hProp is a set, and that the operations below are well defined on it, are theorems of the cubical library, not assumptions.

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

Three points worth keeping:

  1. The abstraction costs nothing. Record projections compute on a concrete instance, so TruthAlgebra._⊓_ (hPropAlgebra ℓ) is the library's _⊓_, definitionally. Working at the hProp instance is exactly as if the abstraction had never happened: whatever held by refl before still holds by

refl.

  1. The ⊥ field takes the level-polymorphic pair (⊥* , isProp⊥*), since the library's falsum is pinned to the bottom universe. This is also the whole relationship between the two symbols: the truth value ⊥ is the host type

⊥* packaged with its propositionality, so ⟨ ⊥ ⟩ is ⊥*. Write ⊥ where a truth value is expected and ⊥* where a type is expected; the two positions are not interchangeable, and the type checker polices the division.

  1. ⋁ is the propositionally truncated existential and ⋀ is a genuine Π type: the shape of constructive semantics. Chapters on the hProp side may still take proof devices (∃[ x ] … sugar, truncation eliminators) straight from the library; they are definitionally the same operations, not a second meaning.

A seat reserved for forcing

The forcing part of this book will provide the second instance: the regular-open Boolean completion of a forcing poset, with Ω a complete Boolean algebra. The record above will carry it unchanged, and the symbol family ∈ᴮ ≈ᴮ is already reserved for that day.

Recap

Truth values are a parameter: the operation-only record TruthAlgebra, whose eight symbols are the book's entire logic notation, with hPropAlgebra as the canonical, definitionally transparent instance. Next: the size vocabulary of impredicativity, and then the one classical principle that redeems it.