§ First order logic: Semantics
- M⊨F can be reads as M models F, or M makes true F ( M for model, F for formula).
§ Defining models for quantification
- We wish to define M⊨∀x,F(x)
- A first shot might be M⊨∃x,F(x) iff for every closed term t, M⊨F(t).
- However, see that intuitively, ∃x ranges over the denotational space , while closed terms range over the image of syntax in the denotation .
- For example, consider the language of nautrals, which we can interpret over naturals, nonnegative rationals, and reals. So let us think of the formula (F≡∃t,t+t=1). If we only allow t to take on closed terms, then see that since the closed terms of naturals are natural numbers, this will be false! But really, when interpreted over the integers, we want the formula to be true, since there is the real number 1/2 which witnesses the truth of (∃t,t+t=1). Thus, it is insufficient to range over closed terms, since the "image" of the closed terms in R is going to be N, but in fact, we have "more in R" than just the closed terms which are unreachable.
- So the correct notion of M⊨∃x,F(x) is to take M, extend with a constant symbol c, evaluate it to some m∈M, and call this Mmc. Then, we say that M⊨∃x,F(x) iff there exists an m∈M such that Mmc⊨F(c).
- See that this allows access to denotations, without needing a syntactic closed term.
- his fells close to the notion of adequacy , when the operational and denotational semantics agree. HackMD notes by Alexander Kurz