Read this chapter directly, or use the interactive contents and dependency graph to choose another route.

Fix a proposition-valued structure 𝒮 : ZFStructureₕ ℓ. Its carrier supplies the objects under discussion, and its two relations interpret equality and membership.

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

We now have both a language for writing claims and a structure in which to read them. This chapter connects the two: first we specify which objects the names and numbered positions refer to, then interpret each formula as a proposition about those objects. Giving a claim this meaning is different from deciding whether it holds; the final section explains what excluded middle adds.

Open the fixed structure to use its carrier S and relations ≈ˢ and ∈ˢ directly. No set-theoretic axioms are assumed.

open ZFStructure 𝒮

Environments

A variable position tells us where to look for a value, but does not specify an object. An environment supplies this information by assigning a carrier element to each available position in the context. For a context of length n, we record the assignment as a vector γ : Vec S n; its entry at position i : Fin n is the value of the corresponding variable.

For example, in the environment a ∷ b ∷ [], position 0 holds a and position 1 holds b. A formula may use just one of these positions, refer to the same position several times, or use neither. The environment therefore records the values available when interpreting the formula, rather than one value for each variable occurrence; its length agrees with the context length, not the number of occurrences.

Interpreting terms and formulas

Constant names need values too. A constant interpretation is a function ι : K → S, assigning a carrier element to each name. Unlike variable values, these assignments remain fixed when a quantifier extends the environment. The submodule At fixes K : Type ℓc and ι : K → S for the definitions that follow.

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

Term evaluation

Definition (⟦_⟧) Term evaluation assigns to t : Term K n and γ : Vec S n an element ⟦ t ⟧ γ : S, read as the value of t under γ. A constant takes its value from ι; a variable takes its value from γ.

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

The common index n requires the environment to have exactly the length expected by the term. If K is the carrier itself, ι = id lets each element name itself. If K is empty, no constant case can arise; variable values still come from the environment. These choices are independent of the context length.

Satisfaction

Definition (_⊨_) The satisfaction relation assigns to γ : Vec S n and φ : Formula K n a proposition γ ⊨ φ : hProp ℓ. We read it as γ satisfies φ; an element of ⟨ γ ⊨ φ ⟩ is a proof that the formula holds under that assignment. Define this proposition recursively on the formula as follows.

infix 4 _⊨_
_⊨_ : ∀ {n} → Vec S n → Formula K n → hProp ℓ

For an atomic formula, evaluate the two terms and apply the corresponding relation of the structure: ∈̇ uses ∈ˢ, and ≐ uses ≈ˢ.

γ ⊨ t ∈̇ u = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
γ ⊨ t ≐ u = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ

For conjunction, disjunction and implication, interpret the two subformulas in the same environment, then combine the resulting propositions with the corresponding operation from the Prelude.

γ ⊨ φ ∧̇ ψ = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
γ ⊨ φ ∨̇ ψ = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
γ ⊨ φ ⇒̇ ψ = (γ ⊨ φ) ⇒ (γ ⊨ ψ)

Falsity always yields ⊥. An unbounded quantifier ranges over x : S and interprets its body in x ∷ γ, with the new value at the front. The existential asks that such a value merely exist; the universal requires the body to hold for every value.

γ ⊨ ⊥̇   = ⊥
γ ⊨ ∃̇ φ = ∃[ x ∶ S ] x ∷ γ ⊨ φ
γ ⊨ ∀̇ φ = ∀[ x ∶ S ] x ∷ γ ⊨ φ

For bounded quantifiers, evaluate the bound t in the original environment. Universal quantification requires membership in that value to imply the body; existential quantification requires membership and the body together. Only the body uses the extended environment.

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

These clauses give every formula a meaning without deciding its truth. The equality clause uses the supplied relation ≈ˢ, not necessarily Agda path equality. Disjunction and existential quantification use propositional truncation, so their proofs do not in general provide a branch or a witness that can be extracted as data. None of these clauses requires excluded middle.

Reading a quantified formula

The extra position in a quantifier's body now receives a value. Take the outer environment γ = a ∷ []. Prepending x produces x ∷ a ∷ []: the old value is preserved, while its index shifts. The figure shows the same position convention as in the object-language chapter, now with actual values supplied by an environment.

The extended environment puts the quantified value at position 0 and preserves the old value at position 1

For a concrete example, let the body be var zero ∈̇ var (suc zero). In the extended environment it means x ∈ˢ a. Prefixing ∀̇ therefore says that every carrier element belongs to a; prefixing ∃̇ says that some carrier element belongs to a. Neither is asserted to hold: the example identifies the proposition expressed by each formula.

For a bounded quantifier, the bound still refers to the old environment. In ∀̇∈ (var zero) φ, the bound denotes a, but the first position inside φ denotes x. This is why the code evaluates the bound in the original environment. Finally, negation and truth need no extra clauses: their definitions in the object language already expand into implication and falsity.

Predicates presented by formulas

So far we have started with a formula and obtained a proposition. We can also start with a given predicate predicate : A → hProp ℓ and supply a formula presentation for it. Here A indexes the cases under consideration; it need not be the carrier. One formula is kept fixed, while an environment is supplied for each a : A.

Definition (FormulaPredicate) Given A, K, ι and predicate, a formula presentation consists of an arity, a formula of that arity, an environment for each index, and a proof that its meaning equals the given predicate at every index. The constructor is presented.

record FormulaPredicate {ℓa ℓc} (A : Type ℓa) (K : Type ℓc)
                        (ι : K → S) (predicate : A → hProp ℓ)
    : Type (ℓ-max ℓa (ℓ-max ℓc (ℓ-suc ℓ))) where
  constructor presented

The fields record these four components in order. The arity arity counts available variable positions, just as the index n did above. In reading, the local module name I selects the interpretation At K ι; thus environment a I.⊨ formula is the formula's meaning in the environment assigned to a.

  field
    arity       : ℕ
    formula     : Formula K arity
    environment : A → Vec S arity
    reading     : (a : A) → let module I = At K ι in predicate a ≡ (environment a I.⊨ formula)

For example, fix a : S and consider the predicate λ x → x ∈ˢ a. It has a presentation using the formula var zero ∈̇ var (suc zero) and the environment x ∷ a ∷ [] at each x. The arity is two, even though the predicate has one argument: the environment supplies both that argument and the fixed object. Evaluating the formula gives the predicate directly, so reading can use refl.

The predicate and constant interpretation are parameters, not additional fields. The field reading supplies a path between two hProp ℓ values; along it, proofs of the given predicate can be transported to proofs of satisfaction, and conversely. Neither the formula nor its environments need be unique.

Decisions under excluded middle

Interpreting a formula yields a proposition, not automatically a proof or a refutation. With lem : LEM ℓ, however, we can apply excluded middle to that proposition. The hypothesis is needed here, not in the preceding definitions.

Lemma (decideSatisfaction) Given a constant interpretation, an environment and a formula, LEM ℓ yields a decision of the formula's satisfaction proposition.

Proof Form the proposition with At, then apply lem. Keeping the formula and environment as arguments specifies exactly which proposition is being decided.

decideSatisfaction : ∀ {ℓc n} {K : Type ℓc} (ι : K → S)
                   → LEM ℓ → (γ : Vec S n) → (φ : Formula K n)
                   → let module I = At K ι in Dec ⟨ γ I.⊨ φ ⟩
decideSatisfaction ι lem γ φ = lem (γ I.⊨ φ)
  where module I = At _ ι

The atomic cases make this correspondence concrete. Neither formula needs constant names, so take the empty constant domain ⊥* {ℓ} and its eliminator as the interpretation. The environment x ∷ y ∷ [] assigns the two objects to their respective positions.

Corollary (decideMembership) LEM ℓ decides membership between any two carrier elements.

Proof Apply the lemma to the atomic membership formula. Its two variables evaluate to x and y, so its meaning is precisely x ∈ˢ y.

decideMembership : LEM ℓ → (x y : S) → Dec ⟨ x ∈ˢ y ⟩
decideMembership lem x y =
  decideSatisfaction {K = ⊥* {ℓ}} (⊥*-rec {A = S}) lem
    (x ∷ y ∷ []) (var zero ∈̇ var (suc zero))

Corollary (decideEquality) LEM ℓ decides the structure's equality relation between any two carrier elements.

Proof Use the equality atom with the same constant domain and environment. Its meaning is x ≈ˢ y, rather than a claim about Agda path equality.

decideEquality : LEM ℓ → (x y : S) → Dec ⟨ x ≈ˢ y ⟩
decideEquality lem x y =
  decideSatisfaction {K = ⊥* {ℓ}} (⊥*-rec {A = S}) lem
    (x ∷ y ∷ []) (var zero ≐ var (suc zero))

Recap

Constant interpretations and environments give terms their values; the structure's relations and the logical operations then give formulas their meanings. Quantifiers vary the new first entry while preserving the outer assignment. FormulaPredicate records a formula presentation of a given predicate, and excluded middle separately supplies decisions of satisfaction. Defining meaning itself requires neither excluded middle nor set-theoretic axioms. The next chapter returns to the written formulas and classifies them by the arrangement of their quantifiers.