Sentential Logic: Metatheory

There are infinitely many sentences of SL, so no claim about all of them can be checked one at a time. Induction gets around this by sorting sentences into a series of groups (usually by number of connectives) and proving two things.

The book uses strong induction: the hypothesis covers all earlier groups, not just the previous one. Nothing is lost, since anything provable by weak induction is provable by strong induction.

The book's examples

First, that every sentence of SL has as many left as right parentheses. Then the dual of a TWA sentence (one using only ~, ∨ and &): swap ∨ and & and put a tilde in front of every atomic component. The thesis is that a TWA sentence and its dual always have opposite truth-values. The inductive step splits into cases by the main connective, which is the usual pattern.

A truth-function of n arguments maps each combination of n truth-values to a truth-value. There are 2⁽²ⁿ⁾ of them: 4 of one argument, 16 of two, 256 of three. SL's five connectives define only five, so it isn't obvious that SL can express them all.

The algorithm

1. Use the first n sentence letters.
2. For each row where the function's value is T, write an iterated conjunction that is true on exactly that row: the letter if it's T in that row, its negation if it's F.
3. Disjoin those conjunctions. If no row is T, use a sentence that is false on every row instead.

Consequences: {~, ∨} is complete, since P & Q is equivalent to ~ (~ P ∨ ~ Q). So are {~, &} and {~, ⊃}. But {∨, &} is not: with no tilde you can never get F when every atom is T, which is a neat induction proof.

The proof is by induction on line numbers in a derivation. The claim proved for each line i: the set Γ_i of open assumptions in whose scope the sentence P_i lies truth-functionally entails P_i.

• Basis: the first line is an assumption, and {P₁} ⊨ P₁.
• Inductive step: one case per rule. For each rule, if the cited lines are entailed by their open assumptions, the new line is entailed by its own. The subderivation rules need care, because they discharge an assumption.

Applied to the last line of a derivation of P from Γ, this gives Γ ⊨ P. Corollaries: every argument valid in SD is truth-functionally valid, and every theorem is truth-functionally true. SD+ is sound too, since its extra rules preserve entailment.

The proof is not constructive: it shows a derivation exists without saying how to build it. It follows Leon Henkin's 1949 method, which returns in Chapter 11 for predicate logic, where no constructive proof is available.

Key idea: a set that is maximally consistent in SD is consistent and can't take any new sentence without becoming inconsistent. For such a set, membership behaves just like truth: ~ P is in it exactly when P isn't, P & Q exactly when both are, and so on (6.4.11). So making its atoms true makes all its members true.