The alphabet of formula codes

A statement about a constructible set W typically mentions members of W: to say, for instance, that some x in W satisfies a property, the formula carries x as a parameter. Internally, such parameters appear as constant symbols of a first-order language. The ambient coding of syntax, however, expects constants that are sets of the hierarchy V ℓ, not abstract references to members of an arbitrary set. So a bridge is needed: a language whose alphabet indexes the members of W, together with an embedding that gives each index its denotation as a set.

This chapter builds that bridge for a fixed W. The alphabet is the type of member indices of the underlying set of W; the embedding sends each index to the set it designates, and supplies a certificate that this set is a member of W. Relabeling constants along the embedding turns every term and formula over the alphabet into syntax over sets, to which the existing V-valued coding applies, yielding the term code ct and the formula code cd. Because the coding ignores arities, transporting a formula across an equality of arities leaves its code unchanged, as cd-subst records.

Everything in this chapter takes place at a single type-theoretic universe level ℓ, fixed once and used throughout. The hierarchy V ℓ of sets at this level is the target of the eventual coding, and the first-order language is the setting in which parameters live. The plan is uniform: given a constructible set W, read its members as constant symbols, name them by abstract indices, and transport each name to the set it denotes in V ℓ. Nothing in that plan depends on which W is chosen, so it is carried out for an arbitrary W.

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

open import Base.Prelude

module L.Coding.CodeAlphabet {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

The object-language syntax is generic in its alphabet. A type Formula K n of formulas over constants K and arity n never inspects what the constants are; it only arranges them into logical structure. Consequently, any function on the alphabet extends to a relabeling of syntax: mapping each constant through the function rewrites every occurrence while leaving connectives, quantifiers and variables untouched. Here the function will be the embedding of member indices into V ℓ, and the relabeled formulas will have sets as constants, which is precisely the input format of the set-valued syntax coding over the hierarchy. What remains is to choose the alphabet and the embedding so that the constants are genuinely the members of W.

open import FOL.Syntax using ( Formula; Term )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import V.Coding {ℓ} using ( module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ )

open import Cubical.Foundations.Prelude using ( J; substRefl )

Two distinctions organize the construction. First, a member of a set of the hierarchy is presented by an abstract index q in ⟪ a ⟫, and the embedding ⟪ a ⟫↪ sends that index to the set it designates; the index is a name, the value ⟪ a ⟫↪ q is the denotation in V ℓ, and the two roles are kept apart. Second, W is not an arbitrary set but an element of the carrier S of the constructible structure, so it comes with an underlying set fst W of the hierarchy and a constructibility certificate; this is what licenses reading its members as parameters of a language about constructible sets. The alphabet will be ⟪ fst W ⟫ itself, and the next section assembles these pieces into the codes ct and cd.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

open hPropStructure 𝒮ʟ using ( S )

Embedding constants and coding syntax

The section fixes a constructible set W as an element of the carrier S and asks how to code syntax over W as sets. Three steps compose: extract the type Ab of available constant symbols, embed each symbol into the hierarchy V ℓ with a certificate that it lies in W, and then apply the set-valued coding to the relabeled terms and formulas. The final lemma disposes of a bookkeeping issue arising because formulas are indexed by their arity.

An element W : S packages a set of the hierarchy with structure data; fst W is its underlying set. The type Ab is then ⟪ fst W ⟫, the type of indices for members of that set, and ι is the embedding ⟪ fst W ⟫↪ that sends each index to the member it designates inside V ℓ. So an inhabitant of Ab is exactly an available constant symbol, and ι computes its denotation as a set.

module Alphabet (W : S) where
  Ab : Type ℓ
  Ab = ⟪ fst W ⟫

  ι : Ab → V ℓ
  ι = ⟪ fst W ⟫↪

The membership certificate ι∈ says that for every constant symbol q, the set ι q genuinely is a member of fst W; it is read off from the library's equivalence between membership and the classified membership relation ∈ₛ. With the alphabet in place, cd and ct are now almost forced: mapFo ι and mapTm ι rewrite a formula or term by replacing each constant con q with con (ι q), and the brackets ⌜_⌝ and ⌜_⌝ᵗ from the hierarchy coding then package the result as a set. The logical skeleton of the formula survives the relabeling untouched, which is exactly why the coding can be reused.

  ι∈ : (q : Ab) → ⟨ ι q ∈ fst W ⟩
  ι∈ q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)

  cd : ∀ {n} → Formula Ab n → V ℓ
  cd ψ = VCode.⌜ mapFo ι ψ ⌝

  ct : ∀ {n} → Term Ab n → V ℓ

A formula of type Formula Ab n carries an arity n, and in dependent type theory that index is part of the type. If a proof later needs n and n' to be equal, it transports the formula along a path e : n ≡ n', and the transported formula is a different inhabitant syntactically even when the underlying formula is the same. The lemma cd-subst shows that this makes no difference for coding: cd applied to the transported formula equals cd applied to the original. The proof is by J on e, where the reflexive case holds because transporting along refl is the identity and substRefl makes that reduction explicit, leaving cong cd to equate the two applications.

  ct t = VCode.⌜ mapTm ι t ⌝ᵗ

  cd-subst : ∀ {n n'} (e : n ≡ n') (ψ : Formula Ab n) → cd (subst (Formula Ab) e ψ) ≡ cd ψ
  cd-subst {n} e ψ = J (λ n' e' → cd (subst (Formula Ab) e' ψ) ≡ cd ψ)
    (cong cd (substRefl {B = Formula Ab} ψ)) e

Recap

Alphabet W regards the members of a constructible set W as the constant symbols of a first-order language, embeds each of them into the ambient hierarchy with the certificate ι∈, and returns the resulting set codes of terms and formulas through ct and cd. Because the coding never inspects the arity, cd-subst guarantees that transporting a formula across an equality of arities does not change its code.