Modus Ponendo Ponens/Proof Rule
Proof Rule
Modus ponendo ponens is a valid argument in types of logic dealing with conditionals $\implies$.
This includes propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in the form:
- If we can conclude $\phi \implies \psi$, and we can also conclude $\phi$, then we may infer $\psi$.
Thus it provides a means of eliminating a conditional from a sequent.
It can be written:
- $\ds {\phi \qquad \phi \implies \psi \over \psi} \to_e$
Tableau Form
Let $\phi \implies \psi$ be a well-formed formula in a tableau proof whose main connective is the implication operator.
The Modus Ponendo Ponens is invoked for $\phi \implies \psi$ and $\phi$ as follows:
Pool: | The pooled assumptions of $\phi \implies \psi$ | ||||||||
The pooled assumptions of $\phi$ | |||||||||
Formula: | $\psi$ | ||||||||
Description: | Modus Ponendo Ponens | ||||||||
Depends on: | The line containing the instance of $\phi \implies \psi$ | ||||||||
The line containing the instance of $\phi$ | |||||||||
Abbreviation: | $\text{MPP}$ or $\implies \EE$ |
Also known as
Modus Ponendo Ponens is also known as:
- Modus ponens, abbreviated M.P.
- The rule of implies-elimination
- The rule of arrow-elimination
- The rule of (material) detachment
- The process of inference
Also see
- This is a rule of inference of the following proof systems:
Linguistic Note
Modus Ponendo Ponens is Latin for mode that by affirming, affirms.
The shorter form Modus Ponens means mode that affirms.
Technical Note
When invoking Modus Ponendo Ponens in a tableau proof, use the {{ModusPonens}}
template:
{{ModusPonens|line|pool|statement|first|second}}
or:
{{ModusPonens|line|pool|statement|first|second|comment}}
where:
line
is the number of the line on the tableau proof where Modus Ponendo Ponens is to be invokedpool
is the pool of assumptions (comma-separated list)statement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimitersfirst
is the first of the two lines of the tableau proof upon which this line directly depends, the one in the form $p \implies q$second
is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $p$comment
is the (optional) comment that is to be displayed in the Notes column.
Sources
- 1946: Alfred Tarski: Introduction to Logic and to the Methodology of Deductive Sciences (2nd ed.) ... (previous) ... (next): $\S \text{II}.15$: Rules of inference
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 3.9$: Derivation by Substitution
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System: $RST \, 3$
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{I}$: 'NOT' and 'IF': $\S 3$
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
- 1972: A.G. Howson: A Handbook of Terms used in Algebra and Analysis ... (previous) ... (next): $\S 1$: Some mathematical language: Axioms
- 1980: D.J. O'Connor and Betty Powell: Elementary Logic ... (previous) ... (next): $\S \text{II}$: The Logic of Statements $(2): \ 1$: Decision procedures and proofs: $1$
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.1$: Rules for natural deduction