Rule of Sequent Introduction
Jump to navigation
Jump to search
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.
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 \left({P_2 \implies \left({P_3 \implies \left({\ldots \implies \left({P_n \implies Q}\right) \ldots }\right)}\right)}\right)$
$\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:
line
is the number of the line on the tableau proof where Rule of Sequent Introduction is to be invokedpool
is the pool of assumptions (comma-separated list)statement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimitersdepends
is the line (or lines) of the tableau proof upon which this line directly dependssequent
is 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.2$: The Rule of Replacement