Lemma·L70
Every formula provably implies itself
A classical two-step derivation from the first two propositional axiom schemas alone: no assumptions needed.
For a language
,
, and
:
In words
For any formula, every theory proves that it implies itself - purely from the shapes of the first two propositional axiom schemas, no premises needed.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1Write , the formula " " in prefix notation. This is an instance of schema A1 ( ) taking the schema's and , so is a logical axiom; the length- sequence is a proof of from , giving .
- 2Write , the formula " ". This is an instance of schema A1 taking and , so likewise .
- 3Write , the formula " ". This is an instance of schema A2 ( ) taking , , - matching , , and " " exactly - so .
- 4By modus ponens applied to and (reading as ): , i.e. . Applying modus ponens again to and this: , the claim.
∎
Remarks
The classical two-line derivation of
from
and
alone, present in essentially every treatment of Hilbert systems. Needed for the "
itself" case of the deduction theorem: when
appears verbatim as an assumption entry of a proof from
, deriving
handles it.