HOME

TheInfoList



OR:

This is a list of
rules of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
, logical laws that relate to mathematical formulae.


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 : \varphi \vdash \psi indicates such a subderivation from the temporary assumption \varphi to \psi.


Rules for classical sentential calculus

Sentential calculus is also known as
propositional calculus 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 (which can be true or false) and relations b ...
.


Rules for negations

;
Reductio ad absurdum In logic, (Latin for "reduction to absurdity"), also known as (Latin for "argument to absurdity") or ''apagogical arguments'', is the form of argument that attempts to establish a claim by showing that the opposite scenario would lead to absu ...
(or ''Negation Introduction''): : \varphi \vdash \psi : \underline : \lnot \varphi ;Reductio ad absurdum (related to the
law of excluded middle In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradi ...
): : \lnot \varphi \vdash \psi : \underline : \varphi ;'' Ex contradictione quodlibet'': : \varphi : \underline : \psi ;
Double negation elimination In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not ( ...
: : \underline : \varphi ; Double negation introduction: : \underline : \lnot \lnot \varphi


Rules for conditionals

;
Deduction theorem In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...
(or '' Conditional Introduction''): : \underline : \varphi \rightarrow \psi ;
Modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference ...
(or ''Conditional Elimination''): : \varphi \rightarrow \psi : \underline : \psi ;
Modus tollens In propositional logic, ''modus tollens'' () (MT), also known as ''modus tollendo tollens'' (Latin for "method of removing by taking away") and denying the consequent, is a deductive argument form and a rule of inference. ''Modus tollens' ...
: : \varphi \rightarrow \psi : \underline : \lnot \varphi


Rules for conjunctions

; Adjunction (or ''Conjunction Introduction''): : \varphi : \underline : \varphi \land \psi ; Simplification (or ''Conjunction Elimination''): : \underline : \varphi : \underline : \psi


Rules for disjunctions

;
Addition Addition (usually signified by the plus symbol ) is one of the four basic operations of arithmetic, the other three being subtraction, multiplication and division. The addition of two whole numbers results in the total amount or '' sum'' ...
(or ''Disjunction Introduction''): : \underline : \varphi \lor \psi : \underline : \varphi \lor \psi ; Case analysis (or ''Proof by Cases'' or ''Argument by Cases'' or ''Disjunction elimination'') : \varphi \rightarrow \chi : \psi \rightarrow \chi : \underline : \chi ;
Disjunctive syllogism In classical logic, disjunctive syllogism (historically known as ''modus tollendo ponens'' (MTP), Latin for "mode that affirms by denying") is a valid argument form which is a syllogism having a disjunctive statement for one of its premises ...
: : \varphi \lor \psi : \underline : \psi : \varphi \lor \psi : \underline : \varphi ;
Constructive dilemma Constructive dilemmaCopi and Cohen is a valid rule of inference of propositional logic. It is the inference that, if ''P'' implies ''Q'' and ''R'' implies ''S'' and either ''P'' or ''R'' is true, then either ''Q or S'' has to be true. In sum, i ...
: \varphi \rightarrow \chi : \psi \rightarrow \xi : \underline : \chi \lor \xi


Rules for biconditionals

;
Biconditional introduction In propositional logic, biconditional introductionCopi and Cohen is a valid rule of inference. It allows for one to infer a biconditional from two conditional statements. The rule makes it possible to introduce a biconditional statement into ...
: : \varphi \rightarrow \psi : \underline : \varphi \leftrightarrow \psi ;
Biconditional elimination Biconditional elimination is the name of two valid rules of inference of propositional logic. It allows for one to infer a conditional from a biconditional. If P \leftrightarrow Q is true, then one may infer that P \to Q is true, and also that ...
: : \varphi \leftrightarrow \psi : \underline : \psi : \varphi \leftrightarrow \psi : \underline : \varphi : \varphi \leftrightarrow \psi : \underline : \lnot \psi : \varphi \leftrightarrow \psi : \underline : \lnot \varphi : \varphi \leftrightarrow \psi : \underline : \psi \land \varphi : \varphi \leftrightarrow \psi : \underline : \lnot \psi \land \lnot \varphi


Rules of classical

predicate calculus Predicate or predication may refer to: * Predicate (grammar), in linguistics * Predication (philosophy) * several closely related uses in mathematics and formal logic: **Predicate (mathematical logic) **Propositional function ** Finitary relation, ...

In the following rules, \varphi(\beta / \alpha) is exactly like \varphi except for having the term \beta wherever \varphi has the free variable \alpha. ;
Universal Generalization In predicate logic, generalization (also universal generalization or universal introduction,Moore and Parker GEN) is a valid inference rule. It states that if \vdash \!P(x) has been derived, then \vdash \!\forall x \, P(x) can be derived. Gener ...
(or Universal Introduction): : \underline : \forall \alpha\, \varphi Restriction 1: \beta is a variable which does not occur in \varphi.
Restriction 2: \beta is not mentioned in any hypothesis or undischarged assumptions. ; Universal Instantiation (or Universal Elimination): : \forall \alpha\, \varphi : \overline Restriction: No free occurrence of \alpha in \varphi falls within the scope of a quantifier quantifying a variable occurring in \beta. ;
Existential Generalization In predicate logic, existential generalization (also known as existential introduction, ∃I) is a valid rule of inference that allows one to move from a specific statement, or one instance, to a quantified generalized statement, or existentia ...
(or Existential Introduction): : \underline : \exists \alpha\, \varphi Restriction: No free occurrence of \alpha in \varphi falls within the scope of a quantifier quantifying a variable occurring in \beta. ;
Existential Instantiation In predicate logic, existential instantiation (also called existential elimination)Moore and Parker is a rule of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a ...
(or
Existential Elimination In predicate logic, existential instantiation (also called existential elimination)Moore and Parker is a rule of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting o ...
): : \exists \alpha\, \varphi : \underline : \psi Restriction 1: \beta is a variable which does not occur in \varphi.
Restriction 2: There is no occurrence, free or bound, of \beta in \psi.
Restriction 3: \beta 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 Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also ...
. ;Rule of weakening (or
monotonicity of entailment Monotonicity of entailment is a property of many logical systems that states that the hypotheses of any derived fact may be freely extended with additional assumptions. In sequent calculi this property can be captured by an inference rule called ...
) (aka
no-cloning theorem In physics, the no-cloning theorem states that it is impossible to create an independent and identical copy of an arbitrary unknown quantum state, a statement which has profound implications in the field of quantum computing among others. The theore ...
) : \alpha\vdash\beta : \overline ;Rule of contraction (or
idempotency of entailment Idempotency of entailment is a property of logical systems that states that one may derive the same consequences from many instances of a hypothesis as from just one. This property can be captured by a structural rule called contraction, and in s ...
) (aka no-deleting theorem) : \underline : \alpha,\gamma\vdash\beta


Table: Rules of Inference

The rules above can be summed up in the following table.Kenneth H. Rosen: ''Discrete Mathematics and its Applications'', Fifth Edition, p. 58. 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 A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—which sets out the functional values of logical expressions on each of their functional arg ...
, 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: 0, false,
Contradiction In traditional logic, a contradiction occurs when a proposition conflicts either with itself or established fact. It is often used as a tool to detect disingenuous beliefs and bias. Illustrating a general tendency in applied logic, Aristotle's ...
; 1, NOR, Logical NOR (Peirce's arrow); 2, Converse nonimplication; 3, ¬p,
Negation In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
; 4,
Material nonimplication Material nonimplication or abjunction ( Latin ''ab'' = "from", ''junctio'' =–"joining") is the negation of material implication. That is to say that for any two propositions P and Q, the material nonimplication from P to Q is true if ...
; 5, ¬q, Negation; 6, XOR,
Exclusive disjunction Exclusive or or exclusive disjunction is a logical operation that is true if and only if its arguments differ (one is true, the other is false). It is symbolized by the prefix operator J and by the infix operators XOR ( or ), EOR, EXOR, , ...
; 7, NAND, Logical NAND (Sheffer stroke); 8, AND,
Logical conjunction In logic, mathematics and linguistics, And (\wedge) is the truth-functional operator of logical conjunction; the ''and'' of a set of operands is true if and only if ''all'' of its operands are true. The logical connective that represents thi ...
; 9, XNOR,
If and only if In logic and related fields such as mathematics and philosophy, "if and only if" (shortened as "iff") is a biconditional logical connective between statements, where either both statements are true or both are false. The connective is bic ...
, Logical biconditional; 10, q,
Projection function In set theory, a projection is one of two closely related types of functions or operations, namely: * A set-theoretic operation typified by the ''j''th projection map, written \mathrm_, that takes an element \vec = (x_1,\ \ldots,\ x_j,\ \ldots,\ x ...
; 11, if/then, Logical implication; 12, p, Projection function; 13, then/if,
Converse implication In logic and mathematics, the converse of a categorical or implicational statement is the result of reversing its two constituent statements. For the implication ''P'' → ''Q'', the converse is ''Q'' → ''P''. For the categorical proposi ...
; 14, OR,
Logical disjunction In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor ...
; 15, true, Tautology. Each logic operator can be used in an assertion about variables and operations, showing a basic rule of inference. Examples: * The column-14 operator (OR), shows ''Addition rule'': when ''p''=T (the hypothesis selects the first two lines of the table), we see (at column-14) that ''p''∨''q''=T. *: We can see also that, with the same premise, another conclusions are valid: columns 12, 14 and 15 are T. * The column-8 operator (AND), shows ''Simplification rule'': when ''p''∧''q''=T (first line of the table), we see that ''p''=T. *: With this premise, we also conclude that ''q''=T, ''p''∨''q''=T, etc. as shown by columns 9–15. * The column-11 operator (IF/THEN), shows ''Modus ponens rule'': when ''p''→''q''=T and ''p''=T only one line of the truth table (the first) satisfies these two conditions. On this line, ''q'' is also true. Therefore, whenever p → q is true and p is true, q must also be true. 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.


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 \therefore), 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 p be the proposition "If it rains today", q be "We will not go on a canoe today" and let r be "We will go on a canoe trip tomorrow". Then this argument is of the form: \begin p \rightarrow q\\ q \rightarrow r\\ \therefore \overline \\ \end


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


See also

List of logic systems This article contains a list of sample Hilbert-style deductive systems for propositional logics. Classical propositional calculus systems Classical propositional calculus is the standard propositional logic. Its intended semantics is bivalen ...


References

{{DEFAULTSORT:Rules Of Inference * Mathematics-related lists Logic-related lists de:Schlussregel he:חוקי היקש