Syntax and Semantics

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

How to use Read

This page follows the chapter in source order. Equations are native MathML, so compatible screen readers and braille systems can navigate their internal structure. Every equation has an exact source-line link.

Propositional Logic: introduction to this part

This part contains material on classical propositional logic. The first chapter is relatively rudimentary and just lists definitions and results, many proofs are not carried out but are left as exercises. The material on proof systems and the completeness theorem is included from the part on first-order logic, with the “FOL” tag set to false. This leaves out everything related to predicates, terms, and quantifiers, and replaces talk of structures $\Struct{M}$ source 17 with talk about valuations $\pAssign{v}$ source 18.

It is planned to expand this part to include more detail, and to add further topics and results, such as truth-functional completeness.

Introduction

Propositional logic deals with formulas that are built from propositional variables using the propositional connectives $\lnot$ source 15, $\land$ source 15, $\lor$ source 15, $\lif$ source 15, and $\liff$ source 15. Intuitively, a propositional variable $p$ source 16 stands for a sentence or proposition that is true or false. Whenever the “truth value” of the propositional variable in a formula is determined, so is the truth value of any formulas formed from them using propositional connectives. We say that propositional logic is truth functional, because its semantics is given by functions of truth values. In particular, in propositional logic we leave out of consideration any further determination of truth and falsity, e.g., whether something is necessarily true rather than just contingently true, or whether something is known to be true, or whether something is true now rather than was true or will be true. We only consider two truth values true ( $\True$ source 27) and false ( $\False$ source 27), and so exclude from discussion the possibility that a statement may be neither true nor false, or only half true. We also concentrate only on connectives where the truth value of a formula built from them is completely determined by the truth values of its parts (and not, say, on its meaning). In particular, whether the truth value of conditionals in English is truth functional in this sense is contentious. The material conditional $\lif$ source 34 is; other logics deal with conditionals that are not truth functional.

In order to develop the theory and metatheory of truth-functional propositional logic, we must first define the syntax and semantics of its expressions. We will describe one way of constructing formulas from propositional variables using the connectives. Alternative definitions are possible. Other systems will choose different symbols, will select different sets of connectives as primitive, and will use parentheses differently (or even not at all, as in the case of so-called Polish notation). What all approaches have in common, though, is that the formation rules define the set of formulas inductively. If done properly, every expression can result essentially in only one way according to the formation rules. The inductive definition resulting in expressions that are uniquely readable means we can give meanings to these expressions using the same method—inductive definition.

Giving the meaning of expressions is the domain of semantics. The central concept in semantics for propositional logic is that of satisfaction in a valuation. A valuation $\pAssign{v}$ source 54 assigns truth values $\True$ source 55, $\False$ source 55 to the propositional variables. Any valuation determines a truth value $\pValue{v}(!A)$ source 56 for any formula $!A$ source 57. A formula is satisfied in a valuation $\pAssign{v}$ source 58 iff $\pValue{v}(!A) = \True$ source 58—we write this as $\pSat{v}{!A}$ source 59. This relation can also be defined by induction on the structure of $!A$ source 60, using the truth functions for the logical connectives to define, say, satisfaction of $!A \land !B$ source 61 in terms of satisfaction (or not) of $!A$ source 62 and $!B$ source 62.

On the basis of the satisfaction relation $\pSat{v}{!A}$ source 64 for sentences we can then define the basic semantic notions of tautology, entailment, and satisfiability. A formula is a tautology, $\Entails !A$ source 67, if every valuation satisfies it, i.e., $\pValue{v}(!A) = \True$ source 68 for any $\pAssign{v}$ source 68. It is entailed by a set of formulas, $\Gamma \Entails !A$ source 69, if every valuation that satisfies all the formulas in $\Gamma$ source 70 also satisfies $!A$ source 70. And a set of formulas is satisfiable if some valuation satisfies all formulas in it at the same time. Because formulas are inductively defined, and satisfaction is in turn defined by induction on the structure of formulas, we can use induction to prove properties of our semantics and to relate the semantic notions defined.

Propositional formula

Formulas of propositional logic are built up from propositional variables and the propositional constant $\lfalse$ source 16 using logical connectives.

A denumerable set $\PVar$ source 21 of propositional variables $\Obj p_0$ source 21, $\Obj p_1$ source 22, … The propositional constant for falsity $\lfalse$ source 23.
The logical connectives: , $\lnot$ source 27 (negation) , $\land$ source 28 (conjunction) , $\lor$ source 29 (disjunction) , $\lif$ source 30 (conditional)
Punctuation marks: (, ), and the comma.

We denote this language of propositional logic by $\Lang L_0$ source 35.

In addition to the primitive connectives introduced above, we also use the following defined symbols:

, $\liff$ source 45 (biconditional)

, $\ltrue$ source 47 (truth).

Introduction

You may be familiar with different terminology and symbols than the ones we use above. Logic texts (and teachers) commonly use either $\sim$ source 66, $\neg$ source 66, and ! for “negation”, $\wedge$ source 66, $\cdot$ source 66, and $\&$ source 66 for “conjunction”. Commonly used symbols for the “conditional” or “implication” are $\rightarrow$ source 68, $\Rightarrow$ source 68, and $\supset$ source 68. Symbols for “biconditional,” “bi-implication,” or “(material) equivalence” are $\leftrightarrow$ source 70, $\Leftrightarrow$ source 71, and $\equiv$ source 71. The $\lfalse$ source 72 symbol is variously called “falsity,” “falsum,” “absurdity,” or “bottom.” The $\ltrue$ source 74 symbol is variously called “truth,” “verum,” or “top.”

Definition: Propositional formulas

The set $\Frm[L_0]$ source 80 of formulas of propositional logic is defined inductively as follows:

$\lfalse$ source 83 is an atomic formula.

Every propositional variable $\Obj p_i$ source 87 is an atomic formula.
If $!A$ source 90 is a formula, then $\lnot !A$ source 90 is a formula.
If $!A$ source 93 and $!B$ source 93 are formulas, then $(!A \land !B)$ source 93 is a formula.
If $!A$ source 96 and $!B$ source 96 are formulas, then $(!A \lor !B)$ source 96 is a formula.
If $!A$ source 99 and $!B$ source 99 are formulas, then $(!A \lif !B)$ source 99 is a formula.
Nothing else is a formula.

source 78

When writing a formula $(!B \ast !C)$ source 129 constructed from $!B$ source 129, $!C$ source 129 using a two-place connective $\ast$ source 130, we will often leave out the outermost pair of parentheses and write simply $!B \ast !C$ source 131.

Definition: Defined propositional operators

Formulas constructed using the defined operators are to be understood as follows:

$\ltrue$ source 140 abbreviates $\lnot\lfalse$ source 141.

$!A \liff !B$ source 161 abbreviates $(!A \lif !B) \land (!B \lif !A)$ source 161.

source 134

Definition: Syntactic identity

The symbol $\ident$ source 168 expresses syntactic identity between strings of symbols, i.e., $!A \ident !B$ source 169 iff $!A$ source 169 and $!B$ source 169 are strings of symbols of the same length and which contain the same symbol in each place.

source 167

The $\ident$ source 173 symbol may be flanked by strings obtained by concatenation, e.g., $!A \ident (!B \lor !C)$ source 174 means: the string of symbols $!A$ source 175 is the same string as the one obtained by concatenating an opening parenthesis, the string $!B$ source 176, the $\lor$ source 176 symbol, the string $!C$ source 177, and a closing parenthesis, in this order. If this is the case, then we know that the first symbol of $!A$ source 178 is an opening parenthesis, $!A$ source 179 contains $!B$ source 179 as a substring (starting at the second symbol), that substring is followed by $\lor$ source 180, etc.

Preliminaries

Theorem: Structural induction for formulas

If some property $P$ source 15 holds for all the atomic formulas and is such that

it holds for $\lnot !A$ source 18 whenever it holds for $!A$ source 19; it holds for $(!A \land !B)$ source 20 whenever it holds for $!A$ source 21 and $!B$ source 21; it holds for $(!A \lor !B)$ source 22 whenever it holds for $!A$ source 23 and $!B$ source 23; it holds for $(!A \lif !B)$ source 24 whenever it holds for $!A$ source 25 and $!B$ source 25;

then $P$ source 29 holds for all formulas.

source 13

Proof

Let $S$ source 33 be the collection of all formulas with property $P$ source 34. Clearly $S \subseteq \Frm[L_0]$ source 34. $S$ source 34 satisfies all the conditions of Definition: Propositional formulas: it contains all atomic formulas and is closed under the operators. $\Frm[L_0]$ source 36 is the smallest such class, so $\Frm[L_0] \subseteq S$ source 37. So $\Frm[L_0] = S$ source 37, and every formula has property $P$ source 38.

End of proof.

Proposition: Balanced parentheses in formulas

Any formula in $\Frm[L_0]$ source 42 is balanced, in that it has as many left parentheses as right ones.

source 41

Exercise: Prove balanced parentheses

Prove Proposition: Balanced parentheses in formulas

source 46

Proposition: No proper initial segment is a formula

No proper initial segment of a formula is a formula.

source 50

Exercise: Prove the initial-segment proposition

Prove Proposition: No proper initial segment is a formula

source 54

Proposition: Unique readability of formulas

Any formula $!A$ source 59 in $\Frm[L_0]$ source 59 has exactly one parsing as one of the following

$\lfalse$ source 62.

$\Obj p_n$ source 66 for some $\Obj p_n \in \PVar$ source 66.
$\lnot !B$ source 68 for some formula $!B$ source 68.
$(!B \land !C)$ source 70 for some formulas $!B$ source 70 and $!C$ source 70.
$(!B \lor !C)$ source 72 for some formulas $!B$ source 72 and $!C$ source 72.
$(!B \lif !C)$ source 74 for some formulas $!B$ source 74 and $!C$ source 74.

Moreover, this parsing is unique.

source 58

Proof

By induction on $!A$ source 82. For instance, suppose that $!A$ source 82 has two distinct readings as $(!B \lif !C)$ source 83 and $(!B' \lif !C')$ source 83. Then $!B$ source 83 and $!B'$ source 83 must be the same (or else one would be a proper initial segment of the other); so if the two readings of $!A$ source 85 are distinct it must be because $!C$ source 86 and $!C'$ source 86 are distinct readings of the same sequence of symbols, which is impossible by the inductive hypothesis.

End of proof.

Definition: Uniform substitution

If $!A$ source 92 and $!B$ source 92 are formulas, and $\Obj p_i$ source 92 is a propositional variable, then $\Subst{!A}{!B}{\Obj p_i}$ source 93 denotes the result of replacing each occurrence of $\Obj p_i$ source 94 by an occurrence of $!B$ source 94 in $!A$ source 94; similarly, the simultaneous substitution of $\Obj p_1$ source 95, …, $\Obj p_n$ source 95 by formulas $!B_1$ source 96, …, $!B_n$ source 96 is denoted by $\SSubst{!A}{\subst{!B_1}{\Obj p_1},\dots,\subst{!B_n}{\Obj p_n}}$ source 97.

source 91

Exercise: Identify uniform substitutions

For each of the five formulas below determine whether the formula can be expressed as a substitution $\Subst{!A}{!B}{\Obj p_i}$ source 101 where $!A$ source 102 is (i) $\Obj p_0$ source 102; (ii) $( \lnot \Obj p_0 \land \Obj p_1)$ source 102; and (iii) $( ( \lnot \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 )$ source 103. In each case specify the relevant substitution.

$\Obj p_1$ source 106
$( \lnot \Obj p_0 \land \Obj p_0 )$ source 107
$( ( \Obj p_0 \lor \Obj p_1 ) \land \Obj p_2 )$ source 108
$\lnot ( ( \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 )$ source 109
$(( \lnot ( \Obj p_0 \lif \Obj p_1 ) \lif ( \Obj p_0 \lor \Obj p_1 )) \land \lnot ( \Obj p_0 \land \Obj p_1 ))$ source 110

source 100

Exercise: Define substitution by induction

Give a mathematically rigorous definition of $\Subst{!A}{!B}{p}$ source 115 by induction.

source 114

Formation Sequences

Defining formulas via an inductive definition, and the complementary technique of proving properties of formulas via induction, is an elegant and efficient approach. However, it can also be useful to consider a more bottom-up, step-by-step approach to the construction of formulas, which we do here using the notion of a formation sequence.

Definition: Formation sequences for formulas

A finite sequence $\tuple{!A_0,\dotsc,!A_n}$ source 22 of strings of symbols from the language $\Lang L_0$ source 23 is a formation sequence for $!A$ source 24 if $!A \ident !A_n$ source 24 and for all $i \leq n$ source 24, either $!A_i$ source 25 is an atomic formula or there exist $j,k < i$ source 25 such that one of the following holds:

$!A_i \ident \lnot !A_j$ source 28. $!A_i \ident (!A_j \land !A_k)$ source 29. $!A_i \ident (!A_j \lor !A_k)$ source 30. $!A_i \ident (!A_j \lif !A_k)$ source 31.

source 20

Example: A formation sequence

$\tuple{ \Obj p_0, \Obj p_1, (\Obj p_1 \land \Obj p_0), \lnot (\Obj p_1 \land \Obj p_0) }$ source 37 is a formation sequence of $\lnot (\Obj p_1 \land \Obj p_0)$ source 46, as is $\tuple{ \Obj p_0, \Obj p_1, \Obj p_0, (\Obj p_1 \land \Obj p_0), (\Obj p_0 \lif \Obj p_1), \lnot (\Obj p_1 \land \Obj p_0) }.$ source 47

As can be seen from the second example, formation sequences may contain `junk': formulas which are redundant or do not contribute to the construction.

source 36

Proposition: Every formula has a formation sequence

Every formula $!A$ source 65 in $\Frm[L_0]$ source 65 has a formation sequence.

source 63

Proof

Suppose $!A$ source 69 is atomic. Then the sequence $\tuple{!A}$ source 69 is a formation sequence for $!A$ source 70.

Now suppose that $!B$ source 72 and $!C$ source 72 have formation sequences $\tuple{!B_0,\dotsc,!B_n}$ source 73 and $\tuple{!C_0,\dotsc,!C_m}$ source 73 respectively.

If $!A \ident \lnot !B$ source 77, then $\tuple{!B_0,\dotsc,!B_n,\lnot !B_n}$ source 78 is a formation sequence for $!A$ source 79. If $!A \ident (!B \land !C)$ source 80, then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \land !C_m)}$ source 81 is a formation sequence for $!A$ source 82. If $!A \ident (!B \lor !C)$ source 83, then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lor !C_m)}$ source 84 is a formation sequence for $!A$ source 85. If $!A \ident (!B \lif !C)$ source 86, then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lif !C_m)}$ source 87 is a formation sequence for $!A$ source 88.

By the principle of induction on formulas, every formula has a formation sequence.

End of proof.

We can also prove the converse. This is important because it shows that our two ways of defining formulas are equivalent: they give the same results. It also means that we can prove theorems about formulas by using ordinary induction on the length of formation sequences.

Lemma: Initial subsequences remain formation sequences

Suppose that $\tuple{!A_0,\dotsc,!A_n}$ source 105 is a formation sequence for $!A_n$ source 106, and that $k \leq n$ source 106. Then $\tuple{!A_0,\dotsc,!A_k}$ source 106 is a formation sequence for $!A_k$ source 107.

source 103

Proof

Exercise.

End of proof.

Theorem: Formulas characterized by formation sequences

$\Frm[L_0]$ source 116 is the set of all strings of symbols in the language $\Lang L_0$ source 117 with a formation sequence.

source 114

Proof

Let $F$ source 121 be the set of all strings of symbols in the language $\Lang L_0$ source 122 that have a formation sequence. We have seen in Proposition: Every formula has a formation sequence that $\Frm[L_0] \subseteq F$ source 124, so now we prove the converse.

Suppose $!A$ source 126 has a formation sequence $\tuple{!A_0,\dotsc,!A_n}$ source 126. We prove that $!A \in \Frm[L_0]$ source 127 by strong induction on $n$ source 127. Our induction hypothesis is that every string of symbols with a formation sequence of length $m < n$ source 129 is in $\Frm[L_0]$ source 129. By the definition of a formation sequence, either $!A_n$ source 130 is atomic or there must exist $j,k < n$ source 131 such that one of the following is the case:

$!A_n \ident \lnot !A_j$ source 134. $!A_n \ident (!A_j \land !A_k)$ source 135. $!A_n \ident (!A_j \lor !A_k)$ source 136. $!A_n \ident (!A_j \lif !A_k)$ source 137.

Now we reason by cases. If $!A_n$ source 140 is atomic then $!A_n \in \Frm[L_0]$ source 141. Suppose instead that $!A \equiv (!A_j \land !A_k)$ source 141. By Lemma: Initial subsequences remain formation sequences, $\tuple{!A_0,\dotsc,!A_j}$ source 143 and $\tuple{!A_0,\dotsc,!A_k}$ source 143 are formation sequences for $!A_j$ source 144 and $!A_k$ source 144 respectively. Since these are proper initial subsequences of the formation sequence for $!A$ source 146, they both have length less than $n$ source 146. Therefore by the induction hypothesis, $!A_j$ source 147 and $!A_k$ source 147 are in $\Frm[L_0]$ source 147, and so by the definition of a formula, so is $(!A_j \land !A_k)$ source 149. The other cases follow by parallel reasoning.

End of proof.

valuation and Satisfaction

Definition: Propositional valuations

Let $\{\True, \False\}$ source 14 be the set of the two truth values, “true” and “false.” A valuation for $\Lang{L_0}$ source 15 is a function $\pAssign{v}$ source 16 assigning either $\True$ source 16 or $\False$ source 16 to the propositional variables of the language, i.e., $\pAssign{v} \colon \PVar \to \{\True, \False \}$ source 17.

source 13

Definition: Evaluation of propositional formulas

Given a valuation $\pAssign{v}$ source 22, define the evaluation function $\pValue{v} \colon \Frm[L_0] \to \{\True, \False \}$ source 23 inductively by: $\pValue{v}(\lfalse) & = \False; \\ \pValue{v}(\Obj p_n) & = \pAssign{v}(\Obj p_n); \\ \pValue{v}(\lnot !A) & = \begin{cases} \True & \text{if } \pValue{v}(!A) = \False;\\ \False & \text{otherwise.} \end{cases} \\ \pValue{v}(!A \land !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \False$}. \end{cases}\\ \pValue{v}(!A \lor !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \True$ or $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \False$ and $\pValue{v}(!B) = \False$}. \end{cases}\\ \pValue{v}(!A \lif !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \False$}. \end{cases}\\$ source 24

source 21

Explanation

The clauses correspond to the following truth tables:

Negation truth table

Negation truth table. The first columns give input truth values and the final column gives the connective's result.

Negation truth table
A	not A
True	False
False	True

Source formula occurrences in table order

$!A$ source 64
$\lnot !A$ source 64
$\True$ source 66
$\False$ source 66
$\False$ source 67
$\True$ source 67

source 63

Conjunction truth table

Conjunction truth table. The first columns give input truth values and the final column gives the connective's result.

Conjunction truth table
A	B	A and B
True	True	True
True	False	False
False	True	False
False	False	False

Source formula occurrences in table order

$!A$ source 73
$!B$ source 73
$!A \land !B$ source 73
$\True$ source 75
$\True$ source 75
$\True$ source 75
$\True$ source 76
$\False$ source 76
$\False$ source 76
$\False$ source 77
$\True$ source 77
$\False$ source 77
$\False$ source 78
$\False$ source 78
$\False$ source 78

source 72

Disjunction truth table

Disjunction truth table. The first columns give input truth values and the final column gives the connective's result.

Disjunction truth table
A	B	A or B
True	True	True
True	False	True
False	True	True
False	False	False

Source formula occurrences in table order

$!A$ source 84
$!B$ source 84
$!A \lor !B$ source 84
$\True$ source 86
$\True$ source 86
$\True$ source 86
$\True$ source 87
$\False$ source 87
$\True$ source 87
$\False$ source 88
$\True$ source 88
$\True$ source 88
$\False$ source 89
$\False$ source 89
$\False$ source 89

source 83

Material conditional truth table

Material conditional truth table. The first columns give input truth values and the final column gives the connective's result.

Material conditional truth table
A	B	if A then B
True	True	True
True	False	False
False	True	True
False	False	True

Source formula occurrences in table order

$!A$ source 96
$!B$ source 96
$!A \lif !B$ source 96
$\True$ source 98
$\True$ source 98
$\True$ source 98
$\True$ source 99
$\False$ source 99
$\False$ source 99
$\False$ source 100
$\True$ source 100
$\True$ source 100
$\False$ source 101
$\False$ source 101
$\True$ source 101

source 95

Exercise: A ternary connective

Consider adding to $\Lang{L_0}$ source 120 a ternary connective $\diamondsuit$ source 120 with evaluation given by $\pValue{v}(\diamondsuit( !A , !B , !C ) ) = \begin{cases} \pValue{v}( !B ) & \text{if $\pValue{v}(!A) = \True$;}\\ \pValue{v}( !C ) & \text{if $\pValue{v}(!A) = \False $}. \end{cases}$ source 122 Write down the truth table for this connective.

source 119

Theorem: Local determination

Suppose that $\pAssign{v_1}$ source 134 and $\pAssign{v_2}$ source 135 are valuations that agree on the propositional variables occurring in $!A$ source 136, i.e., $\pAssign{v_1}(\Obj p_n) = \pAssign{v_2}(\Obj p_n)$ source 136 whenever $\Obj p_n$ source 137 occurs in some formula $!A$ source 138. Then $\pValue{v_1}$ source 138 and $\pValue{v_2}$ source 138 also agree on $!A$ source 139, i.e., $\pValue{v_1}(!A) = \pValue{v_2}(!A)$ source 139.

source 133

Proof

By induction on $!A$ source 143.

End of proof.

Definition: Satisfaction by a valuation

We can inductively define the notion of satisfaction of a formula $!A$ source 148 by a valuation $\pAssign{v}$ source 149, $\pSat{v}{!A}$ source 149, as follows. (We write $\pSat/{v}{!A}$ source 150 to mean “not $\pSat{v}{!A}$ source 150.”)

Case: $\pSat/{v}{\indfrm}$ source 153.

Case: $\pSat{v}{\indfrm}$ source 158 iff $\pAssign{v}(\Obj p_i) = \True$ source 159.
Case: $\pSat{v}{\indfrm}$ source 162 iff $\pSat/{v}{!B}$ source 163.
Case: $\pSat{v}{\indfrm}$ source 166 iff $\pSat{v}{!B}$ source 166 and $\pSat{v}{!C}$ source 167.
Case: $\pSat{v}{\indfrm}$ source 170 iff $\pSat{v}{!B}$ source 171 or $\pSat{v}{!C}$ source 171 (or both).
Case: $\pSat{v}{\indfrm}$ source 174 iff $\pSat/{v}{!B}$ source 174 or $\pSat{v}{!C}$ source 175 (or both).

If $\Gamma$ source 182 is a set of formulas, $\pSat{v}{\Gamma}$ source 182 iff $\pSat{v}{!A}$ source 183 for every $!A \in \Gamma$ source 183.

source 146

Proposition: Satisfaction agrees with truth value

$\pSat{v}{!A}$ source 187 iff $\pValue{v}(!A) = \True$ source 187.

source 186

Proof

By induction on $!A$ source 191.

End of proof.

Exercise: Prove satisfaction agrees with truth value

Prove Proposition: Satisfaction agrees with truth value

source 194

Semantic Notions

We define the following semantic notions:

Definition: Satisfiability, tautology, and semantic consequence

A formula $!A$ source 17 is satisfiable if for some $\pAssign{v}$ source 18, $\pSat{v}{!A}$ source 18; it is unsatisfiable if for no $\pAssign{v}$ source 19, $\pSat{v}{!A}$ source 19;
A formula $!A$ source 20 is a tautology if $\pSat{v}{!A}$ source 20 for all valuations $\pAssign{v}$ source 21;
A formula $!A$ source 22 is contingent if it is satisfiable but not a tautology;
If $\Gamma$ source 24 is a set of formulas, $\Gamma \Entails !A$ source 24 (“ $\Gamma$ source 24 entails $!A$ source 25”) if and only if $\pSat{v}{!A}$ source 25 for every valuation $\pAssign{v}$ source 26 for which $\pSat{v}{\Gamma}$ source 26.
If $\Gamma$ source 27 is a set of formulas, $\Gamma$ source 27 is satisfiable if there is a valuation $\pAssign{v}$ source 28 for which $\pSat{v}{\Gamma}$ source 29, and $\Gamma$ source 29 is unsatisfiable otherwise.

source 15

Exercise: Classify formulas semantically

For each of the following four formulas determine whether it is (a) satisfiable, (b) tautology, and (c) contingent.

$( \Obj p_0 \lif ( \lnot \Obj p_1 \lif \lnot \Obj p_0 ) )$ source 38.
$( ( \Obj p_0 \land \lnot \Obj p_1 ) \lif ( \lnot \Obj p_0 \land \Obj p_2 )) \liff ( ( \Obj p_2 \lif \Obj p_0 ) \lif ( \Obj p_0 \lif \Obj p_1 ))$ source 39.
$( \Obj p_0 \liff \Obj p_1 ) \lif ( \Obj p_2 \liff \lnot \Obj p_1 )$ source 40.
$(( \Obj p_0 \liff ( \lnot \Obj p_1 \land \Obj p_2 )) \lor ( \Obj p_2 \lif ( \Obj p_0 \liff \Obj p_1 )))$ source 41.

source 34

Proposition: Basic semantic consequence facts

$!A$ source 48 is a tautology if and only if $\emptyset \Entails !A$ source 49;
If $\Gamma \Entails !A$ source 50 and $\Gamma \Entails !A \lif !B$ source 50 then $\Gamma \Entails !B$ source 51;
If $\Gamma$ source 52 is satisfiable then every finite subset of $\Gamma$ source 52 is also satisfiable;
Monotonicity: if $\Gamma \subseteq \Delta$ source 54 and $\Gamma \Entails !A$ source 55 then also $\Delta \Entails !A$ source 55;
Transitivity: if $\Gamma \Entails !A$ source 56 and $\Delta \cup \{ !A\} \Entails !B$ source 57 then $\Gamma \cup \Delta \Entails !B$ source 57.

source 45

Proof

Exercise.

End of proof.

Exercise: Prove the semantic consequence facts

Prove Proposition: Basic semantic consequence facts

source 66

Proposition: Consequence and unsatisfiability

$\Gamma \Entails !A$ source 71 if and only if $\Gamma \cup \{\lnot !A\}$ source 71 is unsatisfiable.

source 70

Proof

Exercise.

End of proof.

Exercise: Prove the consequence-unsatisfiability equivalence

Prove Proposition: Consequence and unsatisfiability

source 79

Theorem: Semantic deduction theorem

$\Gamma \Entails !A \lif !B$ source 84 if and only if $\Gamma \cup \{!A\} \Entails !B$ source 85.

source 83

Proof

Exercise.

End of proof.

Exercise: Prove the semantic deduction theorem

Prove Theorem: Semantic deduction theorem

source 92