This is a list of rules of inference, logical laws that relate to mathematical formulae.
Rules of inference are syntactical transform rules which one can use to infer a conclusion from a premise to create an argument.
A set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if it is sound.
Discharge rules permit inference from a subderivation based on a temporary assumption.
Below, the notation indicates such a subderivation from the temporary assumption
is not mentioned in any hypothesis or undischarged assumptions.
Restriction: No free occurrence of
Restriction: No free occurrence of
Restriction 2: There is no occurrence, free or bound, of
is not mentioned in any hypothesis or undischarged assumptions.
The following are special cases of universal generalization and existential elimination; these occur in substructural logics, such as linear logic.
The rules above can be summed up in the following table.
[1] The "Tautology" column shows how to interpret the notation of a given rule.
All rules use the basic logic operators.
A complete table of "logic operators" is shown by a truth table, giving definitions of all the possible (16) truth functions of 2 boolean variables (p, q): where T = true and F = false, and, the columns are the logical operators: Each logic operator can be used in an assertion about variables and operations, showing a basic rule of inference.
Examples: Machines and well-trained people use this look at table approach to do basic inferences, and to check if other inferences (for the same premises) can be obtained.
), if it rains today, we will go on a canoe trip tomorrow".
To make use of the rules of inference in the above table we let
be the proposition "If it rains today",
be "We will go on a canoe trip tomorrow".
Consider a more complex set of assumptions: "It is not sunny today and it is colder than yesterday".
"We will go swimming only if it is sunny", "If we do not go swimming, then we will have a barbecue", and "If we will have a barbecue, then we will be home by sunset" lead to the conclusion "We will be home by sunset."
Proof by rules of inference: Let
the proposition "It is colder than yesterday",
the proposition "We will be home by sunset".
Using our intuition we conjecture that the conclusion might be
Using the Rules of Inference table we can prove the conjecture easily: