The object language

Usually we write a claim about sets and ask whether it holds. Here we first ask a different question: what parts make up such a claim, and how can they be combined? Treating the written claim itself as a mathematical object, we build an object language.

We start with ways to refer to an object, then use those references to make claims, and finally add forms that say for every or there exists. At each step, the Agda code specifies which written forms are possible. What these forms mean, and whether a claim holds, comes later.

Some choices below may seem odd at first. Why prepare names for objects and number the places where objects can be inserted? Why settle the written forms before explaining their meaning, or treat some logical signs as basic and define others from them? These are worthwhile questions, but we need not answer them all at once. Mathematics does not force a single way to define an object language. Many familiar approaches can be shown to express much the same things, though each is convenient for different purposes. We use an established approach, choosing the balance we find best suited to the set theory developed in this book. The reasons for individual choices will become clearer as we interpret and use the expressions later.

Terms

Before saying that one object belongs to another, we need a way to refer to each object. We might choose a name in advance, or leave a numbered place to be filled when the expression is used. A written form that refers to one object in either way is called a term.

Let K be the type of names chosen in advance. Its elements are constant names, and K is the constant domain. Let n count the numbered places currently available. Together these places form a context; each place is a variable position. The type Fin n, introduced in the Prelude, contains precisely the positions from 0 through one less than n. Thus Term K n can record either way of referring to an object, without yet assigning a meaning to a name or position.

Definition (Term) For a universe level ℓ, a type K : Type ℓ, and a natural number n : ℕ, define the inductive type Term K n : Type ℓ.

data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where

Each k : K determines a term con k : Term K n; each i : Fin n determines a term var i : Term K n.

  con : K → Term K n
  var : Fin n → Term K n

These constructors produce ways to refer to objects, not the objects themselves. From a name k : K, con k is a term; from a position i : Fin n, var i is another. In a context of length two, positions 0 and 1 are available, but 2 is not. A term formed by con can nevertheless have type Term K 2: it uses no position at all. We write t and u for terms, and i and j for positions.

Formulas

Once we can refer to objects, we can write a claim about them. Such a written claim is a formula; we use φ, ψ and θ for formulas. The simplest ones say that one term belongs to another or that two terms are equal. These are atomic formulas. From them we can write and, or and if … then …, as well as the forms for every and some introduced below.

Before giving the construction rules, we set how an expression without parentheses is grouped. Membership and equality bind most tightly; then come the negation defined below, and and or, and finally if … then …. The last of these groups to the right: φ ⇒̇ ψ ⇒̇ θ is read as φ ⇒̇ (ψ ⇒̇ θ). These precedence declarations affect how a formula is read, not which formulas can be built.

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

The small dot on ∈̇, ∧̇ and the other logical signs distinguishes a written claim in this language from an Agda proposition about objects. For instance, t ∈̇ u records a claim about membership; it does not yet say that the objects referred to by t and u really stand in that relation. The meaning is supplied later.

Definition (Formula) For a universe level ℓ, a type K : Type ℓ, and a natural number n : ℕ, define the inductive type Formula K n : Type ℓ.

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where

The constructors _∈̇_ and _≐_ each take two terms of Term K n and yield a formula. The constructors _∧̇_, _∨̇_ and _⇒̇_ each take two formulas of Formula K n and yield another. The constructor ⊥̇ takes no arguments.

  _∈̇_ _≐_     : Term K n → Term K n → Formula K n
  _∧̇_ _∨̇_ _⇒̇_ : Formula K n → Formula K n → Formula K n
  ⊥̇           : Formula K n

The constructors ∃̇_ and ∀̇_ each take a formula in Formula K (suc n) and yield one in Formula K n. The constructors ∀̇∈ and ∃̇∈ also take a term in Term K n.

  ∃̇_ ∀̇_       : Formula K (suc n) → Formula K n
  ∀̇∈ ∃̇∈       : Term K n → Formula K (suc n) → Formula K n

The symbol ⊥̇ is intended to express an always-false claim. For now, the formation rules specify only which formulas can be written, not whether any formula holds. The forms for or (_∨̇_) and if … then … (_⇒̇_) have their own constructors, rather than being rewritten using not (¬̇_) and and (_∧̇_). Such rewritings can depend on additional logical rules that we have not assumed. Keeping the forms distinct lets us explain the meaning of each directly in the next chapters.

The constructors ∀̇_ (for every object) and ∃̇_ (there exists an object) differ from joining two finished claims: the claim that follows must have a place for the object under discussion. A quantifier opens one new position inside that claim. The figure follows the positions when one was already available outside.

The new position 0 represents a bound variable of the quantifier; the old positions represent free variables relative to it and shift up by one. In Agda, the body therefore has type Formula K (suc n), while the complete formula has type Formula K n. The body need not use its new position. Recording positions this way is called de Bruijn indexing: no variable names need to be stored or renamed, and a reference outside the available range cannot be formed.

The constructors ∀̇∈ and ∃̇∈ say for every member of and for some member of a set described by a term t. That term is written before the new position is opened, so it has type Term K n; only the claim following it uses the extended context. We keep these bounded quantifiers as separate constructors, allowing later chapters to recognize a formula that uses only these forms.

Definition (¬̇_) The constructors above give the basic forms of formulas; negation needs no additional one. We define ¬̇ φ as φ ⇒̇ ⊥̇. A function that inspects a formula therefore sees an implication, not a separate negation case. Under the intended interpretation, this implication expresses the refutation of φ.

¬̇_ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n → Formula K n
¬̇ φ = φ ⇒̇ ⊥̇

Definition (⊤̇) Truth is likewise defined, not primitive: ⊤̇ unfolds to ⊥̇ ⇒̇ ⊥̇. The future interpretation needs only its implication and falsity cases to give meaning to both derived symbols. These definitions work for every constant domain and context length.

⊤̇ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n
⊤̇ = ⊥̇ ⇒̇ ⊥̇

The same rules for forming terms and formulas work with different choices of K. If K is a structure’s carrier, constant symbols can name its elements. Restricting the type of names restricts the available constant parameters; choosing the empty type ⊥* leaves none. The number of variable positions is chosen independently through n.

Sentences and parameter-free formulas

There are two distinct ways to rule out names. A sentence has no free variables: its context length is zero, giving Formula K 0, but it may still contain constants. A parameter-free formula has no constants: its constant domain is ⊥*, giving Formula ⊥* n, but it may still have free variables. Neither needs a separate datatype or code name.

Because the empty type maps to any K, a parameter-free formula can be carried into any constant domain by the later constant-mapping operation. Such formulas can be enumerated without first enumerating the elements of a structure. This does not limit coding to parameter-free syntax: later chapters also code formulas whose constants come from a carrier.

Recap

The types record which constants and variable positions are available, while the quantifier constructors record how scope changes. They do not yet assign meanings to terms or formulas. To do that, we first need a structure in which their symbols can be interpreted.