--- title: "The object language" module: FOL.Syntax lang: en site: "Bedrock" description: "The object language" stage: "First-order logic" reading_order: 6 canonical: https://bedrock.institute/en/FOL.Syntax.html html: FOL.Syntax.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Syntax.lagda.md prerequisites: [Base.Prelude] routes: [common-foundations] translations: [https://bedrock.institute/zh/FOL.Syntax.md, https://bedrock.institute/ja/FOL.Syntax.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The object language Set theory talks about sets, but to prove theorems about set theory itself, its statements must first become mathematical objects in their own right: expressions put together by explicit rules rather than informal convention. This chapter defines that object language by fixing the available constant names, the variable positions that may be referred to, and the rules for forming terms and formulas. The central decision concerns scope. The length of an expression's free-variable context is part of its type, so a reference beyond that context is impossible to write, not merely forbidden. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` Each formula is written against a finite context of free variables, and the length of that context, a natural number `n`, belongs to the formula's type. A variable is an element of `Fin n`, the type of positions `0` through `n - 1`. The point becomes visible when a quantifier is formed: its body has one more available variable position than the quantified formula itself, so the index grows from `n` to `suc n`. A term therefore cannot mention a variable outside its context, because no such position exists. ```agda module FOL.Syntax where ``` Variables determine what a formula may refer to; constants determine what it may name. Besides the context length `n`, a formula is formulated over an arbitrary type `K` of constant symbols, the **constant domain**. The type `K` is chosen once for the whole language, so the names available within a formula never change. These two choices are independent: `K` determines which parameters may be named, while `n` determines how many variable positions may be used. Enlarging one leaves the other unchanged. ```agda open import Base.Prelude ``` ## Terms and formulas Terms name the objects a formula can talk about, and formulas then assert things about those objects, so terms come first. A term is either a **constant**, a name drawn from `K`, or a **variable**, a position drawn from the `n` available positions. Formulas are built from such terms. They begin with the two atomic forms, membership and equality, and continue through the propositional connectives and the bounded and unbounded quantifiers. Throughout the book, `t` and `u` range over terms, `φ` and `ψ` over formulas, `n` and `m` over context lengths, and `i` and `j` over variable indices. Here `Term` is a family of types: choosing a type `K` and a number `n` yields a type `Term K n`, and a term never comes without both. Since a term is nothing more than a name from `K` or a number below `n`, the whole family lives at the same universe level `ℓ` as `K` itself. ```agda data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where ``` The constructor `con` takes an element `c : K` and treats it purely as a name. It has no meaning yet; only an interpretation can determine what it denotes. The constructor `var i` selects the position `i` from `Fin n`. With `n = 2`, the expressions `var 0`, `var 1`, and `con c` are terms of `Term K 2`, while `var 2` is unavailable: `Fin 2` has no element named `2`, so this is an expression that cannot be formed, rather than a term rejected by a later check. The number `n` determines which positions may be named, not how often they are used. The terms `con c` and `var 0` both have type `Term K 2` although neither mentions two variables, and a formula may use a single position more than once. Formulas will be built from terms of just this kind. ```agda con : K → Term K n var : Fin n → Term K n ``` Formulas are the assertions, as terms were the names. The smallest assertions are the atoms `_∈̇_` and `_≐_`: that one term is a member of another, or that two terms are equal. From atoms, the connectives `∧̇ ∨̇ ⇒̇ ¬̇ ⊤̇ ⊥̇` build compound statements, and the quantifiers `∃̇ ∀̇` range over all objects. Alongside them, `∀̇∈` and `∃̇∈` are the **bounded** quantifiers, read 'for every member of' and 'for some member of'. Every one of these symbols carries a small upper dot. The dot is a layer mark: `∈̇` speaks of membership as the object language states it, one layer removed from the membership relation of the surrounding theory, and a dotted symbol is always syntax rather than meaning. A quantifier binds a variable, and the syntax records this in the index. Its body has one more available variable position than the quantified formula, and position `0` in the body is the variable just bound. Which occurrences fall under the quantifier is thereby fixed by position alone, in the de Bruijn manner; no name is stored in the formula, so these formation rules need no convention for α-renaming or for distinguishing identically named variables. Nothing in the formula marks whether that extra position is actually used. Written inline, compound formulas need an agreed reading order, and these four lines settle it once for the whole object layer. Atoms and negation bind tightest, at levels 18 and 13. Conjunction and disjunction sit in the middle at level 12 and implication weakest at level 10, both pairs right-associative, so a chain `φ ⇒̇ ψ ⇒̇ θ` reads as `φ ⇒̇ (ψ ⇒̇ θ)`, the customary grouping for iterated implication. These are conventions of parsing, not additions to the language; with them, a nested formula reads the way ordinary mathematical prose does, and parentheses appear only where a different grouping is meant. This is the book's single declaration of the object layer's reading levels. ```agda infix 18 _≐_ _∈̇_ infixr 12 _∧̇_ _∨̇_ infixr 10 _⇒̇_ infix 13 ¬̇_ ``` The family `Formula` is indexed exactly like `Term`, by a constant domain `K` and a count `n` of available variable positions. The atoms `_∈̇_` and `_≐_` take two terms of `Term K n` and assert membership or equality between them. The propositional constructors go from formulas to formulas: `_∧̇_`, `_∨̇_` and `_⇒̇_` form conjunction, disjunction and implication, and `⊥̇` is falsity itself. None of them binds or releases a variable, which is why the index stays at `n`; quantifiers change it only when they bind a variable. That the connectives are constructors rather than abbreviations is a deliberate choice with a semantic reason. Formulas will eventually be read in the host's proposition type `hProp`, and each connective is interpreted by its corresponding direct operation there, not by reduction to other symbols. A classical text can economize, spelling `φ ∨̇ ψ` as `¬̇ (¬̇ φ ∧̇ ¬̇ ψ)`, `∀̇` as `¬̇ ∃̇ ¬̇`, or `φ ⇒̇ ψ` as `¬̇ φ ∨̇ ψ`, because classically double negations cancel. Constructively no such cancellation is generally available, and the substitutions would not deliver the intended meanings. This book therefore keeps `∨̇`, `⇒̇` and the quantifiers as constructors in their own right. ```agda data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where _∈̇_ _≐_ : Term K n → Term K n → Formula K n _∧̇_ _∨̇_ _⇒̇_ : Formula K n → Formula K n → Formula K n ⊥̇ : Formula K n ``` The types of the quantifiers state binding precisely. `∃̇_` and `∀̇_` take a body of type `Formula K (suc n)` and return a formula over `n` positions: the body has one more position at its disposal, position `0`, and that is the variable the quantifier binds. The extra position is available, not obliged; a body that never mentions it is a legitimate formula. The bounded forms `∀̇∈` and `∃̇∈` read as 'for every member of' and 'for some member of'. Their bound `t` is a term of the outer context, from `Term K n`, and quantification ranges over the members of `t`; the body is again `Formula K (suc n)`. The bounded quantifiers could have been spelled with the plain ones, and keeping them as constructors is a second deliberate choice, this time for a reason about syntax itself. Had `∀̇∈ t φ` been an abbreviation, the statement that every quantifier in `φ` is bounded would be a fact about how `φ` happens to be written, invisible to anything that computes over `φ`'s shape. As constructors, boundedness belongs to the shape. Later chapters classify formulas by a datatype with one case per constructor, and certify that all quantifiers are bounded by a datatype having no case for `∃̇` and `∀̇` at all; such a certificate is possible only because the bounded forms are given independently. Formulas of this shape behave well across structures, a thread the model chapters take up and the chapters on the constructible universe carry on. ```agda ∃̇_ ∀̇_ : Formula K (suc n) → Formula K n ∀̇∈ ∃̇∈ : Term K n → Formula K (suc n) → Formula K n ``` Negation is not a constructor but a defined symbol: `¬̇ φ` is, by definition, `φ ⇒̇ ⊥̇`. The definition has a visible consequence for computation. A function matching on formulas never encounters a negation as such; it encounters an implication whose consequent is `⊥̇`, and the clause prepared for `_⇒̇_` already covers the case. No separate clause for negation will ever be needed, not even in the semantics. ```agda ¬̇_ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n → Formula K n ¬̇ φ = φ ⇒̇ ⊥̇ ``` Truth is defined in the same style: `⊤̇` is `⊥̇ ⇒̇ ⊥̇`, the implication from absurdity to absurdity. Beyond the syntax, nothing is assumed, and the chapter imposes no law on how these symbols will later be read. Since the definitions unfold into constructors, an interpretation handles them by its existing clauses for `_⇒̇_`, with nothing special to arrange. Like the constructors, `¬̇_` and `⊤̇` take the universe level and `K` as implicit arguments, so the same two symbols serve at every constant domain and every variable count. ```agda ⊤̇ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n ⊤̇ = ⊥̇ ⇒̇ ⊥̇ ``` A single syntax serves every use the book will make of it; the freedom lies in the choice of the constant domain `K`: | choice of `K` | what it gives | |---|---| | the carrier of a structure | the working syntax: any set may appear in a formula as a parameter | | `⊥*` (no constants) | the **parameter-free formulas**: countable and codable independently of ambient parameters | | a restricted carrier | parameters confined to a class; the shape the constructible-universe development builds `L` with | ## Sentences and parameter-free formulas A sentence has no free variables; a parameter-free formula has no constants. The two restrictions are independent, and the difference matters as soon as formulas are coded and evaluated inside a model. A **sentence** is a formula with no free variables. Intrinsic scoping makes this a type, `Formula K 0`, rather than a side condition, and the book gives it no separate name. **Parameter-free formulas** restrict along the other axis: the constant domain is the empty type `⊥*`, so no parameter can be named, while free variables remain. This too is simply a type, `Formula ⊥* n`, with no separate name of its own. Because a function out of the empty type exists for every `K`, a parameter-free formula can be read over any constant domain, and the relabelling kit supplies exactly that map. Parameter-free formulas are useful when syntax must be enumerated without first enumerating the surrounding sets; parameters can then be supplied through an environment. They are not the only formulas that can be coded. The coding developed later also treats `Formula S n` directly, including constants drawn from the carrier `S`. ## Recap The inductive syntax records the constant domain, the length of the free-variable context, and quantifier scope in its types, so later chapters can transform formulas while Agda checks that variables stay in scope. The object language is the inductive family `Formula K n`: the constant domain as a parameter, scoping intrinsic through `Fin`, every constructor dotted. Alongside it stand the parameter-free formulas, with their entry map in the relabelling kit. Note what is absent: no substitution and no weakening appear anywhere. The design will keep it that way, and what little the book needs for handling variables arrives in later chapters. First, formulas need objects to talk about.