Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Would it be inconsistent to write Modus Ponens using only implication, not entailment?

$(p \wedge (p \to q)) \to q$

The way I understand is that implication ($ \to$) is an operator that yields a new statement $p \to q$ given existing statements $p$, $q$, in the same way that $+$ is an operator that yields a number given two numerical arguments. On the other hand entailment ($ \Rightarrow$) is a relation between statements, not a new statement.

Does an inconsistency arise in interpreting MP as the statement: "p and (p implies q) implies q"? As opposed to the entailment relation?

Heyting Algebras:

I'm vaguely aware of the representation of MP in category theory. From Wikipedia entry: a Heyting algebra is a generalization of Boolean algebra, algebraically a lattice with a binary operation $p \to q$ of implication (also written exponentially as $q^p$) such that $(p \to q) \wedge p \leq q$, and $p \to q$ is the maximal element such that $r \wedge p \leq q$ then $r \leq p \to q$.

Substituting $r= p \to q$, the connection is that $p \to q$ is the "weakest proposition" for which MP is sound.

The article goes on to say that the order $\leq$ on a Heyting algebra "can be recovered from" the implication operation $\to$ for any elements $p,q$ like this: $p \leq q$ iff $a \to b = 1$, where $1$ means provably true.

What's the connection between the classical interpretation and the algebraic representation? What does "can be recovered from" mean?

share|cite|improve this question
How would you infer one statement from another? For example, given $p$ and $p \rightarrow q$ what rule(s) would you use to conclude $q$? – arjafi Jan 26 '13 at 5:45
Usually the syntactic part of a (formal) logic is made up of axioms and rules of inference. These rules allow you to conclude certain statements under the assumption of others, that is, to write proofs. Modus ponens is the perhaps most basic of these rules; for example, the Hilbert system for propositional logic has only modus ponens as a rule of inference. – arjafi Jan 26 '13 at 6:00
No inconsistency. But logic has axioms and rules of inference. Without rules of inference one can't prove much. – André Nicolas Jan 26 '13 at 6:00
$+$ is not a transformation rule, it is a function symbol. Similarly, $\to$ is a symbol. These are used, alongside other symbols, to form sentences. – André Nicolas Jan 26 '13 at 6:06
My comment was made under the assumption that the question was about formal logic, not Mathematica. – André Nicolas Jan 26 '13 at 6:13
up vote 16 down vote accepted

Suppose you are given the premisses $$(P1)\quad\quad p\quad$$ and $$(P2)\quad p \to q.$$ (It doesn't matter for what follows whether we are working here in mathematician's English, augmented with an arrow to abbreviate 'if ..., then ..' or working in a more fully formalized language.)

To derive the obvious conclusion from these two premisses we need a principle of inference, a permissive rule that says

From $A$ and $A \to B$, you can infer $B$.

Without accepting some such a rule, we can't get anywhere. If we do accept the rule, then from the we can then from our two premisses we can infer the conclusion

$$(C)\quad q.\quad$$

That displayed inference rule is of course the Modus Ponens rule.

And as was pointed out long ago, most famously by Lewis Carroll in 1895 (in his article `What the Tortoise Said to Achilles'), you can't replace the rule by a sentence or proposition such as

$$(P3) \quad (p \wedge (p \to q)) \to q.$$

to serve as a third premiss. For if we just accept this as a new premiss, we will still need a permissive rule to allow us to get anywhere, e.g. the rule

From $A$ and $A \to B$ and $(A \wedge (A \to B)) \to B$, you can infer $B$.

Can we avoid appeal to that new rule by instead accepting the proposition

$$(P4)\quad[(p \wedge (p \to q) \wedge (p \wedge (p \to q)) \to q] \to q?$$

as a new premiss. Of course not. To get to $q$ we'd need to invoke yet another rule! So we really, really, don't want to start down this regress!

For more discussion, see e.g.

Moral: we can't replace the modus ponens rule by a sentence such as $(P3)$. Of course, $(P3)$ is true, and the rule and the truth are intimately connected. But even if both are available 'modus ponens' is -- by very long tradition -- the name for the rule, not for the related true sentence.

share|cite|improve this answer
+1 for the excellent explanation. I've edited my post with more detailed information on Heyting algebras from the Wiki article will accept your answer if you can address those last couple of bits please? – alancalvitti Jan 26 '13 at 17:48
Maybe I should ask about HA's as a separate Q? – alancalvitti Jan 26 '13 at 17:59
@alancalvitti, that would be best – user58512 Jan 26 '13 at 18:29
@PeterSmith, in amWhy's answer to this Q:…, he calls the double-arrows in (1) and (2) implication. I commented on this. Is it correct usage? – alancalvitti Jan 31 '13 at 15:52
Fantastic answer. – goblin Apr 1 '14 at 12:12

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.