# Rule of Theorem Introduction

Jump to navigation
Jump to search

## Definition

We may introduce, at any stage of a proof (citing **TI**), a theorem already proved, or a substitution instance of such a theorem, together with a reference to the theorem that is being cited.

## Proof

This theorem is a corollary of the Rule of Sequent Introduction.

$\blacksquare$

## Application

Using this rule, we can use theorems that we have derived in order to shorten proofs which may otherwise be long and unwieldy.

## Technical Note

When invoking **Rule of Theorem Introduction** in a tableau proof, use the `{{TheoremIntro}}`

template:

`{{TheoremIntro|line|statement|theorem}}`

where:

`line`

is the number of the line on the tableau proof where the Rule of Theorem Introduction is to be invoked`statement`

is the statement of logic that is to be displayed in the**Formula**column,**without**the`$ ... $`

delimiters`theorem`

is the link to the theorem in question that will be displayed in the**Notes**column.

## Sources

- 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