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?
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?