Examples of interpretations: Manna’s book provides many insightful examples, some of which are summarized below. We focus on the notion of interpretations,
which, in case of first-order logic: (i) chooses domains for constants, predicates, and function symbols to range over, and (ii) assigns to them. Examples below will clarify.
Example 1: Consider the formula
Fmla1 = ∃F.F(a) = b ∧(∀x).[p(x) ⇒ F(x) = g(x, F(f(x)))]
We will now provide three distinct interpretations for it. Interpretation 1.
D = Nat
a = 0
b = 1
f = λx.(x = 0 → 0, x − 1)
g = *
p = λx.x > 0
Interpretation 2.
D = Σ∗
a = ε
b = ε
f = λx.(tail(x))
g(x,y) = concat(y,head(x))
p = λx.x = ε
Interpretation 3.
D = Nat
a = 0
b = 1
f = λx.x
g(x,y) = y 1
p = λx.x > 0
It is clear that under Interpretation 1, Fmla1 is true, because there indeed exists a function F, namely the factorial function, that makes the assertion true. It is also true under Interpretation 2, while it is false under Interpretation 3 (Exercise 18.4 asks for proofs). Hence, this formula is not valid — because it is not true under all interpretations.
Example 2: Consider the formula
Fmla2 = ∀P.P(a) ∧(∀x).[(x = a) ∧ P(f(x)) ⇒ P(x)]
⇒ (∀x.P (x))
We can interpret this formula suitably to obtain the principle of induction over many domains: for example, Nat, strings, etc.
