Substitution Instance
Contents |
Context
This proof is demonstrated in the field of natural deduction, but is broadly applicable in other fields of mathematics.
Theorem
Let $S$ be a sequent that has been proved.
Then a proof can be found for any substitution instance of $S$.
Proof
This is apparent from inspection of the proof rules themselves.
The rules concern only the broad structure of the statement forms involved, and this structure is unaffected by substitution.
By performing the substitutions systematically throughout the given sequent, all applications of proof rules remain correct applications in the sequent.
You can help ProofWiki by adding precise reasons why such statements hold.
To discuss it in more detail, feel free to use the talk page.
If you are able to do this, then when you have done so you can remove this instance of {{Handwaving}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Applications
This proof leads on to the Rule of Sequent Introduction.
Sources
- Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 4$
