Semantics: synthesis and challenges

Summary

This lesson closes the unit devoted to semantics. It rebuilds the deductive chain that runs from the extension of a valuation to all formulas and from the coincidence lemma to consequence, equivalence and their two working theorems, replacement and uniform substitution; from there to the laws for any number of terms, to functional completeness and to the sets of connectives, and from there to normal forms, to their algorithm and to circuits, pointing out at each link which results it uses and in which lesson it is proved. It distinguishes what the unit proved from what it took from the previous ones, decides in three ways an argument that the course has carried along since the first unit and explains why the question that the unit leaves open, that of knowing whether what is true under every valuation coincides with what is derivable, leads to metatheory. It repeats in its exit assessment the skills of the entry assessment, and it ends with six challenges, harder than the problems of the lessons, which require combining the tools of several of them.

Learning objectives

Rebuild the logical order of the results of the unit, identifying the earlier results on which each one rests and the lesson in which it is proved.
Explain how the recursive extension, the coincidence lemma, semantic replacement and the generalized laws lead to functional completeness, to the existence of normal forms and to the correctness and termination of their algorithm.
Distinguish what the unit proved from what it took from the previous ones and from what it left to metatheory, in particular the coincidence of semantic consequence with derivability, and compactness.
Solve problems that combine calculation with values, consequence, uniform substitution, sets of connectives, normal forms and circuits.

What the unit achieved

The unit set out to give meaning to the formulas of the language built in the first unit, without touching the deductive system of the second, and to obtain from that meaning procedures for deciding the questions that logic asks about them: whether a formula is valid, whether it is satisfiable, whether it follows from others, whether it says the same as another. The purpose has been fulfilled with a few reservations, each one declared in its place: bivalence and truth-functionality, which are not proved but chosen, and whose price was shown by the lesson on formalization; unique readability, definition by recursion, induction and the official abbreviations, which were proved or fixed in the first unit and are used here; and the indispensable facts about sets and functions, which were recalled where they were needed. With those reservations, the path travelled can be read as a single deductive chain in six segments, one per lesson.

The value of a formula

The lesson on the semantics of propositional logic defined a valuation as a function from the variables to $\{0, 1\}$ and proved, with the theorem of definition by recursion on formulas, that it extends in a unique way to all formulas with a single clause: $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ . From the official abbreviations it computed, without stipulating anything else, the value of each defined connective, written as a polynomial in the values of the components, and with it the table of implication, which is here a theorem. It proved by induction on complexity the coincidence lemma, from which it follows that the truth table, with $2^{n}$ rows, contains everything that the infinitely many valuations say about a formula with $n$ variables; it defined satisfaction, validity, satisfiability, contradiction and contingency, made precise that $\not\models \varphi$ says that $\varphi$ is not valid and not that it is contradictory, fixed $\top := (v_{1} \rightarrow v_{1})$ and $\bot := \neg\top$ , and obtained the decidability of validity and of satisfiability, at an exponential cost that the directed search for a falsifying valuation reduces without eliminating it.

Consequence and equivalence

The lesson on semantic consequence and equivalence defined consequence from a set of premises, finite or infinite, and proved that it has the structural properties of deduction (reflexivity, monotonicity, cut and transitivity), with proofs that go through valuations instead of manipulating lines. The semantic deduction theorem, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , was reduced to the only false row of implication, and consequence was reduced to unsatisfiability: $\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\}$ is unsatisfiable. Semantic equivalence, defined as the equality of values, turned out to coincide with mutual consequence and with the validity of the biconditional. Its two working theorems were proved by induction on complexity: the replacement of an occurrence of a subformula by an equivalent one, with the case of the total occurrence, which cannot be omitted, and the uniform substitution of arbitrary formulas for variables, which preserves validity, equivalence and consequence. With them, the laws of the catalogue, verified as identities between polynomials, apply anywhere in any formula and can be chained.

Laws for any number of terms

The lesson on the generalized De Morgan and distributive laws defined by recursion, associating to the left, the conjunction and the disjunction of $n$ formulas, and proved by induction on the number of terms the value lemma, which says that a conjunction is true if and only if all its terms are and a disjunction if and only if some term is. With it and with the compatibility of the connectives with equivalence, it obtained generalized associativity, which was proved with a chain of equivalences so that it also holds for provable equivalence, the independence of order and of repetitions, the generalized De Morgan laws and generalized distributivity, whose induction on two indices was organized so that the induction hypothesis covers all the lengths of the second list; the dual law was obtained by De Morgan, without repeating the double induction.

Truth functions

The lesson on functional completeness travelled the opposite path, from the table to the formula. It counted the truth functions of $n$ arguments, $2^{2^{n}}$ , showed that each formula represents exactly one of them and that two formulas are equivalent if and only if they represent the same one, and proved the functional completeness theorem: the conjunction of a row is true exactly on its row, and the disjunction of the conjunctions of the rows on which the function takes the value $1$ represents it. Since that formula is a string of circles and disks, joint denial suffices by itself; with the joint denial criterion, $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ and alternative denial also suffice; and with the closure principle, it proved that all the formulas of $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ preserve $1$ , so that this set does not suffice.

Normal forms

The lesson on normal forms chose, in each class of equivalent formulas, representatives of a fixed shape. It defined literals, clauses and elementary conjunctions, and proved that the negation of a normal form is equivalent to its dual, which changes each conjunction into a disjunction and each literal into its opposite. It built from the table the canonical forms, unique once the variables are fixed, and proved the existence of both normal forms in two ways: by the table, as a corollary of functional completeness, and by induction on complexity, with the only case of joint denial, which is equivalent to the conjunction of the negations of its components, and with an induction hypothesis that asks for both forms at once, because negation interchanges them. It showed, lastly, that the validity of a conjunctive form and the satisfiability of a disjunctive one can be read at a glance in their complementary pairs.

The algorithm and the circuits

The lesson on the normal form algorithm and its applications turned the second proof of existence into a procedure that acts on written forms: eliminate the connectives other than $\neg$ , $\wedge$ and $\vee$ , push the negations down to the variables and distribute. It proved its correctness with replacement in a written form, which adapts the replacement theorem to abbreviations, and its termination with three measures that decrease at each step, the last of which reads conjunction as a product; it also proved that the conjunctive form of $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ necessarily has $2^{n}$ clauses, so that the growth is not a defect of the algorithm. It then obtained the normal forms of a black box from its table, shortened them by merging adjacent rows and turned them into switching circuits, whose conduction is the value of their formula.

The following figure gathers the six segments into a single chain. Each node of the column is a definition or a result, numbered according to the logical order and joined by an arc to the earlier links that its proof uses; around them float the supports, that is, the principles and tools to which the chain turns again and again, each joined by a solid line to the links that rest on it and by a dotted one to the link where it is established, except those that this chain does not prove (unique readability with recursion, induction and the official abbreviations, from the first unit), which are drawn as rings. Clicking a support highlights all the links that use it, and each link refers to the lesson in which it is proved. Note that induction and the values of the connectives are the most visited supports of the unit, and that the value lemma, although it is proved in the third lesson, supports almost everything that the last three say about conjunctions and disjunctions.

Supports of the chain

AUnique readability and recursion. If $\sigI\varphi\psi = \sigI\varphi'\psi'$ , with the four strings formulas, then $\varphi = \varphi'$ and $\psi = \psi'$ ; hence a rule that computes the value of $\sigI\varphi\psi$ from $\varphi$ , from $\psi$ and from their values defines a single function on formulas. It was proved in the first unit. Admitted without proof in this unit.
BInduction. Simple and strong on the natural numbers, and on the complexity of formulas, whose only cases are the variables and joint denial $(\varphi \downarrow \psi)$ . It was proved in the first unit. Admitted without proof in this unit.
COfficial abbreviations. $\neg\varphi := (\varphi \downarrow \varphi)$ , $(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)$ , $(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)$ , $(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)$ , $(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$ and $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$ . They were fixed in the first unit. Admitted without proof in this unit.
DValues of the connectives. With $a = v(\varphi)$ and $b = v(\psi)$ : $v(\neg\varphi) = 1 - a$ , $v((\varphi \vee \psi)) = a + b - ab$ , $v((\varphi \wedge \psi)) = ab$ , $v((\varphi \rightarrow \psi)) = 1 - a(1 - b)$ , $v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b)$ and $v((\varphi \veebar \psi)) = a + b - 2ab$ , where $a^{2} = a$ . Established in: 1. Extension of a valuation.
ECoincidence lemma. If two valuations agree on the variables of $\varphi$ , they give $\varphi$ the same value; that is why the table with $2^{n}$ rows says everything. Established in: 2. Coincidence lemma and tables.
FSemantic replacement. If $\theta \eqsem \theta'$ and $\chi'$ results from replacing in $\chi$ an occurrence of $\theta$ by $\theta'$ , then $\chi \eqsem \chi'$ . Established in: 7. Semantic replacement theorem.
GLaws of equivalence. Double negation, idempotence, commutativity, associativity, distributivity, De Morgan, absorption, identity, domination, excluded middle and non-contradiction, for arbitrary formulas. Established in: 9. Laws of equivalence.
HValue lemma. $v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1$ if and only if $v(\varphi_i) = 1$ for every $i$ ; $v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1$ if and only if $v(\varphi_i) = 1$ for some $i$ . Established in: 10. Value lemma and compatibility.

Segment 1 The value of a formula
- Compute the value of a formula with the clause of joint denial and derive from the abbreviations that of each defined connective.
- Prove the coincidence lemma and justify with it that a table with $2^{n}$ rows suffices.
- Classify formulas and sets without confusing $\not\models \varphi$ with contradiction, and decide validity by searching for a falsifying valuation.
1. Extension of a valuation. Each valuation $v$ extends in a unique way to all formulas with the clause $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ ; by unfolding the abbreviations one computes the value of $\neg$ , $\vee$ , $\wedge$ , $\rightarrow$ , $\leftrightarrow$ and $\veebar$ .
  Rests on: A (Unique readability and recursion), C (Official abbreviations). Proved in: Semantics of propositional logic.
2. Coincidence lemma and tables. If $v$ and $v'$ agree on $V(\varphi)$ , then $v(\varphi) = v'(\varphi)$ , by induction on complexity; hence the values of $\varphi$ under all valuations are exactly those of the $2^{n}$ rows of its table.
  Uses: 1. Extension of a valuation. Rests on: B (Induction). Proved in: Semantics of propositional logic.
3. Classification and decision. Every formula is exactly one of three things: valid, contingent or a contradiction; $\varphi$ is valid if and only if $\neg\varphi$ is a contradiction, and it is a contradiction if and only if $\models \neg\varphi$ . $\top$ and the excluded middle are valid, $\bot$ is a contradiction, and validity and satisfiability are decided by going through the rows.
  Rests on: D (Values of the connectives), E (Coincidence lemma). Proved in: Semantics of propositional logic.
Segment 2 Consequence and equivalence
- Decide consequences from finite or infinite sets, by exhibiting a countermodel or by proving that none exists.
- Apply the semantic deduction theorem and the reduction of consequence to unsatisfiability.
- Distinguish the replacement of an occurrence from uniform substitution, and prove both by induction on complexity.
- Establish equivalences by chains, naming each law correctly.
1. Consequence and its properties. $\Gamma \models \varphi$ if every valuation that satisfies $\Gamma$ satisfies $\varphi$ ; $\emptyset \models \varphi$ if and only if $\models \varphi$ ; reflexivity, monotonicity, cut and transitivity hold, and an unsatisfiable set has every formula as a consequence.
  Uses: 3. Classification and decision. Proved in: Semantic consequence and equivalence.
2. Semantic deduction and unsatisfiability. $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , by the only false row of implication; $\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots))$ ; and $\Gamma \models \varphi$ if and only if $\Gamma \cup \{\neg\varphi\}$ is unsatisfiable.
  Uses: 4. Consequence and its properties. Rests on: D (Values of the connectives). Proved in: Semantic consequence and equivalence.
3. Semantic equivalence. $\varphi \eqsem \psi$ if and only if $\varphi \models \psi$ and $\psi \models \varphi$ , if and only if $\models (\varphi \leftrightarrow \psi)$ ; equivalence is reflexive, symmetric and transitive, and two equivalent formulas are interchangeable as premises and as conclusions.
  Uses: 4. Consequence and its properties. Rests on: D (Values of the connectives). Proved in: Semantic consequence and equivalence.
4. Semantic replacement theorem. If $\theta \eqsem \theta'$ , replacing in $\chi$ an occurrence of $\theta$ by $\theta'$ , the total occurrence included, gives a formula equivalent to $\chi$ ; and so does substituting all the occurrences at once.
  Uses: 1. Extension of a valuation, 6. Semantic equivalence. Rests on: A (Unique readability and recursion), B (Induction). Proved in: Semantic consequence and equivalence.
5. Uniform substitution. If $w(v_n) = v(\sigma(v_n))$ , then $v(\sigma(\chi)) = w(\chi)$ ; hence, if $\models \chi$ , also $\models \sigma(\chi)$ , and substitution preserves equivalence and consequence, but not satisfiability or contingency.
  Uses: 1. Extension of a valuation, 4. Consequence and its properties, 6. Semantic equivalence. Rests on: A (Unique readability and recursion), B (Induction). Proved in: Semantic consequence and equivalence.
6. Laws of equivalence. The laws of the catalogue are verified as identities between polynomials with $a^{2} = a$ ; with replacement and transitivity, they apply to subformulas and can be chained.
  Uses: 3. Classification and decision, 6. Semantic equivalence. Rests on: D (Values of the connectives), F (Semantic replacement). Proved in: Semantic consequence and equivalence.
Segment 3 Laws for any number of terms
- Unfold conjunctions and disjunctions of $n$ terms as strings associated to the left and compute their value.
- Prove by induction on the number of terms generalized associativity, the independence of order and the generalized De Morgan laws.
- Prove generalized distributivity with an induction on two indices, and count the terms it produces.
1. Value lemma and compatibility. If $\alpha \eqsem \alpha'$ and $\beta \eqsem \beta'$ , then $\neg\alpha \eqsem \neg\alpha'$ , $(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')$ and $(\alpha \vee \beta) \eqsem (\alpha' \vee \beta')$ ; a conjunction of $n$ terms has the value $1$ if and only if all its terms have the value $1$ , a disjunction if and only if some term has the value $1$ , and equivalent terms give equivalent conjunctions and disjunctions.
  Uses: 6. Semantic equivalence. Rests on: D (Values of the connectives), B (Induction). Proved in: Generalized De Morgan and distributive laws.
2. Associativity and order. The conjunction of the conjunctions of two lists is equivalent to that of their concatenation, and every grouping is equivalent to the one associated to the left; two lists with the same terms give equivalent conjunctions and disjunctions, whatever the order and the repetitions.
  Rests on: H (Value lemma), G (Laws of equivalence), B (Induction). Proved in: Generalized De Morgan and distributive laws.
3. Generalized De Morgan laws. $\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i$ and $\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i$ , by applying the binary law to the last join and the induction hypothesis to what remains inside.
  Rests on: H (Value lemma), G (Laws of equivalence), B (Induction). Proved in: Generalized De Morgan and distributive laws.
4. Generalized distributivity. $\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j)$ , with $nm$ terms in lexicographic order; and its dual, which distributes the disjunction of two conjunctions, by De Morgan.
  Uses: 11. Associativity and order, 12. Generalized De Morgan laws. Rests on: H (Value lemma), G (Laws of equivalence), B (Induction). Proved in: Generalized De Morgan and distributive laws.
Segment 4 Truth functions
- Count the truth functions and decide equivalence by comparing the functions that two formulas represent.
- Build the formula of a table and write any function with joint denial alone.
- Prove that a set of connectives is adequate with the joint denial criterion, or that it is not with a property that its formulas preserve.
1. Truth functions. There are $2^{2^{n}}$ truth functions of $n$ arguments; a formula with variables among $v_1, \ldots, v_n$ represents exactly one of them, $f_\varphi$ , and $\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi$ .
  Uses: 6. Semantic equivalence. Rests on: E (Coincidence lemma). Proved in: Functional completeness.
2. Functional completeness. The conjunction of a row has the value $1$ exactly on its row; the disjunction of the conjunctions of the rows on which $f$ has the value $1$ , or $(v_{1} \wedge \neg v_{1})$ if there are none, represents $f$ ; and every formula is equivalent to the formula of its table.
  Uses: 14. Truth functions. Rests on: H (Value lemma), D (Values of the connectives). Proved in: Functional completeness.
3. Adequate and inadequate sets. Joint denial suffices, because the abbreviations can be unfolded; if the formulas of $K$ express the value $(1 - a)(1 - b)$ , $K$ is adequate, as are $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ and $\{\uparrow\}$ ; the formulas of $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ have the value $1$ when all the variables have the value $1$ , and that set is not adequate.
  Uses: 15. Functional completeness. Rests on: C (Official abbreviations), B (Induction), D (Values of the connectives). Proved in: Functional completeness.
Segment 5 Normal forms
- Recognize literals, clauses and normal forms, distinguishing the shape of the string from its meaning.
- Build the canonical forms from the table and prove their uniqueness.
- Prove by induction the existence of normal forms, with the induction hypothesis that asks for both.
- Decide at a glance the validity of a conjunctive form and the satisfiability of a disjunctive one.
1. Literals and duality. $\neg\ell \eqsem \ell^{*}$ ; an elementary conjunction is satisfiable if and only if it contains no complementary pair, and a clause is valid if and only if it contains one; the negation of a normal form is equivalent to its dual, so that the conjunctive form of $\varphi$ is the dual of the disjunctive form of $\neg\varphi$ .
  Uses: 12. Generalized De Morgan laws. Rests on: G (Laws of equivalence), F (Semantic replacement), H (Value lemma). Proved in: Normal forms.
2. Canonical forms. If $\varphi$ is satisfiable, it is equivalent to its disjunctive canonical form, and if it is not valid, to the conjunctive one; once the variables $v_1, \ldots, v_n$ are fixed, two canonical forms are equivalent if and only if they are the same string, and two satisfiable formulas are equivalent if and only if they have the same disjunctive canonical form.
  Uses: 15. Functional completeness, 17. Literals and duality. Rests on: H (Value lemma), E (Coincidence lemma). Proved in: Normal forms.
3. Existence by induction. $(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)$ ; normal forms are preserved under conjunction and disjunction, the disjunctive form of a conjunction and the conjunctive form of a disjunction by generalized distributivity; by induction, with the induction hypothesis for both forms, every formula has a disjunctive form and a conjunctive one.
  Uses: 17. Literals and duality, 11. Associativity and order, 13. Generalized distributivity. Rests on: B (Induction), F (Semantic replacement). Proved in: Normal forms.
4. What can be seen at a glance. A conjunctive form is valid if and only if each clause contains a complementary pair; a disjunctive form is satisfiable if and only if some elementary conjunction contains none.
  Uses: 17. Literals and duality. Rests on: H (Value lemma). Proved in: Normal forms.
Segment 6 The algorithm and the circuits
- Apply the rewriting algorithm and choose the elimination of the biconditional that is convenient.
- Prove its correctness and its termination, and explain why the conjunctive form can grow exponentially.
- Obtain and simplify the normal forms of a black box, and design switching circuits with them.
1. Correctness and termination of the algorithm. Replacing a written subform by an equivalent one gives an equivalent written form; each rule is an equivalence, and an irreducible written form is a normal form grouped in some way; the measures $M_1$ , $M_2$ , with $M_2(\neg\varphi) = 2^{M_2(\varphi)}$ , and $M_3$ , with $M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi)$ , decrease at each step.
  Uses: 19. Existence by induction, 11. Associativity and order. Rests on: G (Laws of equivalence), D (Values of the connectives), B (Induction). Proved in: The normal form algorithm and its applications.
2. Exponential growth. $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ is equivalent to a conjunctive form with $2^{n}$ clauses, and every equivalent conjunctive form has at least $2^{n}$ non-valid clauses.
  Uses: 19. Existence by induction, 17. Literals and duality. Rests on: H (Value lemma). Proved in: The normal form algorithm and its applications.
3. Adjacent rows and circuits. $(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa$ and its dual; a series-parallel circuit conducts in the state $v$ if and only if $v(\varphi_C) = 1$ , and every truth function is realized by some circuit.
  Uses: 15. Functional completeness, 18. Canonical forms, 17. Literals and duality, 11. Associativity and order. Rests on: G (Laws of equivalence), F (Semantic replacement), D (Values of the connectives), B (Induction). Proved in: The normal form algorithm and its applications.

Towards metatheory. The chain stops where semantics reaches a procedure for every question about formulas. It remains to know whether what is true under every valuation is exactly what is deduced in the system: the next unit will compare both notions.