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 in ...
, 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 noncontradic ...
): : \lnot \varphi \vdash \psi : \underline : \varphi ;''
Ex contradictione quodlibet In classical logic, intuitionistic logic and similar logical systems, the principle of explosion (, 'from falsehood, anything ollows; or ), or the principle of Pseudo-Scotus, is the law according to which any statement can be proven from a co ...
'': : \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 (not ...
: : \underline : \varphi ;
Double negation introduction 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 (not ...
: : \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 and minus signs#Plus sign, plus symbol ) is one of the four basic Operation (mathematics), operations of arithmetic, the other three being subtraction, multiplication and Division (mathematics), division. ...
(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 premise ...
: : \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 calculus, propositional logic, biconditional introductionCopi and Cohen is a Validity (logic), valid rule of inference. It allows for one to inference, infer a Logical biconditional, biconditional from two Material conditional, ...
: : \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, o ...

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 In predicate logic, universal instantiation (UI; also called universal specification or universal elimination, and sometimes confused with '' dictum de omni'') is a valid rule of inference from a truth about each member of a class of individuals ...
(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 existential ...
(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 which says that, given a formula of the form (\exists x) \phi(x), one may infer \phi(c) for a new constant symbol ''c''. Th ...
(or
Existential Elimination In predicate logic, existential instantiation (also called existential elimination)Moore and Parker is a rule of inference which says that, given a formula of the form (\exists x) \phi(x), one may infer \phi(c) for a new constant symbol ''c''. Th ...
): : \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 In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are ...

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 be ...
. ;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 ...
) (aka
no-deleting theorem In physics, the no-deleting theorem of quantum information theory is a no-go theorem which states that, in general, given two copies of some arbitrary quantum state, it is impossible to delete one of the copies. It is a time-reversed dual to the no ...
) : \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 argumen ...
, 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 In logic, converse nonimplication is a logical connective which is the negation of converse implication (equivalently, the negation of the converse of implication). Definition Converse nonimplication is notated P \nleftarrow Q, or P \not \subse ...
; 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 a ...
; 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 In Boolean functions and propositional calculus, the Sheffer stroke denotes a logical operation that is equivalent to the negation of the conjunction operation, expressed in ordinary language as "not both". It is also called nand ("not and") or ...
(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 this ...
; 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 bicondi ...
,
Logical biconditional In logic and mathematics, the logical biconditional, sometimes known as the material biconditional, is the logical connective (\leftrightarrow) used to conjoin two statements and to form the statement " if and only if ", where is known as th ...
; 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 Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically ''follows from'' one or more statements. A valid logical argument is one ...
; 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 proposit ...
; 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 S ...
; 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 bivalent ...


References

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