The object language

Part 1 begins. The host language has been speaking all along; this part builds the language that will be spoken about: the first-order language of set theory, with membership and equality as its only predicates, embedded deeply as an inductive datatype. The host is strictly more expressive, so the embedded Formula is never needed to say anything; it exists because later parts study formulas as mathematical objects: count them, code them, and ask what is definable by them. This chapter is pure syntax, owing nothing to truth values or structures.

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

module FOL.Syntax where

open import Base.Prelude

Terms and formulas

Some conventions first, used from here to the end of the book: t, u stand for terms, φ, ψ for formulas, n, m for numbers of free variables, and i, j for variables themselves. A term is either a constant or a variable. Which constants exist is a type parameter K, the constant domain; a variable is an element of Fin n, so a term with n free variables can only mention variables 0 to n - 1. Scoping is thereby intrinsic: an out-of-scope term is not forbidden, it is unrepresentable.

data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where
  con : K → Term K n         -- a constant, drawn from the domain K
  var : Fin n → Term K n     -- a de Bruijn variable

Formulas follow, indexed the same way. Every constructor of the object language carries an upper dot: a layer mark, and seeing it tells you at once that a symbol is syntax, not meaning. Reading them: ∈̇ is object membership, ≐ object equality, ∧̇ ∨̇ ⇒̇ ¬̇ ⊤̇ ⊥̇ the connectives, ∃̇ ∀̇ the quantifiers, and ∀̇∈, ∃̇∈ the bounded quantifiers, read "for every member of" and "for some member of". Binding is by de Bruijn: a quantifier takes a body with one more free variable, and variable 0 is the one just bound.

Two design decisions are visible in the constructor list. First, every connective is a primitive, and the reason is the semantics this language is headed for: each constructor will mean exactly one truth-algebra operation, and the algebra is constructive. A classical text can economize, spelling φ ∨ ψ as ¬ (¬ φ ∧ ¬ ψ), ∀ as ¬ ∃ ¬, φ ⇒ ψ as ¬ φ ∨ ψ, because classically the double negations cancel. Constructively they do not: ¬ ¬ P is weaker than P, so every one of those spellings would assign the connective the wrong meaning. ∨, ∀, ⇒ therefore must be constructors. The remaining three (⊤̇, ⊥̇, ¬̇) could be spelled honestly, say ¬̇ φ as φ ⇒̇ ⊥̇; they are primitive anyway so that every later structural recursion treats every connective alike, one clause each, no encoded special cases.

Second, the bounded quantifiers earn primitive seats even though ∀̇∈ t φ could be spelled with ∀̇. Had they been abbreviations, "every quantifier in φ is bounded" would be a fact about how φ happens to be spelled, invisible to anything that computes over φ's shape. As constructors, boundedness is shape: later chapters classify formulas by a datatype over their constructors, and certify "all quantifiers bounded" by a datatype that simply has no case for ∃̇ and ∀̇, an absence that can only speak if the bounded forms stand on their own. Formulas of that shape behave remarkably tamely across structures, a thread picked up once Part 2's model is on the table and carried into Part 4. The fixity table here is the book's single declaration for the object layer, each level chosen to match the truth-algebra operation it will be interpreted by.

infix   _≐_ _∈̇_
infixr  _∧̇_ _∨̇_
infixr  _⇒̇_
infix   ¬̇_

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where
  _∈̇_ _≐_     : Term K n → Term K n → Formula K n        -- atoms: membership, equality
  _∧̇_ _∨̇_ _⇒̇_ : Formula K n → Formula K n → Formula K n  -- binary connectives
  ¬̇_          : Formula K n → Formula K n                -- negation
  ⊤̇ ⊥̇         : Formula K n                              -- truth, falsity
  ∃̇_ ∀̇_       : Formula K (suc n) → Formula K n          -- quantifiers
  ∀̇∈ ∃̇∈       : Term K n → Formula K (suc n) → Formula K n  -- bounded quantifiers

The parameter K is where one syntax covers every use the book will make of it:

Sentences and parameter-free formulas

A sentence is a formula with no free variables; with intrinsic scoping this is a type, Formula K 0, not a side condition, and the book gives it no separate name. Parameter-free formulas restrict along a different, orthogonal axis. A constant is how an ambient set enters a formula as a parameter; here the constant domain is the empty type ⊥*, so there are no parameters at all, while free variables remain; like sentences, this is just a type, Formula ⊥* n, with no separate name. From the empty type anything follows, so a parameter-free formula can enter the syntax over any domain whatsoever; the map that performs the entry lives with the constant-transformation kit at the book's tail. Parameter-free formulas are no rivals of the working syntax but its companions: a syntax whose constants are all sets is too big to be counted or coded, so whenever a later part needs formulas as data, theories as sets of formulas, codes of formulas inside a model, it is the parameter-free formulas that get collected, their parameters fed through environments instead.

Recap

The object language is an inductive family Formula K n: constant domain as a parameter, scoping intrinsic through Fin, every constructor primitive and dotted. Around it: the parameter-free formulas, the data axis whose entry map arrives with the relabelling kit at the book's tail. Note what is absent: no substitution and no weakening operators anywhere. The design will keep it that way, and the little variable machinery the book does need arrives later in the book. First, formulas need something to talk about.