# 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 invoked`pool`

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`$ ... $`

delimiters`depends`

is the line (or lines) of the tableau proof upon which this line directly depends`sequent`

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