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?

  • 5
    $\begingroup$ 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$? $\endgroup$
    – user642796
    Jan 26 '13 at 5:45
  • 2
    $\begingroup$ 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. $\endgroup$
    – user642796
    Jan 26 '13 at 6:00
  • 2
    $\begingroup$ No inconsistency. But logic has axioms and rules of inference. Without rules of inference one can't prove much. $\endgroup$ Jan 26 '13 at 6:00
  • 1
    $\begingroup$ $+$ is not a transformation rule, it is a function symbol. Similarly, $\to$ is a symbol. These are used, alongside other symbols, to form sentences. $\endgroup$ Jan 26 '13 at 6:06
  • 6
    $\begingroup$ My comment was made under the assumption that the question was about formal logic, not Mathematica. $\endgroup$ Jan 26 '13 at 6:13

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

  • 2
    $\begingroup$ +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? $\endgroup$ Jan 26 '13 at 17:48
  • 1
    $\begingroup$ Maybe I should ask about HA's as a separate Q? $\endgroup$ Jan 26 '13 at 17:59
  • $\begingroup$ @alancalvitti, that would be best $\endgroup$
    – user58512
    Jan 26 '13 at 18:29
  • $\begingroup$ @PeterSmith, in amWhy's answer to this Q: math.stackexchange.com/questions/290646/…, he calls the double-arrows in (1) and (2) implication. I commented on this. Is it correct usage? $\endgroup$ Jan 31 '13 at 15:52
  • $\begingroup$ Fantastic answer. $\endgroup$ Apr 1 '14 at 12:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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