Rules of Inference

Rules of inference provide valid patterns for deriving conclusions from known statements.

What are Rules of Inference?

A rule of inference is a logical principle that allows us to derive a conclusion from one or more premises.

In other words, rules of inference tell us when a conclusion logically follows from information that we already know.

They are fundamental to formal proofs and are used throughout mathematics, computer science, and logical reasoning.

Propositional Rules

Propositional inference rules operate on complete propositions using logical connectives such as AND (∧), OR (∨), NOT (¬), and implication (→).

Modus Ponens

Modus Ponens, also called the Law of Detachment, allows us to conclude Q when P implies Q and P is known to be true.

For example:

Modus Tollens

Modus Tollens, also called the Law of Contrapositive, allows us to conclude that P is false when P implies Q and Q is false.

Hypothetical Syllogism

Hypothetical Syllogism combines two conditional statements into a third.

Disjunctive Syllogism

Disjunctive Syllogism allows us to determine one part of an OR statement when the other part is known to be false.

Conjunction

Conjunction allows two known true statements to be combined into a single statement using AND.

Simplification

Simplification allows us to extract either part of a conjunction.

Since both P and Q are true, P is necessarily true. The same rule can also be used to conclude Q.

Addition

Addition allows a true proposition to be combined with any other proposition using OR.

If P is true, then "P or Q" must also be true, regardless of the truth value of Q.

Absorption

Absorption transforms a conditional statement into another conditional statement that includes both the original proposition and its consequence.

Resolution

Resolution combines two disjunctions containing a proposition and its negation.

The complementary pair P and ¬P is eliminated, leaving a conclusion involving the remaining propositions.

Predicate Logic Rules

Predicate logic uses the propositional rules above and adds rules for working with variables and quantifiers.

These rules allow us to move between statements about individual objects and statements about entire domains.

Universal Instantiation

Universal Instantiation allows us to obtain a statement about a particular object from a statement that applies to every object.

Universal Generalization

Universal Generalization allows us to establish a universal statement when a property has been proven for an arbitrary member of the domain.

The important condition is that the object c must be arbitrary rather than a specially chosen object.

Existential Instantiation

Existential Instantiation allows us to introduce a specific name for an object when we know that at least one object with a particular property exists.

Here, c represents some particular object that satisfies P. The object is known to exist, but its identity does not have to be known beforehand.

Existential Generalization

Existential Generalization works in the opposite direction. If a property is known to hold for a particular object, then at least one object with that property exists.

Summary

Rules of inference provide the building blocks for formal reasoning. Propositional rules operate on statements, while predicate-logic rules extend this reasoning to variables and quantifiers.

By applying these rules correctly, a sequence of valid steps can be used to construct a formal proof.