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 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
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. 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)$ 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.