Rule of Sequent Introduction
If you are familiar with this area of mathematics, you may be able to help improve $\mathsf{Pr} \infty \mathsf{fWiki}$ by determining the precise term which is to be used.
To discuss it in more detail, feel free to use the talk page.
When this has been done, {{Disambiguate}} should be removed 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).
Theorem
Let the statements $P_1, P_2, \ldots, P_n$ be conclusions in a proof, on various assumptions.
Let $P_1, P_2, \ldots, P_n \vdash Q$ be a substitution instance of a sequent for which we already have a proof.
Question the use of "substitution instance": can we not "just" allow for $P_1, \ldots, P_n$ to be "just" statements?
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
Then we may introduce, at any stage of a proof (citing SI), either:
- The conclusion $Q$ of the sequent already proved
or:
- A substitution instance of such a conclusion, together with a reference to the sequent that is being cited.
This conclusion depend upon the pool of assumptions upon which $P_1, P_2, \ldots, P_n \vdash Q$ rests.
This is called the rule of sequent introduction.
Proof
By hypothesis and substitution instance we have a proof, using primitive rules, of:
- $P_1, P_2, \ldots, P_n \vdash Q$
By the Extended Rule of Implication, we have:
- $\vdash P_1 \implies \paren {P_2 \implies \paren {P_3 \implies \paren {\ldots \implies \paren {P_n \implies Q} \ldots} } }$
$\blacksquare$
Also known as
This rule is also known as the rule of replacement.
Also see
- Rule of Theorem Introduction, which is a direct corollary of this.
Thus we can convert any sequent into a theorem so as to use results already calculated in order to prove further results.
Technical Note
When invoking Rule of Sequent Introduction in a tableau proof, use the {{SequentIntro}} template:
{{SequentIntro|line|pool|statement|depends|sequent}}
where:
lineis the number of the line on the tableau proof where Rule of Sequent Introduction is to be invokedpoolis the pool of assumptions (comma-separated list)statementis the statement of logic that is to be displayed in the Formula column, without the$ ... $delimitersdependsis the line (or lines) of the tableau proof upon which this line directly dependssequentis the link to the sequent in question that will be displayed in the Notes column.
Sources
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 3.9$: Derivation by Substitution
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 4$
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): $\S 2.2$: Theorems and Derived Rules
- 1973: Irving M. Copi: Symbolic Logic (4th ed.) ... (previous) ... (next): $3$: The Method of Deduction: $3.2$: The Rule of Replacement