---
title: "Semantics"
module: FOL.Semantics
lang: en
site: "Bedrock"
description: "Semantics"
stage: "First-order logic"
reading_order: 8
canonical: https://bedrock.institute/en/FOL.Semantics.html
html: FOL.Semantics.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Semantics.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/zh/FOL.Semantics.md, https://bedrock.institute/ja/FOL.Semantics.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Semantics

The object language consists of symbols and rules for combining them, and so far none of the symbols denotes anything. What must be supplied before `∈̇` or `_≐_` can be read? A structure decides what the variables range over and what the two atomic predicates mean there; an interpretation gives each constant symbol its carrier element; an environment gives each available variable position its current value. Once these data are fixed, structural recursion assigns to every term a carrier element and to every formula a proposition. The whole chapter turns on one distinction, that between a symbol and its denotation: the sign `∈̇` belongs to the syntax, what it comes to mean is the relation `∈ˢ` of the structure, and the two live on different layers.

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

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Semantics {ℓ} (𝒮 : ZFStructure ℓ) where
```

Fix a structure `𝒮 : ZFStructure ℓ`, the model-theoretic data of the preceding chapter: a carrier `S` that is an h-set, together with an equality `≈ˢ` and a membership `∈ˢ`, each sending two carrier elements to a proposition in `hProp ℓ`. The interpretation of every formula will land in this same proposition universe, so a claim about sets becomes, quite literally, a proposition with proofs as its inhabitants. Nothing beyond these fields is used. The record `ZFStructure` itself contains no set-theoretic axioms, and defining the semantics requires none.

```agda
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

open ZFStructure 𝒮
```

The fields of the record are now in scope under their own names: `S` for the carrier, `∈ˢ` and `≈ˢ` for the relations, so `x ∈ˢ y` reads as the structure's membership proposition about `x` and `y`. The constructors of the object language are in scope as well, and each kind of symbol has a clear partner on the semantic side. A constant symbol needs a carrier element, fixed once by a function from the constant domain to `S`. A variable position needs a value that may change from use to use; an environment supplies it. An atomic formula needs one of the two relations. A connective or a quantifier needs no set theory at all: the logical operations on propositions from the Prelude, `⊓`, `⊔`, `⇒`, `∀[ x ] P x` and `∃[ x ] P x`, take their places. Interpretation is compositional: the meaning of a term or formula is determined from its constructor and the meanings of its immediate parts.

## Environments

A term of arity `n` may refer to the positions `0` through `n - 1`, and an **environment** `γ` assigns a carrier element to each of them. An environment in `S ^ 2` has two entries, available to `var zero` and `var (suc zero)`; a particular term or formula may use either, both, or neither. The length `n` therefore bounds the positions that are available rather than counting the variables that actually occur. Binding works on the same principle. When a quantifier considers a candidate from the carrier, the environment is extended by placing that element in front, and the body addresses it at position `zero`.

The type of an environment is written `S ^ n`, matching the traditional superscript $S^n$; `_^_` reads "power" and is pure notation. It is defined as `Vec A n`, an ordered vector whose length is part of its type. Here a dependent type does real work: the arity of a formula and the length of an environment cannot disagree, for a mismatch would not be a well-formed combination at all. The operation `lookup` returns the entry at a position in `Fin n`, and `x ∷ γ` prepends one entry, moving the previous ones to the successor positions.

```agda
infixl 30 _^_

_^_ : ∀ {ℓ''} → Type ℓ'' → ℕ → Type ℓ''
A ^ n = Vec A n
```

## Evaluation and satisfaction

Two judgments carry the semantics. Write `⟦ t ⟧ γ` for the carrier element denoted by the term `t` under the environment `γ`, and `γ ⊨ φ` for the proposition stating that the formula `φ` holds under `γ`. Both are defined relative to a fixed constant interpretation `ι : K → S`: constants receive their values from `ι`, while variables keep varying with `γ`. The separation matters as soon as quantifiers appear: binding changes the values of the variables, and the constant symbols keep their denotations.

The interpretation and the environment answer two different questions. The constant `con k` denotes `ι k`, whichever environment is supplied; the variable `var i` denotes `lookup i γ`, whichever interpretation is fixed. Thus the environment enters term evaluation only in the variable case, while the meanings of the constant symbols remain fixed by `ι`. These two cases exhaust term evaluation.

Fix a constant domain `K` and an interpretation `ι : K → S`. At this fixed interpretation, term evaluation sends a term and an environment to an element of `S`, while satisfaction sends a formula and an environment to a proposition. Satisfaction is defined by structural recursion: atomic formulas use the two relations of the structure, connectives use the propositional operations of the Prelude, falsity uses the empty proposition, and quantifiers range over the carrier. In a bounded quantifier, the denotation of the bound determines the membership condition on the quantified element.

```agda
module At {ℓc} (K : Type ℓc) (ι : K → S) where
```

Two definitions carry the section, and their types say what they are. Evaluation `⟦_⟧` maps a term and an environment to a carrier element. Satisfaction `_⊨_` maps an environment and a formula to a proposition in `hProp ℓ`, that is, to a type any two of whose elements are equal; the inhabitants of such a type are its proofs. Satisfaction is therefore not a bare verdict but a proposition, and the definition computes, for each formula and environment, exactly which proposition is meant. The arity `n` appears in both types, so only an environment of matching length can be applied to a formula: the earlier discipline between formula and environment is now enforced by the types themselves.

```agda
  ⟦_⟧ : ∀ {n} → Term K n → S ^ n → S
  ⟦ con k ⟧ γ = ι k
  ⟦ var i ⟧ γ = lookup i γ

  infix 6 _⊨_

  _⊨_ : ∀ {n} → S ^ n → Formula K n → hProp ℓ
```

An atomic membership evaluates its two terms and hands them to the structure: the claim becomes the structure's membership proposition about the two denotations. The equality atom does the same with `≈ˢ`. Here, at last, the dotted symbol means something: `∈̇` is read as `∈ˢ`, one layer down from the syntax. The propositional clauses stay entirely on the host side. Conjunction is interpreted by `⊓`, disjunction by `⊔`, implication by `⇒`, each an operation on propositions. A proof of a conjunction is a pair of proofs; a proof of an implication is a function turning a proof of the antecedent into a proof of the consequent. These three clauses use no set theory at all; they are the propositional logic of the host, applied to the propositions denoted by the subformulas.

```agda
  γ ⊨ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
  γ ⊨ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
  γ ⊨ (φ ∧̇ ψ)  = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
  γ ⊨ (φ ∨̇ ψ)  = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
  γ ⊨ (φ ⇒̇ ψ)  = (γ ⊨ φ) ⇒ (γ ⊨ ψ)
```

Falsity needs no environment: `⊥̇` is read as the empty proposition `⊥`. The quantifiers are where the carrier finally enters. The unbounded `∃̇ φ` expresses existential quantification over the carrier: the proposition that some element `x` of `S` makes the body hold at the extended environment `x ∷ γ`. Its twin `∀̇ φ` expresses universal quantification, and a proof of it is a function assigning to each `x : S` a proof of the body at `x ∷ γ`. Inside the body, position `zero` holds the candidate `x`, while the entries of `γ` have moved to the successor positions; a variable free in the outer formula is read from the tail. By propositional truncation, the existential records that such an element exists without carrying the element as data.

The bounded forms add one ingredient: membership in the denotation of the bound. `∀̇∈ t φ` demands that membership in `⟦ t ⟧ γ` imply the body, so every member of `⟦ t ⟧ γ` satisfies `φ`; `∃̇∈ t φ` asks for an element that is a member and satisfies the body. Note where each environment is used. The bound `t` lies outside the new binder and is evaluated in the original `γ`; only the body sees the extension `x ∷ γ`. These two clauses are precisely the semantic content of the readings "every member of `t` satisfies `φ`" and "some member of `t` satisfies `φ`".

```agda
  γ ⊨ ⊥̇        = ⊥
  γ ⊨ (∃̇ φ)    = ∃[ x ∶ S ] (x ∷ γ) ⊨ φ
  γ ⊨ (∀̇ φ)    = ∀[ x ∶ S ] (x ∷ γ) ⊨ φ
  γ ⊨ (∀̇∈ t φ) = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ φ)
  γ ⊨ (∃̇∈ t φ) = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ)
```

## Recap

Meaning is compositional. A term denotes a carrier element, determined by the constant interpretation and the environment. A formula of arity `n` determines a function `S ^ n → hProp ℓ`, whether or not it uses every available position. The atoms consult the structure's two relations; the connectives apply the propositional operations of the host; the quantifiers let a fresh front position range over the carrier, and the bounded forms test membership in the denotation of the bound outside the extension while interpreting the body inside it. Every clause is one step of structural recursion. The construction uses the carrier `S` and the two relations `∈ˢ` and `≈ˢ`; it does not use the proof `isSetS` or any set-theoretic axiom.