2. Models and interpretation
2.1. Two-element Boolean algebra
A Boolean algebra is a mathematical structure
($A, +, ⋅,\text'̄', 0, 1$) consisting of:
- a set $A$;
-
two binary opeartions '$+$' and '$⋅$' that are associative and commutative, and that are each
distributive over the other:
- $x+(y+z)=(x+y)+z$
- $x+y=y+x$
- $x⋅(y⋅z)=(x⋅y)⋅z$
- $x⋅y=y⋅x$
- $x+(y⋅z)=(x+y)⋅(x+z)$
- $x⋅(y+z)=(x⋅y)+(x⋅z)$
-
two constants '$0$' and '$1$' that are the identity elements of the two binary opeartions:
- $x+0=x$
- $x⋅1=x$
-
a unary operation ' $\text'̄'$ ', called the complement, such that:
- $x+x↖{-}=1$
- $x⋅x↖{-}=0$
For instance, the power set of any given set $U$, equiped with set union, set intersection, and set
complementation, forms a Boolean algebra. Constant $0$ is the empty set, and constant $1$ is
the set $U$ itself.
Consider the two-element set $\text'𝔹'=\{0,1\}$. It can be given a structure of Boolean algebra by defining addition, multiplication, and complement as follows:
Indeed, we may easily check by an exhaustive (but tedious) case analysis that the required equations
are satisfied.
We can think of 𝔹 in terms of truth values, $1$ standing for true, and $0$ for false. Consequently, we can provide the formulas with a notion of truth by interpreting them as members of 𝔹.
Consider the two-element set $\text'𝔹'=\{0,1\}$. It can be given a structure of Boolean algebra by defining addition, multiplication, and complement as follows:
| $x$ | $y$ | $x+y$ |
| $0$ | $0$ | $0$ |
| $0$ | $1$ | $1$ |
| $1$ | $0$ | $1$ |
| $1$ | $1$ | $1$ |
| $x$ | $y$ | $x⋅y$ |
| $0$ | $0$ | $0$ |
| $0$ | $1$ | $0$ |
| $1$ | $0$ | $0$ |
| $1$ | $1$ | $1$ |
| $x$ | $x↖{-}$ |
| $0$ | $1$ |
| $1$ | $0$ |
We can think of 𝔹 in terms of truth values, $1$ standing for true, and $0$ for false. Consequently, we can provide the formulas with a notion of truth by interpreting them as members of 𝔹.
2.2. Interpretation
The interpretation of a formula (i.e., whether it is considered as true or false) depends of the truth
values that are assigned to its atomic formulas. Take, for instance, $a ∧ b$, where
$a, b ∈ \sc A$. In order to know whether $a ∧ b$ is true or not, we must know whether $a$ and
$b$ are true or false.
Accordingly, the interpretation of a formula is defined with respect to a given basic interpretation that
assigns truth values to the atomic propositions. Such a basic interpretation, which is called a
model, is defined as follows.
A (propositional) model is a function from $\sc A$ into 𝔹.
Given a model $\sc M$, the interpretation of a formula $α$ (in notation $⟦α⟧^{\sc M}$)
associates to it a truth value.
Let $\sc M$ be a model. The interpretation of a formula with respect to $\sc M$ is inductively defined
as follows:
- $⟦a⟧^{\sc M} = \sc M(a)$, for $a ∈ \sc A$
- $⟦\text'⊥'⟧^{\sc M} = 0$
- $⟦\text'⊤'⟧^{\sc M} = 1$
- $⟦¬α⟧^{\sc M} = \ov {⟦α⟧^{\sc M}}$
- $⟦α∧β⟧^{\sc M} = ⟦α⟧^{\sc M}⋅⟦β⟧^{\sc M}$
- $⟦α∨β⟧^{\sc M} = ⟦α⟧^{\sc M}+⟦β⟧^{\sc M}$
- $⟦α→β⟧^{\sc M} = \ov {⟦α⟧^{\sc M}}+⟦β⟧^{\sc M}$
2.3. Satisfiability and validity
Let $α$ be a formula and $\sc M$ be a model. We say that $\sc M$ satisifies $α$
(in notation, $\sc M ⊨ α$) if and only if $⟦α⟧^{\sc M} = 1$.
In case there exists a model $\sc M$ that satisfies $α$, we say that $α$ is
satisfiable.
Finaly, if every model $\sc M$ satisfies $α$, we say that $α$ is valid, and we
write $⊨ α$.
An alternative definition of the notion of satisfaction of a formula $α$ by a model $\sc M$ is as follows:
An alternative definition of the notion of satisfaction of a formula $α$ by a model $\sc M$ is as follows:
- $\sc M ⊨ a$ if and only if $\sc M(a)=1$, for $a ∈ \sc A$
- $\sc M ⊨ \text'⊥'$ never holds true
- $\sc M ⊨ \text'⊤'$ always holds true
- $\sc M ⊨ ¬α$ if and only if not $\sc M ⊨ α$
- $\sc M ⊨ α∧β$ if and only if $\sc M ⊨ α$ and $\sc M ⊨ β$
- $\sc M ⊨ α∨β$ if and only if $\sc M ⊨ α$ or $\sc M ⊨ β$
- $\sc M ⊨ α→β$ if and only if $\sc M ⊨ β$ whenever $\sc M ⊨ α$
2.4. Truth tables
Given a model, Definition 4 provides a way of computing the semantics of a formula
(in terms of truth value). Does it also provide a way of deciding wheter a formula is
satisfiable or valid? A possible problem here is that there is generally an infinite (not even countable)
number of models. It is therefore impossible to check them all. Our intuition, however, tells us that
the meaning of a formula should only depends upon the meaning of the atomic proposition it contains.
This is indeed the case, as shown by the next proposition.
Let $α$ be a formula. The set of atomic propositions occurring in $α$ (in notation, $\text'atom'(α)$)
is inductively defined as follows:
- $\text'atom'(a) = \{a\}$, For $a ∈ \sc A$
- $\text'atom'(\text'⊥') = ∅$
- $\text'atom'(\text'⊤') = ∅$
- $\text'atom'(¬α) = \text'atom'(α)$
- $\text'atom'(α∧β) = \text'atom'(α) ∪ \text'atom'(β)$
- $\text'atom'(α∨β) = \text'atom'(α) ∪ \text'atom'(β)$
- $\text'atom'(α→β) = \text'atom'(α) ∪ \text'atom'(β)$
Let $α$ be a formula, and let ${\sc M_1}$ and ${\sc M_2}$ be models such that ${\sc M_1(a)} = {\sc M_2(a)}$
for every $a ∈ \text'atom'(α)$. Then $⟦α⟧^{\sc M_1} = ⟦α⟧^{\sc M_2}$.
The proof proceeds by induction on the definition of a formula.
-
$α = a$, for some $a ∈ \sc A$.
$⟦α⟧^{\sc M_1}$ $=$ $⟦a⟧^{\sc M_1}$ $=$ $\sc M_1(a)$ (by Definition 4) $=$ $\sc M_2(a)$ (by hypothesis) $=$ $⟦a⟧^{\sc M_2}$ (by Definition 4) $=$ $⟦α⟧^{\sc M_2}$ -
$α = \text'⊥'$.
$⟦α⟧^{\sc M_1}$ $=$ $⟦\text'⊥'⟧^{\sc M_1}$ $=$ $0$ (by Definition 4) $=$ $⟦\text'⊥'⟧^{\sc M_2}$ (by Definition 4) $=$ $⟦α⟧^{\sc M_2}$ -
$α = \text'⊤'$.
Similarly to Case 2, mutatis mutandis.
-
$α = ¬α_1$, for some formula $α_1$.
$⟦α⟧^{\sc M_1}$ $=$ $⟦¬α_1⟧^{\sc M_1}$ $=$ $\ov{⟦α_1⟧^{\sc M_1}}$ (by Definition 4) $=$ $\ov{⟦α_1⟧^{\sc M_2}}$ (by induction hypothesis) $=$ $⟦¬α_1⟧^{\sc M_2}$ (by Definition 4) $=$ $⟦α⟧^{\sc M_2}$ -
$α = α_1∧α_2$, for some formulas $α_1$ and $α_2$.
$⟦α⟧^{\sc M_1}$ $=$ $⟦α_1∧α_2⟧^{\sc M_1}$ $=$ $⟦α_1⟧^{\sc M_1}⋅⟦α_2⟧^{\sc M_1}$ (by Definition 4) $=$ $⟦α_1⟧^{\sc M_2}⋅⟦α_2⟧^{\sc M_1}$ (by induction hypothesis on $α_1$) $=$ $⟦α_1⟧^{\sc M_2}⋅⟦α_2⟧^{\sc M_2}$ (by induction hypothesis on $α_2$) $=$ $⟦α_1∧α_2⟧^{\sc M_2}$ (by Definition 4) $=$ $⟦α⟧^{\sc M_2}$ -
$α = α_1∨α_2$, for some formulas $α_1$ and $α_2$.
Similarly to Case 5, mutatis mutandis.
-
$α = α_1→α_2$, for some formulas $α_1$ and $α_2$.
Similarly to Case 5, mutatis mutandis.
As expected, the above proposition allows us to check the validity of a formula by considering
only a finite number of cases. Take, for instance, the following formula:
$(a ∧ (b ∨ ¬a)) → b$
It contains only two atomic propositions $a$ and $b$.
Accordingly, the set of models may be divided into four mutually exclusive subsets (in general, if the formula contains $n$ atomic
propositions, the set of models is divided into $2^n$ subsets):
| $M_{00}$ | $=$ | $\{\sc M ∈ {\text'𝔹'}^{\sc A} ∣ \sc M(a) = 0 \text' and ' \sc M(b) = 0\}$ |
| $M_{01}$ | $=$ | $\{\sc M ∈ {\text'𝔹'}^{\sc A} ∣ \sc M(a) = 0 \text' and ' \sc M(b) = 1\}$ |
| $M_{10}$ | $=$ | $\{\sc M ∈ {\text'𝔹'}^{\sc A} ∣ \sc M(a) = 1 \text' and ' \sc M(b) = 0\}$ |
| $M_{11}$ | $=$ | $\{\sc M ∈ {\text'𝔹'}^{\sc A} ∣ \sc M(a) = 1 \text' and ' \sc M(b) = 1\}$ |
Then, the interpretation of the formula may be computed for each case:
-
For $\sc M ∈ M_{00}$:
$⟦(a ∧ (b ∨ ¬a)) → b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+⟦b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+0$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}$ $=$ $\ov {⟦a⟧^{\sc M}⋅⟦b ∨ ¬a⟧^{\sc M}}$ $=$ $\ov {0⋅⟦b ∨ ¬a⟧^{\sc M}}$ $=$ $\ov 0$ $=$ $1$ -
For $\sc M ∈ M_{01}$:
$⟦(a ∧ (b ∨ ¬a)) → b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+⟦b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+1$ $=$ $1$ -
For $\sc M ∈ M_{10}$:
$⟦(a ∧ (b ∨ ¬a)) → b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+⟦b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+0$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}$ $=$ $\ov {⟦a⟧^{\sc M}⋅⟦b ∨ ¬a⟧^{\sc M}}$ $=$ $\ov {1⋅⟦b ∨ ¬a⟧^{\sc M}}$ $=$ $\ov {⟦b ∨ ¬a⟧^{\sc M}}$ $=$ $\ov {⟦b⟧^{\sc M}+⟦¬a⟧^{\sc M}}$ $=$ $\ov {0+⟦¬a⟧^{\sc M}}$ $=$ $\ov {⟦¬a⟧^{\sc M}}$ $=$ $\ov {\ov {⟦a⟧^{\sc M}}}$ $=$ $\ov {\ov 1}$ $=$ $\ov 0$ $=$ $1$ -
For $\sc M ∈ M_{11}$:
$⟦(a ∧ (b ∨ ¬a)) → b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+⟦b⟧^{\sc M}$ $=$ $\ov {⟦a ∧ (b ∨ ¬a)⟧^{\sc M}}+1$ $=$ $1$
The above computations may be presented in what is called a truth table:
| $a$ | $b$ | $¬a$ | $b ∨ ¬a$ | $a ∧ (b ∨ ¬a)$ | $(a ∧ (b ∨ ¬a)) → b$ |
| $0$ | $0$ | $1$ | $1$ | $0$ | $1$ |
| $0$ | $1$ | $1$ | $1$ | $0$ | $1$ |
| $1$ | $0$ | $0$ | $0$ | $0$ | $1$ |
| $1$ | $1$ | $0$ | $1$ | $1$ | $1$ |
The columns of this table are headed by the subformulas that occur
in the formula to be checked. In particular, the first columns correspond
to the atomic propositions, and the last column to the formula itself.
Truth values are assigned to the atomic propositions in such a way that each row of the table
corresponds to one of the possible cases. Then, the truth values assigned to the other columns
are computed from the values assigned to the immediate components of the formula heading the column,
using the elementary tables here below:
| $α$ | $¬α$ |
| $0$ | $1$ |
| $1$ | $0$ |
| $α$ | $β$ | $α∧β$ |
| $0$ | $0$ | $0$ |
| $0$ | $1$ | $0$ |
| $1$ | $0$ | $0$ |
| $1$ | $1$ | $1$ |
| $α$ | $β$ | $α∨β$ |
| $0$ | $0$ | $0$ |
| $0$ | $1$ | $1$ |
| $1$ | $0$ | $1$ |
| $1$ | $1$ | $1$ |
| $α$ | $β$ | $α→β$ |
| $0$ | $0$ | $1$ |
| $0$ | $1$ | $1$ |
| $1$ | $0$ | $0$ |
| $1$ | $1$ | $1$ |
Take for instance the entry corresponding to the fifth column and the second row (not counting the header as a row).
It is headed by formula $a ∧ (b ∨ ¬a)$, which is a conjunction. The immediate components of this formula
are $a$ and $b ∨ ¬a$, which are assigned $0$ and $1$, respectively. Then, by looking at the elementary table
for conjunction, we see that if $α$ is assigned $0$, and $β$ is assigned $1$, then $α∧β$
must be assigned $0$. This is indeed the value that we have in the second row of the fifth column.
Show that the following formulas are valid:
- $a → b → a$
- $(a → b → c) → (a → b) → a → c$
- $a → b → (a ∧ b)$
- $(a ∧ b) → a$
- $(a ∧ b) → b$
- $a → (a ∨ b)$
- $b → (a ∨ b)$
- $(a → c) → (b → c) → (a ∨ b) → c$
- $(a → b) → (a → ¬b) → ¬a$
- $¬¬a → a$
- $\text'⊥' → a$
- $a → \text'⊤'$
-
$a$ $b$ $b → a$ $a → b → a$ $0$ $0$ $1$ $1$ $0$ $1$ $0$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $c$ $b → c$ $a → b → c$ $a → b$ $a → c$ $(a → b) → a → c$ $(a → b → c) → (a → b) → a → c$ $0$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $0$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $0$ $0$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $0$ $1$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $0$ $0$ $0$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $a ∧ b$ $b → (a ∧ b)$ $a → b → (a ∧ b)$ $0$ $0$ $0$ $1$ $1$ $0$ $1$ $0$ $0$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $a ∧ b$ $(a ∧ b) → a$ $0$ $0$ $0$ $1$ $0$ $1$ $0$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $a ∧ b$ $(a ∧ b) → b$ $0$ $0$ $0$ $1$ $0$ $1$ $0$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $a ∨ b$ $a → (a ∨ b)$ $0$ $0$ $0$ $1$ $0$ $1$ $1$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $a ∨ b$ $b → (a ∨ b)$ $0$ $0$ $0$ $1$ $0$ $1$ $1$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $c$ $a → c$ $b → c$ $a ∨ b$ $(a ∨ b) → c$ $(b → c) → (a ∨ b) → c$ $(a → c) → (b → c) → (a ∨ b) → c$ $0$ $0$ $0$ $1$ $1$ $0$ $1$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $0$ $1$ $1$ $1$ $0$ $1$ $0$ $1$ $0$ $1$ $0$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $0$ $0$ $0$ $1$ $1$ $0$ $0$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $0$ $0$ $0$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ $1$ -
$a$ $b$ $a → b$ $¬b$ $a → ¬b$ $¬a$ $(a → ¬b) → ¬a$ $(a → b) → (a → ¬b) → ¬a$ $0$ $0$ $1$ $1$ $1$ $1$ $1$ $1$ $0$ $1$ $1$ $0$ $1$ $1$ $1$ $1$ $1$ $0$ $0$ $1$ $1$ $0$ $0$ $1$ $1$ $1$ $1$ $0$ $0$ $0$ $1$ $1$ -
$a$ $¬a$ $¬¬a$ $¬¬a → a$ $0$ $1$ $0$ $1$ $1$ $0$ $1$ $1$ -
$a$ $\text'⊥'$ $\text'⊥' → a$ $0$ $0$ $1$ $1$ $0$ $1$ -
$a$ $\text'⊤'$ $a → \text'⊤'$ $0$ $1$ $1$ $1$ $1$ $1$
2.5. Substitution and validity
The truth table method provides a way to check wheter a formula is valid or not. For instance, one may easily check that $a→a$ is a valid formula. Can we also apply this method to formula schemes, and consider, for instance, that $α→α$ is a valid scheme? Can we then conclude that $(a ∧ (¬b ∨ c))→(a ∧ (¬b ∨ c))$ is a valid formula because it obeys a valid scheme? We may have a strong intuition that this is the case. Intuition, however, is not enough. What we need is to establish this mathematically. To this end, we will prove the following property: let $α$ be a formula, and let $α^{*}$ be the formula obtained by replacing in $α$ all the occurrences of a given atomic proposition by some given arbitrary formula. Then, if $α$ is valid, so is $α^{*}$.We first define precisely what it means to replace all the occurrences of an atomic proposition by some formula.
The substitution of a formula $γ$ for an atomic proposition $c$ in a formula $α$
(in notation, $α[c≔γ]$)
is inductively defined as follows:
- $a[c≔γ] = a$, for $a ∈ \sc A$ and $a ≠ c$
- $c[c≔γ] = γ$
- $\text'⊥'[c≔γ] = \text'⊥'$
- $\text'⊤'[c≔γ] = \text'⊤'$
- $(¬α)[c≔γ] = (¬α[c≔γ])$
- $(α∧β)[c≔γ] = (α[c≔γ] ∧ β[c≔γ])$
- $(α∨β)[c≔γ] = (α[c≔γ] ∨ β[c≔γ])$
- $(α→β)[c≔γ] = (α[c≔γ] → β[c≔γ])$
It might seems strange that we stipulate, in the first clause of the above definition, that $a$ must
be different from $c$. This is needed because $a$ and $c$ are not atomic propositions but metavariables
ranging over atomic propositions. Consequently, it might be the case that both $a$ and $c$ stand for the
same atomic proposition.
Let $\sc M$ be a model, $b$ be an atomic proposition, and t be a truth value. We write $\sc M [b≔\text't']$ for the model such that:
Remark that we use the same symbol, namely '$≔$', in two different senses: once for the syntactic operation of substitution, and once for the semantic operation of modifying a model. In fact, these two operations are related, as stated by the following lemma.
Let $\sc M$ be a model, $b$ be an atomic proposition, and t be a truth value. We write $\sc M [b≔\text't']$ for the model such that:
$
\sc M [b≔\text't'] (a) =
\{\table \text't ', \text'if ' a=b; \sc M (a), \text'otherwise'
$
In words, $\sc M [b≔\text't']$ provides the same interpretation as $\sc M$, except possibly for
$b$, which is interpreted as t.
Remark that we use the same symbol, namely '$≔$', in two different senses: once for the syntactic operation of substitution, and once for the semantic operation of modifying a model. In fact, these two operations are related, as stated by the following lemma.
Let $α$ and $β$ be formulas, $b$ be an atomic proposition, and $\sc M$ be a model.
Then
$⟦α[b≔β]⟧^{\sc M}
=
⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$.
The proof proceeds by induction on the definition of a formula.
-
$α = a$, for some $a ∈ \sc A$.
1.1. $a≠b$
1.2. $a=b$$⟦α[b≔β]⟧^{\sc M}$ $=$ $⟦a[b≔β]⟧^{\sc M}$ $=$ $⟦a⟧^{\sc M}$ (by definition 6) $=$ $\sc M(a)$ (by definition 4) $=$ $\sc M[b≔⟦β⟧^{\sc M}](a)$ (because $a≠b$) $=$ $⟦a⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ (by definition 4) $=$ $⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$
$⟦α[b≔β]⟧^{\sc M}$ $=$ $⟦b[b≔β]⟧^{\sc M}$ $=$ $⟦β⟧^{\sc M}$ (by definition 6) $=$ $\sc M[b≔⟦β⟧^{\sc M}](b)$ $=$ $⟦b⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ (by definition 4) $=$ $⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ -
$α = \text'⊥'$.
$⟦α[b≔β]⟧^{\sc M}$ $=$ $⟦\text'⊥'[b≔β]⟧^{\sc M}$ $=$ $⟦\text'⊥'⟧^{\sc M}$ (by Definition 6) $=$ $0$ (by Definition 4) $=$ $⟦\text'⊥'⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ (by Definition 4) $=$ $⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ -
$α = \text'⊤'$.
Similarly to Case 2, mutatis mutandis.
-
$α = ¬α_1$, for some formula $α_1$.
$⟦α[b≔β]⟧^{\sc M}$ $=$ $⟦(¬α_1)[b≔β]⟧^{\sc M}$ $=$ $⟦¬α_1[b≔β]⟧^{\sc M}$ (by Definition 6) $=$ $\ov{⟦α_1[b≔β]⟧^{\sc M}}$ (by Definition 4) $=$ $\ov{⟦α_1⟧^{\sc M[b≔⟦β⟧^{\sc M}]}}$ (by induction hypothesis) $=$ $⟦¬α_1⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ (by Definition 4) $=$ $⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ -
$α = α_1∧α_2$, for some formulas $α_1$ and $α_2$.
$⟦α[b≔β]⟧^{\sc M}$ $=$ $⟦(α_1∧α_2)[b≔β]⟧^{\sc M}$ $=$ $⟦α_1[b≔β]∧α_2[b≔β]⟧^{\sc M}$ (by Definition 6) $=$ $⟦α_1[b≔β]⟧^{\sc M}⋅⟦α_2[b≔β]⟧^{\sc M}$ (by Definition 4) $=$ $⟦α_1⟧^{\sc M[b≔⟦β⟧^{\sc M}]}⋅⟦α_2[b≔β]⟧^{\sc M}$ (by induction hypothesis on $α_1$) $=$ $⟦α_1⟧^{\sc M[b≔⟦β⟧^{\sc M}]}⋅⟦α_2⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ (by induction hypothesis on $α_2$) $=$ $⟦α_1∧α_2⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ (by Definition 4) $=$ $⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ -
$α = α_1∨α_2$, for some formulas $α_1$ and $α_2$.
Similarly to Case 5, mutatis mutandis.
-
$α = α_1→α_2$, for some formulas $α_1$ and $α_2$.
Similarly to Case 5, mutatis mutandis.
The property we want to prove may be established as a direct consequence of the above lemma.
Let $α$ and $β$ be formulas, and $b$ be an atomic proposition.
If $⊨ α$ then $⊨ α[b≔β]$
We have to show that $α[b≔β]$ is satisified by every model.
Let $\sc M$ be an arbitray model.
| $⟦α[b≔β]⟧^{\sc M}$ | $=$ | $⟦α⟧^{\sc M[b≔⟦β⟧^{\sc M}]}$ | (by Lemma 2) |
| $=$ | $1$ | (because $α$ is valid, and therefore satisfied by every model) |
Remark that the converse of Proposition 3 does not hold. For instance,
we have that $((a→b)→b)[b≔¬a] = (a→¬a)→¬a$, and that
$(a→¬a)→¬a$ is a valid formula. It is not the case, however, that
$(a→b)→b$ is a valid formula.