## Induction and recursion II May 28, 2008

Posted by David Pierce in Uncategorized.

Formal logic provides examples of structures that allow proof by induction, but not necessarily definition by recursion. Let us consider, for example, the propositional logic that is apparently due to Łukasiewicz. We first define the (well-formed) formulas of the logic. We start with some set of so-called propositional variables. Then the set of formulas is the smallest set of strings that contains these variables and is closed under certain formation rules, namely:

1. the singulary operation converting a string S to its negation, ~S;
2. the binary operation converting a pair (S, T) of strings to the implication, (S → T).

The set of theorems of the logic is the smallest set of formulas that contains all of the axioms and is closed under a certain rule of inference. The axioms are the formulas of any of three forms:

1. (F → (G → F))
2. ((F → (G → H)) → ((F → G) → (F → H)))
3. ((~F → ~G) → (G → F))

Here F and G stand for formulas. The rule of inference is detachment (or modus ponens), the binary operation that converts a pair (F, (F → G)) of formulas into the formula G. As stated, this is only a partial operation; we can make it total by having it convert (F, H) to F whenever H does not have the form (F → G) for some formula G.
The “inductive” definition of theorems is thus similar to the inductive definition of formulas. In each case, we start with a set and close under one or more operations. Immediately, proof by induction is possible on the set so defined. For example, we can prove inductively that each formula features as many left as right brackets. A feature of theorems that is proved by induction will be given in a moment.
However, unlike the formation rules for formulas, our rule of inference for theorems is not obviously well-defined. To see that it is well-defined, we must establish “unique readability” of formulas, namely:

1. each formula is exactly one of the following: a variable, a negation, or an implication;
2. the formation rules are injective.

Here injectivity of the formation rules corresponds to injectivity of the successor-operation on the set of natural numbers. The partition of the set of formulas into variables, negations, and implications corresponds to the partition of the set of natural numbers into the successors and the initial number (zero or one, as one prefers).
Unique readability of formulas allows recursive definitions. Indeed, the definition of the rule of detachment can be understood as recursive: If we denote this operation by D, then we have

1. D(F, P) = F for all propositional variables P;
2. D(F, ~G) = F;
3. D(F, (F → G)) = G;
4. D(F, (H → G)) = F if H is not F.

Another example of a recursively defined function on formulas is a truth-assignment. Consider the set {true, false} as the two-element field {1, 0}. Given a function φ from the set of propositional variables into the this field, we have a unique function Φ on the set of all formulas that agrees with φ on the variables, that takes ~F to 1 + Φ(F), and that takes (F → G) to 1 + Φ(F) + Φ(F)Φ(G).
By induction, every theorem takes the value 1 under every truth-assignment. But the truth-assignment is not recursively defined on the set of theorems: it is recursively defined on the set of formulas. Since the rule of detachment is not injective, we do not automatically have recursively defined functions on the set of theorems.
As far as I know, we do not have an efficient algorithm to determine whether a given formula is indeed a theorem: this lack of an algorithm would appear to be connected to the non-injectivity of the rule of detachment. A formula carries within itself the method of its construction; but a theorem does not carry within itself its proof, and indeed it will have infinitely many proofs.

1. wmstem - October 14, 2009

Good explanation.

Is it possible to prove modus ponens must be a valid rule of inference?

2. wmstem - October 14, 2009

I am looking for a way which does not involve a truth table.

David Pierce - October 20, 2009

Why?