Metatheory: synthesis and challenges

Summary

This lesson closes the unit devoted to metatheory and, with it, the content of the course. It rebuilds the deductive chain that runs from the validity of the axioms to the soundness of the system; from the two lemmas on joint denial to Kalmár's lemma and to completeness for finite sets of premises; from the two-witness lemma to the compactness theorem and, through it, to strong completeness; and from the clausal form to the soundness and the refutation completeness of the resolution method, pointing out at each link which results it uses and in which lesson it is proved. It shows how the three earlier parts of the course, language, deduction and semantics, converge in the coincidence of $\vdash$ and $\models$ , and what each of them contributes to that coincidence; it distinguishes what the course proved from what it assumed and from what it leaves open. 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, and justify the order of compactness and strong completeness.
Explain how language, deduction and semantics converge in the coincidence of $\vdash$ and $\models$ , and which result of each unit of the course is indispensable for it.
Distinguish what the course proved from what it assumed (the axiom schemas, the primitive rules and induction) and from what it leaves open (the cost of deciding satisfiability, and logic with quantifiers).
Solve problems that combine markings, Kalmár's lemma, uniform substitution, compactness and resolution, using in each case the easy side of the coincidence.

What the unit achieved

The unit set out to compare the two relations that the previous units had built on the same language, derivability $\Gamma \vdash \varphi$ and semantic consequence $\Gamma \models \varphi$ , and to prove that they coincide. The aim has been achieved without reservations in the statements: both relations are the same for every set of premises, finite or infinite, and resolution offers a third way, equally sound and complete, of deciding consequence. The reservations lie in the methods, and each one was declared in its place: the completeness of the first lesson is constructive but not practical, because it produces deductions as long as the table; compactness ensures that a valuation exists, but does not teach how to find it; and resolution decides, but its cost in the worst case is an open question. With these reservations, the path travelled can be read as a single deductive chain in four segments.

Soundness

The lesson on soundness and completeness began by fixing the vocabulary: the system is sound if $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , and complete if the converse holds, in three degrees (weak, for finite sets and strong). It took apart a circular argument that claims to obtain completeness “by soundness” by passing from $\nvdash \chi$ to $\not\models \chi$ , a step that is the contrapositive of weak completeness, and it showed that the two properties are independent. It then proved that every instance of A1, A2 and A3 is valid, by supposing a valuation that refuted it and arriving, through the false row of the implication, at impossible values; and, by strong induction on the number of lines, soundness, with one case for the axioms, another for the premises, semantic modus ponens and, for the rule of replacement of double negation, the equivalence $\theta \eqsem \neg\neg\theta$ with the semantic replacement theorem. The property transmitted from line to line is not validity but satisfaction by a fixed valuation that satisfies the premises, and that is why soundness holds with premises, even infinitely many. From it followed the consistency of every satisfiable set, in particular that of the system, and the method that the unit on deduction lacked: a countermodel proves that a deduction does not exist.

Kalmár and finite completeness

The same lesson proved the converse in two steps. The first is Kalmár's lemma: if the variables of $\varphi$ are among $u_{1}, \ldots, u_{n}$ , then $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ for every valuation $v$ , where $\psi^{v}$ is $\psi$ if $v(\psi) = 1$ and $\neg\psi$ otherwise; the system deduces from each row what the row says about the formula. Its induction on complexity has a single compound case, $(\alpha \downarrow \beta)$ , because joint denial is the only primitive connective, and within it three subcases, which call for two lemmas of the system, the second in two forms: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , deduced with conjunction introduction, double negation and two applications of the rule RDN, and $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ and $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , deduced with disjunction introduction. The second step eliminates the premises: if $\varphi$ is a tautology, it is deduced from the premises of each of the $2^{n}$ rows, and proof by cases eliminates the literal of the last variable, then that of the last but one, until reaching $\vdash \varphi$ , weak completeness. With the semantic deduction theorem and the converse of the syntactic one, completeness was extended to finite sets of premises; whence, for finite premises, deduction and consequence coincide, provable equivalence coincides with semantic equivalence and derivability is decidable, because the table answers for it.

Compactness and strong completeness

The lesson on the compactness theorem faced the infinite case, which Kalmár's lemma does not reach, because infinitely many premises cannot be discharged into an implication. It proved, without mentioning any deduction, that a set is satisfiable if and only if each of its finite subsets is. A sequence of values for $v_{1}, \ldots, v_{n}$ is good if every finite subset of the set is satisfied by some valuation that extends it; the two-witness lemma ensures that a good sequence extends to a good one, because if neither of the two extensions were good, the union of the two finite witnesses would contradict that the sequence is good; and the valuation that results from always preferring the value $1$ when possible satisfies each formula, by the coincidence lemma, because each formula has finitely many variables. The construction does not need the axiom of choice, because the variables are numbered and each step has a rule. From compactness followed its equivalent forms, the unsatisfiability form and the consequence form; from the latter, from completeness for finite sets of premises and from monotonicity, strong completeness; and from this and from soundness, the full coincidence: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ for every $\Gamma$ , and a set is consistent if and only if it is satisfiable. The lesson warned that this order is not a matter of preference: obtaining compactness from a strong completeness not yet available would be circular. It ended with the coloring of countable graphs, which translates an infinite problem into a set of formulas whose finite parts are satisfiable, and with the limits of what a set of formulas can express.

Resolution

The lesson on the resolution method replaced sets of formulas by sets of clauses, each a finite set of literals, with two representations: the clausal form, which has the same models, and the definitional form, which introduces a new variable for each compound written subform, preserves only satisfiability and grows like the formula, not like a power of two. A single rule acts on clauses: from $C$ and $D$ , with $\ell \in C$ and $\ell^{*} \in D$ , one infers $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , and a refutation is a derivation that reaches $\Box$ . Soundness was proved like that of the system, by induction on the derivation and with the resolvent as a consequence of its premises; refutation completeness, by induction on the number of variables, with the elimination of a variable, which preserves satisfiability and whose proof constructs a model; and for infinite sets, once again with compactness. It followed that $\Gamma \models \varphi$ if and only if a clausal form of $\Gamma \cup \{\neg\varphi\}$ has a refutation, and that saturation, finite because with $n$ variables there are no more than $4^{n}$ clauses, decides satisfiability without tables. The lesson presented the satisfiability problem, whose cost in the worst case nobody knows, and two cases that are decided quickly, Horn clauses and clauses of two literals.

The following figure gathers the four segments into a single chain. Each node of the column is 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 come from the previous units, 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 soundness and compactness, established one in the first segment and the other in the third, reappear in the following segments, and that the most visited support of the unit is valuations and coincidence, followed by induction, in its three forms: on the lines of a deduction, on the complexity of a formula and on the number of variables of a set of clauses.

Supports of the chain

AInduction and recursion. Strong induction on the natural numbers, induction on the complexity of formulas, with the single compound case $(\alpha \downarrow \beta)$ , and definition by recursion. They were proved in the first unit. Admitted without proof in this unit.
BCourse system. A1, A2 and A3, modus ponens and the rule RDN; reflexivity, monotonicity, modus ponens between deductions, finiteness and $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . They were established in the second unit. Admitted without proof in this unit.
CDerived techniques. Double negation, from the lesson on the four techniques; conjunction and disjunction introduction and proof by cases (if $\Gamma \cup \{\psi\} \vdash \chi$ and $\Gamma \cup \{\neg\psi\} \vdash \chi$ , then $\Gamma \vdash \chi$ ), from the lesson on the techniques of classical logic. They were proved in the second unit. Admitted without proof in this unit.
DValuations and coincidence. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; if two valuations agree on $V(\varphi)$ , they give $\varphi$ the same value; validity is decided with $2^{n}$ rows. They were proved in the third unit. Admitted without proof in this unit.
ESemantic consequence. False row of the implication, monotonicity, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ if and only if $\Gamma \cup \{\neg\varphi\}$ is unsatisfiable, and the semantic replacement theorem. They were proved in the third unit. Admitted without proof in this unit.
FConjunctive forms. Value lemma; every formula is equivalent to a conjunctive normal form, which may need $2^{n}$ clauses; a disjunction of literals is valid if and only if it contains a complementary pair. They were proved in the third unit. Admitted without proof in this unit.
GSoundness. If $\Gamma \vdash \varphi$ , then $\Gamma \models \varphi$ , for every set $\Gamma$ ; a countermodel proves that a deduction does not exist. Established in: 2. Soundness.
HCompactness. A set of formulas is satisfiable if and only if every finite subset of it is satisfiable; whence what is unsatisfiable is already so in a finite part. Established in: 11. Compactness theorem.

Segment 1 Soundness
- Check that every instance of the schemas is valid without building its table.
- Prove soundness by strong induction on the number of lines, with the case of the rule of replacement of double negation.
- Prove with a countermodel that a formula is not deduced, and obtain consistency from soundness.
1. Validity of the axioms. Every instance of A1, A2 and A3 is valid: a valuation that refuted it would require, through the false row of the implication, impossible values.
  Rests on: E (Semantic consequence). Proved in: Soundness and completeness.
2. Soundness. If $\Gamma \vdash \varphi$ , then $\Gamma \models \varphi$ , for every $\Gamma$ : by strong induction on the number of lines, with one case for the axioms, another for the premises, semantic modus ponens and, for the rule RDN, $\theta \eqsem \neg\neg\theta$ with semantic replacement.
  Uses: 1. Validity of the axioms. Rests on: A (Induction and recursion), B (Course system), E (Semantic consequence). Proved in: Soundness and completeness.
3. Consistency and countermodels. Every satisfiable set is consistent; the system is consistent and $\nvdash v_{1}$ ; if a valuation satisfies $\Gamma$ and refutes $\varphi$ , then $\Gamma \nvdash \varphi$ , and the table certifies that what is not valid is not a theorem.
  Rests on: G (Soundness), D (Valuations and coincidence). Proved in: Soundness and completeness.
Segment 2 Kalmár and finite completeness
- Deduce in the system the two lemmas on joint denial, with the rule of replacement of double negation where needed.
- Prove Kalmár's lemma by induction on complexity, with a single compound case.
- Eliminate with proof by cases the premises of the rows, and discharge finite premises with the two deduction theorems.
- Decide derivability, provable equivalence and consistency from finite premises with the table.
1. Joint denial introduction. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ and $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : the conjunction of the negations is $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; double negation removes the outer one, and the rule RDN the two inner ones.
  Rests on: B (Course system), C (Derived techniques). Proved in: Soundness and completeness.
2. Negated joint denial. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ and $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , because $\neg(\alpha \downarrow \beta)$ is $(\alpha \vee \beta)$ and disjunction introduction suffices.
  Rests on: B (Course system), C (Derived techniques). Proved in: Soundness and completeness.
3. Kalmár's lemma. If $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , then $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ for every valuation $v$ ; the inductive step has a single case, $(\alpha \downarrow \beta)$ , with three subcases according to the values of $\alpha$ and of $\beta$ .
  Uses: 4. Joint denial introduction, 5. Negated joint denial. Rests on: A (Induction and recursion), D (Valuations and coincidence), B (Course system). Proved in: Soundness and completeness.
4. Weak completeness. If $\models \varphi$ , then $\vdash \varphi$ : Kalmár's lemma deduces $\varphi$ from each row, and proof by cases eliminates the literals from the last variable to the first, with $2^{n}$ uses of the lemma and $2^{n} - 1$ of proof by cases.
  Uses: 6. Kalmár's lemma. Rests on: C (Derived techniques). Proved in: Soundness and completeness.
5. Completeness for finite sets of premises. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : the semantic deduction theorem leads to a tautology, weak completeness deduces it and the converse of the deduction theorem gives the premises back.
  Uses: 7. Weak completeness. Rests on: E (Semantic consequence), B (Course system). Proved in: Soundness and completeness.
6. Finite coincidence and decision. For finite $\Gamma$ , $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ , and $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; whence derivability from finite premises is decidable, by the table.
  Uses: 8. Completeness for finite sets of premises. Rests on: G (Soundness), D (Valuations and coincidence). Proved in: Soundness and completeness.
Segment 3 Compactness and strong completeness
- Prove compactness by fixing the values of the variables one by one, with the invariant of good sequences and the two-witness argument.
- Move between the satisfiability form, the unsatisfiability form and the consequence form.
- Obtain strong completeness from compactness, without circularity, and from it the coincidence of consistency with satisfiability.
- Encode in sets of formulas problems about infinite objects and solve them with compactness.
1. Two-witness lemma. If the sequence $s$ of fixed values is good (every finite subset of the set is satisfied by a valuation that extends it), so is $(s, 1)$ or $(s, 0)$ : if neither were, the union of the two finite witnesses would contradict that $s$ is good.
  Rests on: D (Valuations and coincidence). Proved in: The compactness theorem.
2. Compactness theorem. $\Gamma$ is satisfiable if and only if every finite subset is: $v_{n + 1}$ is fixed at $1$ if $(s_{n}, 1)$ is good and at $0$ otherwise, and the resulting valuation satisfies each formula by the coincidence lemma. The axiom of choice is not needed, because the variables are numbered.
  Uses: 10. Two-witness lemma. Rests on: A (Induction and recursion), D (Valuations and coincidence). Proved in: The compactness theorem.
3. Equivalent forms. $\Gamma$ is unsatisfiable if and only if some finite part is; $\Gamma \models \varphi$ if and only if $\Gamma_{0} \models \varphi$ for some finite $\Gamma_{0} \subseteq \Gamma$ ; and this last form implies, in turn, the theorem.
  Uses: 11. Compactness theorem. Rests on: E (Semantic consequence). Proved in: The compactness theorem.
4. Strong completeness. If $\Gamma \models \varphi$ , then $\Gamma \vdash \varphi$ , for every $\Gamma$ : the consequence form gives a finite $\Gamma_{0}$ , completeness for finite sets of premises gives $\Gamma_{0} \vdash \varphi$ , and monotonicity $\Gamma \vdash \varphi$ .
  Uses: 8. Completeness for finite sets of premises, 12. Equivalent forms. Rests on: B (Course system). Proved in: The compactness theorem.
5. Deduction is consequence. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ for every $\Gamma$ ; the theorems are exactly the tautologies, and a set is consistent if and only if it is satisfiable.
  Uses: 13. Strong completeness. Rests on: G (Soundness). Proved in: The compactness theorem.
6. Coloring of countable graphs. With a variable $x_{i,c}$ for each vertex and color, and formulas saying that each vertex has one color and only one and that neighbors differ, a countable graph admits a coloring with $k$ colors if every finite subgraph admits one.
  Rests on: H (Compactness), F (Conjunctive forms). Proved in: The compactness theorem.
Segment 4 Resolution
- Represent a set of formulas as a set of clauses, by the conjunctive form or by the definitional one.
- Build refutations without eliminating two complementary pairs in one step.
- Prove the soundness and the refutation completeness of resolution, for finite sets and, with compactness, for arbitrary ones.
- Decide consequences by saturation and recognize the cases that are decided quickly.
1. Clausal form. A clause is a finite set of literals, satisfied if some literal takes the value $1$ , and $\Box$ is unsatisfiable; a clausal form of $\Gamma$ has the same models, and $\Gamma \models \varphi$ if and only if a clausal form of $\Gamma \cup \{\neg\varphi\}$ is unsatisfiable.
  Rests on: F (Conjunctive forms), E (Semantic consequence). Proved in: The resolution method.
2. Definitional clausal form. With a new variable per written subform and its definition clauses, $T(\varphi)$ is equisatisfiable with $\varphi$ and has at most $4k + 1$ clauses of at most three literals; definitional forms decide consequence from finite premises.
  Uses: 16. Clausal form. Rests on: A (Induction and recursion), D (Valuations and coincidence). Proved in: The resolution method.
3. Soundness of resolution. $\{C, D\} \models R_{\ell}(C, D)$ , by cases on the value of $\ell$ ; by strong induction on the derivation, $S \models C$ for every clause $C$ derived from $S$ , and if $S$ has a refutation, it is unsatisfiable.
  Uses: 16. Clausal form. Rests on: A (Induction and recursion). Proved in: The resolution method.
4. Elimination of a variable. $E_{p}(S)$ , which keeps the clauses without $p$ or $\neg p$ and adds the resolvents on $p$ , does not contain $p$ and is equisatisfiable with $S$ ; from a model of it one obtains a model of $S$ by choosing the value of $p$ .
  Uses: 18. Soundness of resolution. Rests on: D (Valuations and coincidence). Proved in: The resolution method.
5. Finite refutation completeness. Every finite unsatisfiable set of clauses has a refutation, by induction on the number of variables: the last one is eliminated and the premises of each resolvent are inserted.
  Uses: 19. Elimination of a variable. Rests on: A (Induction and recursion). Proved in: The resolution method.
6. Refutation completeness. A set of clauses, finite or infinite, is unsatisfiable if and only if it has a refutation; whence $\Gamma \models \varphi$ if and only if a clausal form of $\Gamma \cup \{\neg\varphi\}$ has a refutation.
  Uses: 16. Clausal form, 18. Soundness of resolution, 20. Finite refutation completeness. Rests on: H (Compactness). Proved in: The resolution method.
7. Saturation decides. With $n$ variables, the set of the derived clauses has at most $4^{n}$ elements; saturation terminates and decides satisfiability without tables, though not always faster than they do.
  Uses: 18. Soundness of resolution, 20. Finite refutation completeness. Proved in: The resolution method.

The end of the course. The chain ends where the two faces of the course are recognized as a single relation and a method for deciding it is available. What remains open is no longer a question about propositional logic, but about its cost and about its extension to quantifiers.