Skip to content
Topos Uranos
English

Induction on the natural numbers and on formulas

Summary

The formulas of propositional logic are infinitely many, and every assertion about all of them requires a method that does not consist in checking them one by one. This lesson builds that method in two stages. The first is induction on the natural numbers, in its simple form and in its strong form, which is derived from the simple one; the second is induction on the complexity of formulas, or structural induction, which is justified by strong induction on length. With it one proves the weight lemma of the language of circles and disks (every formula weighs +1+1 and every nonempty proper word prefix weighs at most 00), and from the lemma one derives that no formula is a proper prefix of another and, from this, unique readability: each compound formula decomposes in only one way into its initial disk and its two components. Unique readability legitimizes, finally, recursive definitions on formulas (length, number of variables and of connective disks, subformulas, depth) and the substitution of one subformula by another.

Learning objectives

  1. Prove properties of the natural numbers by simple induction and by strong induction, checking the base case and locating the flaw in an incorrect induction.
  2. Prove that all formulas have a property by induction on their complexity, treating the variables and the single formation rule as the only cases.
  3. Prove the weight lemma and derive from it that no formula is a proper prefix of another and that every compound formula is uniquely readable.
  4. Define functions on formulas by recursion (length, depth, subformulas, substitution) and prove relations between them by induction.

Assertions about all formulas

In the lesson on the language of propositional logic, formulas were built from two symbols, ∘\sigO and ∙\sigI, which we call circle and disk, and from a single formation rule. There are infinitely many formulas, and many of the assertions that matter refer to all of them: that every formula ends with a disk, that no formula can be read in two ways, that in every formula there is one more variable than connective disks. Such assertions are not formulas of the language we study, but statements about it, formulated in the metalanguage (English, aided by mathematical notation); their proof is therefore not a deduction within a formal system, but an ordinary mathematical argument whose object is the formal system. That is why they are called metatheoretic, or external, proofs.

Now, no number of verified examples proves an assertion about infinitely many objects. It follows that a principle is needed that allows one to conclude, from a finite number of verifications, that a property holds in infinitely many cases. That principle is induction. It is presented first for the natural numbers, where it is more familiar, and then for formulas, where it rests on the former. The same instrument will prove, in the metatheory unit, the soundness and the completeness of the deductive system.