Lemma·L69
Modus ponens as a derived rule on provability
If a theory proves a formula and proves that formula implies another, it proves the other - by concatenating the two witnessing proofs and appending one more step.
For a language
,
, and
: if
and
, then
.
In words
For any two formulas: if the theory proves the first and proves that the first implies the second, it proves the second - concatenate the two proofs and tack the conclusion on as one more modus-ponens step.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1Let be a proof of from , of length , and a proof of from , of length . Let , of length .
- 2For : (T29), justified exactly as it was within (its justification, if by modus ponens or generalization, cites indices , unaffected by anything appended after position ).
- 3For : (T29). If was justified within by modus ponens from ( ) or generalization from ( ), then in the same relationship holds shifted by : is justified from (and ), with - a valid justification within . A logical axiom or a member of needs no shifting to remain a valid justification.
- 4
- 5So is a proof of from : .
∎
Remarks
The single most-used derived rule from here on: chaining implications through provability without having to write out a fresh proof object by hand each time. The shifting argument in the middle step mirrors the Locality-style reasoning used throughout this wiki's syntax chapters: concatenating two valid structures and re-indexing the second piece preserves whatever made it valid on its own.