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?

## Best Answer

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

Without accepting some such a rule, we can't get anywhere. If we

doaccept the rule, then from the wecanthen from our two premisses we can infer the conclusion$$(C)\quad q.\quad$$

That displayed inference

ruleis 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

Can we avoid appeal to

thatnew 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. http://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achilles

Moral:

we can't replace the modus ponens rule by a sentence such as$(P3)$. Of course, $(P3)$ istrue, 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.