---
title: "The alphabet of formula codes"
module: L.Coding.CodeAlphabet
lang: en
site: "Bedrock"
description: "The alphabet of formula codes"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 64
canonical: https://bedrock.institute/en/L.Coding.CodeAlphabet.html
html: L.Coding.CodeAlphabet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeAlphabet.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, V.Coding, L.Constructible]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.CodeAlphabet.md, https://bedrock.institute/ja/L.Coding.CodeAlphabet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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`.

```agda
{-# 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`.

```agda
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`.

```agda
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.

```agda
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.

```agda
  ι∈ : (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.

```agda
  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.