LEARNING OBJECTIVES:
By the end of this class, the student will be able to:

1. Understand the concept of induction on the complexity of expressions.
2. Apply mathematical induction on the complexity of formulas in propositional logic.
3. Understand the proof by induction on complexity and how it is applied in propositional logic.

INDEX
INDUCTION ON COMPLEXITY
A SIMPLE EXAMPLE: THE SUBSTITUTION THEOREM

Induction on Complexity

Suppose we want to prove that a property \mathcal{P} holds for any expression F. One way to demonstrate this is by using the variant of mathematical induction known as “induction on the complexity of expressions.” This is done through the following series of steps:

• First, we show that all atomic expressions satisfy this property (this corresponds to the case n=1 in traditional induction).
• Then, assuming that it holds for any expressions F and G, we prove that as a consequence it holds for expressions of the form F\downarrow G; or equivalently, for \neg F and any of the following: F\wedge G, F\vee G, F\rightarrow G.

If we manage to do this, then we conclude that the property \mathcal{P} holds for all expressions in propositional logic. This is what we call “mathematical induction on the complexity of expressions.”

A Simple Example: The Substitution Theorem

To get a better idea of how induction is performed on the complexity of formulas, we will review the (meta) substitution theorem

Suppose that F\equiv G. Let H be an expression containing F as a sub-expression, and let H^\prime be the expression obtained by replacing all occurrences of F with G, then H\equiv H^\prime.

Proof by Induction on the Complexity of Formulas

To prove by induction on complexity is to show two things: 1) a base case (for atomic formulas), and 2) the inductive step (if it works for any expressions F and G, then it works for F\downarrow G, or more simply: it works for \neg F and at least one of the following: F\vee G, F\wedge G, F\rightarrow G, or F\leftrightarrow G).

Suppose that H is an atomic expression, F is a sub-expression of H, and F\equiv G. If H^\prime is the result of replacing all sub-expressions F in H, since H is atomic, it will hold that H^\prime \equiv G. On the other hand, since H is atomic and F is a sub-expression of H, then H\equiv F. Finally, we will have:

H\equiv F \equiv G \equiv H^\prime

Thus, the base case for atomic expressions is demonstrated.

Now, let’s look at the inductive case.

The Induction Hypothesis

Suppose the theorem works for two arbitrary expressions H_1 and H_2, each containing F as a sub-expression with F \equiv G. Then it will follow that if H_1^\prime is the result of replacing all F with G in H_1 and H_2^\prime is the result of replacing all F with G in H_2, then we will have H_1\equiv H_1^\prime and H_2\equiv H_2^\prime.

The Inductive Step

Here we will check if, as a consequence of the induction hypothesis, the theorem also holds for \neg H_1 (or \neg H_2, either of the two) and for at least one of the following: H_1 \wedge H_2, H_1 \vee H_2, H_1 \rightarrow H_2.

If H:= \neg H_1, then, by the induction hypothesis, it will follow that H\equiv \neg H_1^\prime=: H^\prime , where H^\prime is the result of replacing all occurrences of F in H with G. Therefore, H\equiv H^\prime.

Similarly, if H:= H_1 \wedge H_2, then, by the induction hypothesis, it will follow that H\equiv H_1^\prime \wedge H_2 \equiv H_1^\prime \wedge H_2^\prime =: H^\prime , where H^\prime is the result of replacing all occurrences of F in H with G. Therefore, H\equiv H^\prime.

Thus, the induction is complete, and the substitution theorem holds for all expressions in propositional logic.

By applying this form of induction, it can be ensured that a property holds for all expressions in a logical system, which is especially useful in propositional logic for structuring rigorous proofs. Moreover, its utility extends to fields such as artificial intelligence and software development, where the verification of logical systems is essential. Through this technique, proofs can be automated and the consistency of complex expressions can be ensured, reducing the risk of errors and improving accuracy in environments that rely on mathematical and logical validity.