Semantics of FOL, Question about a technicality

51 Views Asked by At

In the semantics of predicate logic, the truth conditions for PL (predicate logic) sentences are defined, including quantified sentences. There, you always come across a cryptic condition, namely that $k$ is introduced as an arbitrary constant but must not occur in the formula $A(x)$. Then it is defined for instance:

$\forall x A(x)$ is true if $A(k)$ is true for every possible interpretation.

Why? Can you maybe show with a simple example?

1

There are 1 best solutions below

1
On BEST ANSWER

This is most likely taken from a description of the semantics of first-order logic. This will usually include something like the following for describing the semantics of $\lor$.

$$ M, \vec{x} \models \varphi(\vec{x}) \lor \psi(\vec{x}) \;\;\text{if and only if $M, \vec{x} \models \varphi(\vec{x})$ or $M, \vec{x} \models \varphi(\vec{x})$} $$

This saying what it means for a formula to be true for a specific structure $M$ where the free variables get their values from $\vec{x}$.

Note that the two formulas on the right hand side of the biconditional $\varphi(\vec{x})$ and $\psi(\vec{x})$ are strict subformulas of $\varphi(\vec{x}) \lor \psi(\vec{x})$. Also, note that formulas are fundamentally finite, so if you keep recursing downwards to strict subformulas this process will eventually bottom out.

For the semantics of the universal quantifier, you have a choice in terms of how to define it, although both ways are equivalent.

$$ M, \vec{x} \models [\forall z](\varphi(z, \vec{x})) \;\;\text{if and only if for all $\vec{v}$ extending $\vec{x}$ with a value for $z$, it holds that $M, \vec{v} \models \varphi(\vec{v})$ } $$

Or perhaps

$$ M, \vec{x} \models [\forall z](\varphi(\vec{x})) \\ \textit{if and only if} \\ \text{for all $M^*$ extending $M$ with a value for $k$, it holds that $M^*, \vec{x} \models \varphi(k, \vec{x})$} $$

In both of these cases, we have to deal with a technical problem and that is accidentally capturing a variable.

Suppose we are using the second strategy for talking about the meaning of the universal quantifier.

If our language already has a constant symbol $0$ in it, for example, when we consider the truth value of a well-formed formula headed by a universal quantifier, we can't replace the variable bound by that quantifier with $0$. It has to be a fresh symbol.

You get exactly the same problem in the other version, namely that when you get rid of a quantifier, you need to make sure that the bound variable is replaced with a fresh free variable.


As a quick example of why variable capture is a problem, consider the sentence $\varphi$ below. I'm using an existential quantifier here, but the same principle applies to universal quantifiers too.

$$ \varphi \;\;\text{is the sentence}\;\; [\exists a](a \neq k) $$

In prose, there is an $a$ that is not equal to $k$.

$\varphi$ is a sentence in the language $L_k = \{k\}$, with $k$ being a constant symbol. $k$ is not a free variable. It is the structure's responsibility to give $k$ a meaning.

So, let's suppose we have an $L_k$-structure $M$.

To be extra concrete, suppose the domain of $M$ is $\{0, 1\}$ and $k$ is interpreted as $0$.

Now, let's consider whether $M \models [\exists a](a \neq k)$ is true or not.

If we naively expand the recursive definition of $\models$, we get the following:

$$ M^* \models k \neq k \;\;\text{for some $M^*$ extending $M$} $$

Now, in any $L_k$ structure, $k \neq k$ is going to be false.

However, choosing $a$ to be $1$ would have made $a = k$ true in $M$, so something went wrong.

Basically, when we went to replace the bound variable $a$ with a constant symbol, we reused $k$ instead of introducing a fresh symbol.

Let's try it again with a fresh constant symbol $\ell$.

$$ M^* \models \ell \neq k \;\;\text{for some $M^*$ extending $M$} $$

This is true. We can send $\ell$ to $1$.