--- 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: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} module FOL.Syntax where ``` # The object language ```agda open import Base.Prelude ``` 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 ℓ`. ```agda 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`. ```agda 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. ```agda infix 18 _≐_ _∈̇_ infixr 12 _∧̇_ _∨̇_ infixr 10 _⇒̇_ infix 13 ¬̇_ ``` 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 ℓ`. ```agda 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. ```agda _∈̇_ _≐_ : 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`. ```agda ∃̇_ ∀̇_ : 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 lower arrow shows the old position `0` becoming `1` while still referring to $a$; the upper arrow shows the quantifier opening a new position `0` for $x$
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 `φ`. ```agda ¬̇_ : ∀ {ℓ} {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. ```agda ⊤̇ : ∀ {ℓ} {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. | names available | formula type | |---|---| | both | `Formula K n` | | constants only | `Formula K 0` | | positions only | `Formula ⊥* n` | | neither | `Formula ⊥* 0` | : Free variables and constant names are restricted independently 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.