Using double induction to prove soundness of Natural Deduction?

117 Views Asked by At

In Teller's Formal Logic Premier, the chapter on proving soundneds of natural deduction in proposition logic mentions one method other than the trivial one:

The straightforward but messy procedure in our present case is to do a double induction.One defines the complexity of a derivation as the number of levels of subderivations which occur.The inductive property is that all derivations of complexity n are sound.One then assumes the inductive hypothesis, that all derivations with complexity less than n are sound, and proves that all derivations of complexity n are sound.In this last step one does another induction on the number of lines of the derivation.

where complexity is defined in terms of the "level" of "subdeviation" of the proof; subdeviation is deviations with the introduced provisional assumption when using rules that introduction of imply and introduction of negation ( in the introduction of imply cases is p...q | p->q; in the introduction of negation cases is p...a V ~a | ~p); the "level" is the number of subdeviations of the subdeviation which contains the most subdeviations.

1

There are 1 best solutions below

0
On BEST ANSWER

Long comment

The "inner" induction is simple: it consider the lines in the subderivation. The proof amounts to check that each rule is sound, i.e. that it preserves truth.

Thus, if we assume the induction hypotheses that the previous $n-1$ lines in the subderivation are true, we have that the $n$-th line must be true also, because it is obtained applying one of the rules.

This inductive proof amounts to saying that "linear" derivations, i.e. derivations without subderivations are sound.

Then we have to use it in the main proof, regarding a "general" derivation with $k$ levels of subderivations (i.e. $k$ "nested" subderivations).