List of rules of inference

Last updated

This is a list of rules of inference, logical laws that relate to mathematical formulae.

Contents

Introduction

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. A sound and complete set of rules need not include every rule in the following list, as many of the rules are redundant, and can be proven with the other rules.

Discharge rules permit inference from a subderivation based on a temporary assumption. Below, the notation

indicates such a subderivation from the temporary assumption to .

Rules for propositional calculus

Rules for negations

Reductio ad absurdum (or Negation Introduction )
Reductio ad absurdum (related to the law of excluded middle)
Ex contradictione quodlibet

Rules for conditionals

Deduction theorem (or Conditional Introduction )
Modus ponens (or Conditional Elimination )
Modus tollens

Rules for conjunctions

Adjunction (or Conjunction Introduction )
Simplification (or Conjunction Elimination )

Rules for disjunctions

Addition (or Disjunction Introduction )
Case analysis (or Proof by Cases or Argument by Cases or Disjunction elimination )
Disjunctive syllogism
Constructive dilemma

Rules for biconditionals

Biconditional introduction
Biconditional elimination

Rules of classical predicate calculus

In the following rules, is exactly like except for having the term wherever has the free variable .

Universal Generalization (or Universal Introduction)

Restriction 1: is a variable which does not occur in .
Restriction 2: is not mentioned in any hypothesis or undischarged assumptions.

Universal Instantiation (or Universal Elimination)

Restriction: No free occurrence of in falls within the scope of a quantifier quantifying a variable occurring in .

Existential Generalization (or Existential Introduction)

Restriction: No free occurrence of in falls within the scope of a quantifier quantifying a variable occurring in .

Existential Instantiation (or Existential Elimination)

Restriction 1: is a variable which does not occur in .
Restriction 2: There is no occurrence, free or bound, of in .
Restriction 3: is not mentioned in any hypothesis or undischarged assumptions.

Rules of substructural logic

The following are special cases of universal generalization and existential elimination; these occur in substructural logics, such as linear logic.

Rule of weakening (or monotonicity of entailment) (aka no-cloning theorem)
Rule of contraction (or idempotency of entailment) (aka no-deleting theorem)

Table: Rules of Inference

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.

Rules of inferenceTautologyName
Modus ponens
Modus tollens
Hypothetical syllogism
Absorption
Conjunction introduction
Conjunction elimination
Disjunction introduction
Disjunction elimination
Disjunctive syllogism
Disjunctive simplification
Resolution
Biconditional introduction

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):

pq 0  1  2  3  4  5  6  7  8  9 101112131415
TTFFFFFFFFTTTTTTTT
TFFFFFTTTTFFFFTTTT
FTFFTTFFTTFFTTFFTT
FFFTFTFTFTFTFTFTFT

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.[ citation needed ]

Example 1

Consider the following assumptions: "If it rains today, then we will not go on a canoe today. If we do not go on a canoe trip today, then we will go on a canoe trip tomorrow. Therefore (Mathematical symbol for "therefore" is ), 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 not go on a canoe today" and let be "We will go on a canoe trip tomorrow". Then this argument is of the form:

Example 2

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 be the proposition "It is sunny today", the proposition "It is colder than yesterday", the proposition "We will go swimming", the proposition "We will have a barbecue", and the proposition "We will be home by sunset". Then the hypotheses become and . Using our intuition we conjecture that the conclusion might be . Using the Rules of Inference table we can prove the conjecture easily:

StepReason
1. Hypothesis
2. Simplification using Step 1
3. Hypothesis
4. Modus tollens using Step 2 and 3
5. Hypothesis
6. Modus ponens using Step 4 and 5
7. Hypothesis
8. Modus ponens using Step 6 and 7

See also

Related Research Articles

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for all x, if x is a man, then x is mortal"; where "for all x" is a quantifier, x is a variable, and "... is a man" and "... is mortal" are predicates. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation. Some sources include other connectives, as in the table below.

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

In classical, deductive logic, a consistent theory is one that does not lead to a logical contradiction. A theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when there is no formula such that and . A trivial theory is clearly inconsistent. Conversely, in an explosive formal system every inconsistent theory is trivial. Consistency of a theory is a syntactic notion, whose semantic counterpart is satisfiability. A theory is satisfiable if it has a model, i.e., there exists an interpretation under which all axioms in the theory are true. This is what consistent meant in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead.

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

In propositional logic, the double negation of a statement states that "it is not the case that the statement is not true". In classical logic, every statement is logically equivalent to its double negation, but this is not true in intuitionistic logic; this can be expressed by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.

In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula P, if it is provable in PA that "if P is provable in PA then P is true", then P is provable in PA. If Prov(P) means that the formula P is provable, we may express this more formally as

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen (1955).

<span class="mw-page-title-main">LSZ reduction formula</span> Connection between correlation functions and the S-matrix

In quantum field theory, the Lehmann–Symanzik–Zimmermann (LSZ) reduction formula is a method to calculate S-matrix elements from the time-ordered correlation functions of a quantum field theory. It is a step of the path that starts from the Lagrangian of some quantum field theory and leads to prediction of measurable quantities. It is named after the three German physicists Harry Lehmann, Kurt Symanzik and Wolfhart Zimmermann.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

In abstract algebraic logic, a branch of mathematical logic, the Leibniz operator is a tool used to classify deductive systems, which have a precise technical definition and capture a large number of logics. The Leibniz operator was introduced by Wim Blok and Don Pigozzi, two of the founders of the field, as a means to abstract the well-known Lindenbaum–Tarski process, that leads to the association of Boolean algebras to classical propositional calculus, and make it applicable to as wide a variety of sentential logics as possible. It is an operator that assigns to a given theory of a given sentential logic, perceived as a term algebra with a consequence operation on its universe, the largest congruence on the algebra that is compatible with the theory.

In logic, more specifically proof theory, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style system, Hilbert-style proof system, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of formal proof system attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

In logic and mathematics, contraposition, or transposition, refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as § Proof by contrapositive. The contrapositive of a statement has its antecedent and consequent inverted and flipped.

In logic, the scope of a quantifier or connective is the shortest formula in which it occurs, determining the range in the formula to which the quantifier or connective is applied. The notions of a free variable and bound variable are defined in terms of whether that formula is within the scope of a quantifier, and the notions of a dominant connective and subordinate connective are defined in terms of whether a connective includes another within its scope.

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories are referred to as "the formal theories of ν-times iterated inductive definitions". IDν extends PA by ν iterated least fixed points of monotone operators.

In mathematics, Rathjen's  psi function is an ordinal collapsing function developed by Michael Rathjen. It collapses weakly Mahlo cardinals to generate large countable ordinals. A weakly Mahlo cardinal is a cardinal such that the set of regular cardinals below is closed under . Rathjen uses this to diagonalise over the weakly inaccessible hierarchy.

A non-normal modal logic is a variant of modal logic that deviates from the basic principles of normal modal logics.

References

  1. Kenneth H. Rosen: Discrete Mathematics and its Applications, Fifth Edition, p. 58.