The fundamental rules of inference are classified according to the logical operators that appear in them.
Some rules of inference ask you to temporarily assume something. You should think of these assumptions as taking place in a separate hypothetical world. Anything true in the real world is true in the hypothetical world, but not the other way around. So conclusions from the hypothetical world may not be brought back into the real world, except as specified by the rule of inference. (In a complicated proof, there might be hypothetical worlds within hypothetical worlds within ..., and all of these need to be kept separate.)
T introduction | F elimination |
---|---|
No matter what, | If we know F, |
we can deduce T. | then we can deduce anything. |
∧ (AND) introduction | ∨ (OR) elimination |
If we know P and we know Q, | If we know P ∨ Q and assuming P gives us R and assuming Q gives us R, |
then we can deduce P ∧ Q. | then we can deduce R. |
∨ (OR) introduction (left) | ∧ (AND) elimination (left) |
If we know P, | If we know P ∧ Q, |
then we can deduce P ∨ Q. | then we can deduce P. |
∨ (OR) introduction (right) | ∧ (AND) elimination (right) |
If we know Q, | If we know P ∧ Q, |
then we can deduce P ∨ Q. | then we can deduce Q. |
→ introduction | → elimination |
If assuming P gives us Q, | If we know P and we know P → Q, |
then we can deduce P → Q. | then we can deduce Q. |
¬ introduction | ¬ elimination |
No matter what, | If we know P and we know ¬P, |
we can deduce P ∨ ¬P. | then we can deduce F. |
Also use these definitions:
∀ introduction | ∀ elimination |
---|---|
If assuming a variable x gives us P(x), | If we know ∀x P(x) and we have y, |
then we can deduce ∀x P(x). | then we can deduce P(y). |
∃ introduction | ∃ elimination |
If we have y and we know P(y), | If we know ∃x P(x), |
then we can deduce ∃x P(x). | then we can construct a constant x and deduce P(x). |
This web page was written in 2003 by Toby Bartels. Toby reserves no legal rights to it.
The permanent URI of this web page
is
http://tobybartels.name/MATH112/2003/inference/
.