PlanetMath: modus ponens

(more info)

Math for the people, by the people.

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (194)
Orphanage
Unclass'd
Unproven (498)
Corrections (25)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

modus ponens

(Definition)

Modus ponens is a rule of inference that is commonly found in many logics where the binary logical connective $\rightarrow$ or the binary logical relation $\Rightarrow$ called logical implication are defined. Informally, it states that

and $a \Rightarrow b$ are theorems, then

is a theorem.

Modus ponens is also called the rule of detachment: the theorem can be “detached” from the theorem $a \Rightarrow b$ provided that is also a theorem.

An example of this rule is the following: From the premisses “It is raining”, and “If it rains, then my laundry will be soaked”, we may draw the conclusion “My laundry will be soaked”.

Two common ways of mathematically denoting modus ponens are the following:

$\displaystyle \frac{a,\ a \Rightarrow b}{b}$ or $\displaystyle \quad a, (a \Rightarrow b) \vdash b.$

One formal way of looking at modus ponens is to define it as a partial function $\vdash : F \times F \to F,$ where is a set of formulas in a language where a binary operation $\Rightarrow$ is defined, such that

$\vdash(x, y)$ is defined whenever $x, y \in F$ and $y \equiv (x \Rightarrow z)$ for some $z \in L$ , and
when this is the case, $z \in F$ and $\vdash(x, y) := z$ ;
$\vdash$ is not defined otherwise.

Anyone with an account can edit this entry. Please help improve it!

"modus ponens" is owned by CWoo. [ full author list (4) ]

(view preamble)

Other names:

rule of detachment, detachment, modus ponendo ponens

This object's parent.

Log in to rate this entry.
(view current ratings)

Cross-references: binary operation, language, formulas, partial function, conclusion, states, logical implication, relation, logical connective, binary, logics, rule of inference
There are 4 references to this entry.

This is version 13 of modus ponens, born on 2007-03-18, modified 2008-06-23.
Object id is 9092, canonical name is ModusPonens.
Accessed 1366 times total.

Classification:

AMS MSC:	03B35 (Mathematical logic and foundations :: General logic :: Mechanization of proofs and logical operations)
	03B05 (Mathematical logic and foundations :: General logic :: Classical propositional logic)
	03B22 (Mathematical logic and foundations :: General logic :: Abstract deductive systems)

Pending Errata and Addenda

None.

Discussion

forum policy

No messages.

Interact