Replacement More about propositional logic

This is a technical aside to the Logic Notes, containing a proof of a fact asserted in the body of the notes. It may be skipped by anyone willing to take that assertion on trust, as it assumes rather more mathematical background than is required to follow the general exposition of logic.

Theorem: Let L be an atom (a sentence letter such as p or q) and let C be a formula of propositional logic, in which of course L occurs zero or more times. Let A and B be propositional formulae such that   A ⊣⊢ B.  Then   C^A_L TS  C^B_L.

Proof: The proof is by induction on the structure of C (or, if we prefer, on the number of connective occurrences in C). In the base case C contains no connectives; then either C = p for some p ≠ L, in which case C^A_Land C^B_Lare both just p, or else C = L, and C^A_Land C^B_Lare A and B respectively, leaving nothing to prove. Now for the induction step, suppose C is not atomic and the theorem holds for all of its proper subformulae.

For ease of reading, in what follows we omit the subscript L.

The main connective of C may be any one of the four for which we have natural deduction rules. The four cases are as follows (click to expand):

Case 1:   C = NOTD

Clearly, C^A is the negation of D^A, and similarly C^B is the negation of D^B. Now, on induction hypothesis, we know that D^A is provably equivalent to D^B. Then we can derive NOTD^B from NOTD^A : SP {} PL {1} {1} {D^B} {A} PL {1} {2} {D^A} {1   somehow (because D^B TS D^A)} PL {3} {3} {NOTD^A} {A} PL {3} {4} {NOTD^B} {2, 3 [1] RAA} EP

Case 2:   C = D AND E

For case 2, similarly, we have on induction hypothesis a derivation of D^B from D^A and one of E^B from E^A, so we can argue: SP {} PL {1} {1} {D^A AND E^A} {A} PL {1} {2} {D^A} {1 ANDE} PL {1} {3} {E^A} {1 ANDE} PL {1} {4} {D^B} {2   somehow (because D^A TS D^B)} PL {1} {5} {E^B} {3   somehow (because E^A TS E^B)} PL {1} {6} {D^B AND E^B} {4, 5 ANDI} EP

Case 3:   C = D OR E

By the induction hypothesis,  D^A TS D^B  and E^A TS E^B.  So: SP {} PL {1} {1} {D^A OR E^A} {A} PL {2} {2} {D^A} {A} PL {2} {3} {D^B} {2   somehow (because D^A TS D^B)} PL {2} {4} {D^B OR E^B} {3 ORI} PL {5} {5} {E^A} {A} PL {5} {6} {E^B} {5   somehow (because E^A TS E^B)} PL {5} {7} {D^B OR E^B} {6 ORI} PL {1} {8} {D^B OR E^B} {1, 4 [2], 7 [5] ORE} EP

Case 4:   C = D IMP E

By the induction hypothesis,  D^B TS D^A  and E^A TS E^B.  So: SP {} PL {1} {1} {D^A IMP E^A} {A} PL {2} {2} {D^B} {A} PL {2} {3} {D^A} {2   somehow (because D^B TS D^A)} PL {1,2} {4} {E^A} {1, 3 IMPE} PL {1,2} {5} {E^B} {4   somehow (because E^A TS E^B)} PL {1} {6} {D^B IMP E^B} {5 [2] IMPI} EP

Those being all the cases, the result is proved. Note that since the double negation rule NOTNOTE is not required for this proof, the result continues to hold if that rule is dropped. With suitable adjustments, in fact, it holds of a very wide range of logical systems, including those to come later in these notes.