Modus ponens
Encyclopedia
In classical logic
, modus ponendo ponens (Latin
for "the way that affirms by affirming"; often abbreviated to MP or modus ponens) or implication elimination is a valid
, simple argument form. It is related to another valid form of argument, modus tollens
. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments. Both have apparently similar but invalid forms such as affirming the consequent
or denying the antecedent
and proof by contradiction or proof by contrapositive
or evidence of absence
.
Modus ponens is a very common rule of inference
, and takes the following form:
notation:
or in rule form:
or as a tautology
(plain propositional calculus sentence):
of the conditional claim, is true. From these two premises it can be logically concluded that Q, the consequent
of the conditional claim, must be true as well. In artificial intelligence
, modus ponens is often called forward chaining
.
An example of an argument that fits the form modus ponens:
This argument is valid
, but this has no bearing on whether any of the statements in the argument are true
; for modus ponens to be a sound argument, the premises must be true for any true instances of the conclusion. An argument can be valid but nonetheless unsound
if one or more premises are false; if an argument is valid and all the premises are true, then the argument is sound
. For example, John might be going to work on Wednesday. In this case, the reasoning for John's going to work (because it is Wednesday) is unsound. The argument is not only sound on Tuesdays (when John goes to work), but valid on every day of the week. A propositional argument using modus ponens is said to be deductive.
In single-conclusion sequent calculi
, modus ponens is the Cut rule. The cut-elimination theorem
for a calculus says that every proof involving Cut can be transformed (generally, by a constructive method) into a proof without Cut, and hence that Cut is admissible
.
The Curry-Howard correspondence between proofs and programs relates modus ponens to function application
: if f is a function of type P → Q and x is of type P, then f x is of type Q.
.
In instances of modus ponens we assume as premises that p → q is true and p is true. Only one line of the truth table—the first—satisfies these two conditions (p and p → q). On this line, q is also true. Therefore, whenever p → q is true and p is true, q must also be true.
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
, modus ponendo ponens (Latin
Latin
Latin is an Italic language originally spoken in Latium and Ancient Rome. It, along with most European languages, is a descendant of the ancient Proto-Indo-European language. Although it is considered a dead language, a number of scholars and members of the Christian clergy speak it fluently, and...
for "the way that affirms by affirming"; often abbreviated to MP or modus ponens) or implication elimination is a valid
Validity
In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form is valid....
, simple argument form. It is related to another valid form of argument, modus tollens
Modus tollens
In classical logic, modus tollens has the following argument form:- Formal notation :...
. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments. Both have apparently similar but invalid forms such as affirming the consequent
Affirming the consequent
Affirming the consequent, sometimes called converse error, is a formal fallacy, committed by reasoning in the form:#If P, then Q.#Q.#Therefore, P....
or denying the antecedent
Denying the antecedent
Denying the antecedent, sometimes also called inverse error, is a formal fallacy, committed by reasoning in the form:The name denying the antecedent derives from the premise "not P", which denies the "if" clause of the conditional premise....
and proof by contradiction or proof by contrapositive
Proof by contrapositive
In logic, the contrapositive of a conditional statement of the form "if A then B" is formed by negating both terms and reversing the direction of inference...
or evidence of absence
Evidence of absence
Evidence of absence is evidence of any kind that suggests the non-existence or non-presence of something. A simple example of evidence of absence: checking one's pocket for spare change and finding nothing but being confident that one would have found it if it were there...
.
Modus ponens is a very common rule of inference
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
, and takes the following form:
- If P, then Q.
- P.
- Therefore, Q.
Formal notation
The modus ponens rule may be written in sequentSequent
In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...
notation:
or in rule form:
or as a tautology
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
(plain propositional calculus sentence):
Explanation
The argument form has two premises. The first premise is the "if–then" or conditional claim, namely that P implies Q. The second premise is that P, the antecedentAntecedent (logic)
An antecedent is the first half of a hypothetical proposition.Examples:* If P, then Q.This is a nonlogical formulation of a hypothetical proposition...
of the conditional claim, is true. From these two premises it can be logically concluded that Q, the consequent
Consequent
A consequent is the second half of a hypothetical proposition. In the standard form of such a proposition, it is the part that follows "then".Examples:* If P, then Q.Q is the consequent of this hypothetical proposition....
of the conditional claim, must be true as well. In artificial intelligence
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
, modus ponens is often called forward chaining
Forward chaining
Forward chaining is one of the two main methods of reasoning when using inference rules and can be described logically as repeated application of modus ponens. Forward chaining is a popular implementation strategy for expert systems, business and production rule systems...
.
An example of an argument that fits the form modus ponens:
- If today is Tuesday, then John will go to work.
- Today is Tuesday.
- Therefore, John will go to work.
This argument is valid
Validity
In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form is valid....
, but this has no bearing on whether any of the statements in the argument are true
Truth
Truth has a variety of meanings, such as the state of being in accord with fact or reality. It can also mean having fidelity to an original or to a standard or ideal. In a common usage, it also means constancy or sincerity in action or character...
; for modus ponens to be a sound argument, the premises must be true for any true instances of the conclusion. An argument can be valid but nonetheless unsound
Soundness
In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...
if one or more premises are false; if an argument is valid and all the premises are true, then the argument is sound
Soundness
In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...
. For example, John might be going to work on Wednesday. In this case, the reasoning for John's going to work (because it is Wednesday) is unsound. The argument is not only sound on Tuesdays (when John goes to work), but valid on every day of the week. A propositional argument using modus ponens is said to be deductive.
In single-conclusion sequent calculi
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
, modus ponens is the Cut rule. The cut-elimination theorem
Cut-elimination theorem
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...
for a calculus says that every proof involving Cut can be transformed (generally, by a constructive method) into a proof without Cut, and hence that Cut is admissible
Admissible rule
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,...
.
The Curry-Howard correspondence between proofs and programs relates modus ponens to function application
Function application
In mathematics, function application is the act of applying a function to an argument from its domain so as to obtain the corresponding value from its range.-Representation:...
: if f is a function of type P → Q and x is of type P, then f x is of type Q.
Justification via truth table
The validity of modus ponens in classical two-valued logic can be clearly demonstrated by use of a truth tableTruth table
A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—to compute the functional values of logical expressions on each of their functional arguments, that is, on each combination of values taken by their...
.
| p | q | p → q |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
In instances of modus ponens we assume as premises that p → q is true and p is true. Only one line of the truth table—the first—satisfies these two conditions (p and p → q). On this line, q is also true. Therefore, whenever p → q is true and p is true, q must also be true.
See also
- Hypothetical syllogismHypothetical syllogismIn logic, a hypothetical syllogism has two uses. In propositional logic it expresses one of the rules of inference, while in the history of logic, it is a short-hand for the theory of consequence.-Propositional logic:...
- Modus tollensModus tollensIn classical logic, modus tollens has the following argument form:- Formal notation :...
- Modus tollendo ponens
- Affirming the consequentAffirming the consequentAffirming the consequent, sometimes called converse error, is a formal fallacy, committed by reasoning in the form:#If P, then Q.#Q.#Therefore, P....
- Denying the antecedentDenying the antecedentDenying the antecedent, sometimes also called inverse error, is a formal fallacy, committed by reasoning in the form:The name denying the antecedent derives from the premise "not P", which denies the "if" clause of the conditional premise....
- Disjunctive syllogismDisjunctive syllogismA disjunctive syllogism, also known as disjunction-elimination and or-elimination , and historically known as modus tollendo ponens,, is a classically valid, simple argument form:where \vdash represents the logical assertion....
- Inference rule
- What the Tortoise Said to AchillesWhat the Tortoise Said to Achilles"What the Tortoise Said to Achilles", written by Lewis Carroll in 1895 for the philosophical journal Mind, is a brief dialogue which problematises the foundations of logic. The title alludes to one of Zeno's paradoxes of motion, in which Achilles could never overtake the tortoise in a race...
External links
- Modus ponens at Wolfram MathWorld