While reading the note "First-Order Logic in a Nutshell" from Lorenz Halbeisen (can't find it online, but it's also a section in his book Combinatorial Set Theory page 31-44.), I got confused by the remark at the end of the following paragraph:

Now, let $\mathsf T$ be an arbitrary set of $\mathcal L$-formulas. Then an $\mathcal L$-structure $\mathfrak A$ is a model of $\mathsf T$ if for every assignment $j$ in $\mathfrak A$ and for each formula $\varphi \in \mathsf T$ we have $(\mathfrak A,j) \models \varphi$, i.e. $\varphi$ holds in the $\mathcal L$-interpretation $I=(\mathfrak A,j)$. We usually denote models by bold letters like $\mathbf M$, $\mathbf N$, $\mathbf V$, et cetera. Instead of saying "$\mathbf M$ is a model of $\mathsf T$" we just write $\mathbf M \models \mathsf T$. If $\varphi$ fails in $\mathbf M$, then we write $\mathbf M \nvDash \varphi$, which is equivalent to $\mathbf M \vDash \neg \varphi$ (this is because for any $\mathcal L$-formula $\varphi$ we have either $\mathbf M \models \varphi$ or $\mathbf M \models \neg \varphi$).

What confused me initially is that he defined previously that a sentence is a formula with no free variables. To me, the above remark seems only valid if "formula" is replaced by "sentence" (because $\neg \forall x \varphi \Leftrightarrow \exists x \neg \varphi \not\Leftrightarrow \forall x \neg \varphi$). I then tried to read other texts about first order logic (for example in Wikipedia and SEP) in order to learn whether these definitions of sentence and formula are common. However, these texts are long, and instead of resolving my initial confusion, they turned up another question. They seem to define model only for an $\mathcal L$-interpretation $I=(\mathfrak A,j)$, but not for an $\mathcal L$-structure $\mathfrak A$. Lorenz Halbeisen on the other hand defines model only for an $\mathcal L$-structure $\mathfrak A$, but not for an interpretation.

Here is my main question:

When people talk about first order logic, it's common to use the notion of a model. But I'm confused now of whether this notion refers to an interpretation or to a structure. Is there a "common" definition of model in first order logic, and does this definition refer to an interpretation (instead of referring to a structure)?

And here is my initial question, which caused the confusion:

Is the mentioned remark invalid?

  • $\begingroup$ I think I found the main reason for my confusion now: The notion "interpretation" as used by Wikipedia and SEP doesn't include a variable assignment, contrary to the way "interpretation" is used by Lorenz Halbeisen. So I'm probably back to the point where I'm wondering whether some occurrences of "formula" have to be replaced by "sentence" in the cited paragraph. $\endgroup$ – Thomas Klimpel Apr 14 '12 at 13:33

It is, in the sense you are using the terms, structures and not interpretations. That is so also in the definition that you quote (I looked up the section 31-44 that you mentioned). And it is structure in the definition you quote. For recall that the definition says "in every $\mathcal{L}$-interpretation."

A definition of the type given here is quite common. Essentially, what it does is to define a formula (with free occurrences of variables) to be true if the universally quantified version of the formula is true.

For technical reasons, allowing free occurrences of variables is useful. We will be wanting to define truth of sentences $\varphi$ in $\mathbf{M}$ by induction on the complexity of $\varphi$. So for example we will want to say that the sentence $\exists x \psi(x)$ is true in the structure $\mathbf{M}$ if for every element $m$ of $M$, $\psi(m)$ is true in $\mathbf{M}$. That raises the immediate problem that $\psi(m)$ is not a sentence, you cannot put an object into a sentence.

There are two standard workarounds. One is to invent a new constant symbol for every element of $M$, extend the language $\mathcal{L}$ by adding these symbols. The other is to introduce assignments in the style that Halbeisen uses. If we do that, it is easier to work with formulas than with only those formulas that happen to be sentences.

  • $\begingroup$ OK, so my main problem is probably that his remark "... for any $\mathcal L$-formula $\varphi$ we have either $\mathbf M \models \varphi$ or $\mathbf M \models \neg \varphi$" is as valid as your example "...that the sentence $\exists x \psi(x)$ is true in the structure $\mathbf M$ if for every element $m$ of...". So let's introduce an universal quantifier into his remark, to see what happens: "... for any $\mathcal L$-formula $\varphi$ we have either $\mathbf M \models \forall x \varphi$ or $\mathbf M \models \forall x \neg \varphi$". So his remark is invalid, correct? $\endgroup$ – Thomas Klimpel Apr 14 '12 at 14:06
  • $\begingroup$ @ThomasKlimpel: Yes, I was concentrating on the various definitions, missed the error. At that point he should have switched to sentence. $\endgroup$ – André Nicolas Apr 14 '12 at 15:09
  • $\begingroup$ Thanks for your answer. My confusion is finally gone now, and everything seems to be consistent. (For example, the Generalisation inference rule seemed to be inconsistent with the "Soundness Theorem", because I used the wrong interpretation of model.) I suddenly like Halbeisen's note again. I found it very readable on first reading, but the second reading turned into a nightmare. I tried to prove some "obvious" formulas myself, but had to consult other resources with different definitions. Then I got confused about variable renaming, substitution, axiom schemas and meta-theorems. $\endgroup$ – Thomas Klimpel Apr 14 '12 at 19:39
  • 1
    $\begingroup$ Unfortunately, in logic perhaps more than elsewhere, there is a lack of uniformity. Everybody is going to the same place, but the roads are not the same. That often makes it difficult to answer questions on this site, since the choice of path is instructor-dependent. $\endgroup$ – André Nicolas Apr 14 '12 at 19:47
  • $\begingroup$ @André Nicolas: I think you have hit the nail on the head. I wonder if it would be helpful to have an answer the explains that at length, so that we can link to it from time to time. $\endgroup$ – Carl Mummert Apr 14 '12 at 21:05

We may have different "flavours" in the set-up of First-Order Predicate Calculus in Hilbert-style :

1) to use modus ponens as only inference rule (of course with suitable axioms);

in this way we have a "propositional" Deduction Theorem, without restrictions regarding free variables in the assumption to be discharged: see Herbert Enderton, A Mathematical Introduction to Logic (2nd ed Harcourt - 2001).

Alternatively :

2) to use also generalization rule;

in this way we need the usual restrictions on the Deduction Theorem for the Predicate Calculus, in order to avoid fallacies [to avoid that $\vdash P(x) \rightarrow \forall x P(x)$] : see Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997).

We may have also two approaches to the definition of the basic semantical relation :

$\vDash_{\mathfrak{A}} \varphi$, i.e. "$\varphi$ is true in $\mathfrak{A}$".

a) Enderton (page 83) states it as :

let $\varphi$ be a formula of our language,

$\mathfrak{A}$ a structure for the language,

let $s : V \rightarrow |\mathfrak{A}|$ a function from the set $V$ of all variables [of the language] into the universe $|\mathfrak{A}|$ of $\mathfrak{A}$.

Then we will define what it means for $\mathfrak{A}$ to satisfy $\varphi$ with $s$:

$\vDash_{\mathfrak{A}} \varphi[s]$.

As you can see, $\varphi$ is a formula; there is no restriction on having free variables in it. Then we will have the "special case" of sentences, i.e. closed formulas [page 87] :

for a sentence $\sigma$, either (a) $\mathfrak{A}$ satisfies $\sigma$ with every function $s$ from $V$ into $|\mathfrak{A}|$, or (b) $\mathfrak{A}$ does not satisfy $\sigma$ with any such function. If alternative (a) holds, then we say that $\sigma$ is true in $\mathfrak{A}$ (written $\vDash_{\mathfrak{A}} \sigma$) or that $\mathfrak{A}$ is a model of $\sigma$.

b) Dirk van Dalen in Logic and Structure (5th ed - 2013), page 64, "gives meaning" directly to sentences.

The fundamental clause is :

$| \forall x \varphi|_{\mathfrak{A}} := min \{ |\varphi [a/x]_\mathfrak{A} | : a \in |\mathfrak{A}| \}$.

Then, page 66 :

So far we have only defined truth for sentences of [the language] $L$. In order to extend $\vDash$ to arbitrary formulas we introduce a new notation.

Let $FV(\varphi) = \{z_1, . . . , z_k \}$, then $Cl(\varphi) := \forall z_1 . . . \forall z_k \varphi$ is the universal closure of $\varphi$.

We say that :

$\vDash_{\mathfrak{A}} \varphi$ iff $\vDash_{\mathfrak{A}} Cl(\varphi)$.

In this way, the semantics for open formulas is a "derived one".

Next option is about logical consequence: we may define it only for sentences (van Dalen, page 67 : semantic consequence), or for formulas in general (Eenderton, page 88, and Mendelson, page 65 : logically implies).

But the previous "ingredients" mix together.

Basically, when we define a proof system, we want that it is sound and complete. In the "most general" form, we expect that :

$\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$.

About soundenss: no problem, this is the easy task, while regarding completeness, we may have some "imperfection".

For example, in Mendelson's proof system we have generalization and the (standard) definition of derivation allows us to have :

$P(x) \vdash \forall x P(x)$.

Of course, M's proof system is sound; due to the restrictions on the Deduction Theorem, we cannot derive the (invalid) : $\vdash P(x) \rightarrow \forall x P(x)$.

But, according to M's semantics, we have : $P(x) \nvDash \forall x P(x)$.

Why ? Because the semantics give us : $B$ logically implies $A$ iff $B \rightarrow A$ is valid, and we know that $P(x) \rightarrow \forall x P(x)$ is not valid !

In conclusion, Mendelson is not licensed to state that, in general :

if $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$

and he does not state it ...


Regarding :

If $\varphi$ fails in $\mathbf M$ [i.e. not $\mathbf M \vDash \varphi$], then we write $\mathbf M \nvDash \varphi$, which is equivalent to $\mathbf M \vDash \lnot \varphi$ (this is because for any $\mathcal L$-formula $\varphi$ we have either $\mathbf M \vDash \varphi$ or $\mathbf M \vDash \lnot \varphi$)

it is definitely sentence in place of formula.

Consider again the "basic" semantic clause :

Then an $\mathcal L$-structure $\mathfrak A$ is a model of $\varphi$ if for every assignment $s$ in $\mathfrak A$ we have $(\mathfrak A,s) \models \varphi$, i.e. $\varphi$ holds in the $\mathcal L$-interpretation $(\mathfrak A,s)$.

Consider now the structure $\mathfrak A = (\mathbb N, 0, <)$ and the formula $\varphi$ :

$0 < x$.

Clearly, with the assignement $s : Var \mapsto \mathbb N$ such that $s(x)=0$ we have that :

$(\mathfrak A,s) \nvDash \varphi$;

thus, it is not true that for every assignment s in $\mathfrak A$, $\varphi$ holds in the $\mathcal L$-interpretation $(\mathfrak A,s)$. Thus, it is not true that $\mathfrak A$ is a model of $\varphi$ (i.e. that $\mathfrak A \vDash \varphi$).

Consider now its negation : $\lnot \varphi$, which is :

$\lnot (0 < x)$, i.e. $0 \ge x$.

With the assignement $s^* : Var \mapsto \mathbb N$ such that $s^*(x)=1$ we have :

$(\mathfrak A,s^*) \nvDash \lnot \varphi$.

Again, it is not true that $\mathfrak A \vDash \lnot \varphi$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.