6

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?

alancalvitti
  • 3,400
  • 5
    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$? – user642796 Jan 26 '13 at 05:45
  • What do you mean by "infer"? I didn't use that term. – alancalvitti Jan 26 '13 at 05:50
  • 2
    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. – user642796 Jan 26 '13 at 06:00
  • 2
    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 06:00
  • Yes, I understand MP to be the common denominator to constructive math. However, in the link you provided, "rules of inference" are also called "transformation rules". Operators like addition ($+$) and implication ($\to$) are also transformation rules: the former yields a new number, the latter yields a new sentence. – alancalvitti Jan 26 '13 at 06:02
  • 1
    $+$ 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 06:06
  • @AndréNicolas, Type Plus[1,2] in Mathematica as input you get 3 as output. It's a binary operator $+ : \mathbb R \times \mathbb R \to \mathbb R$ (Of course in Mathematica it's variadic, not binary but that's besides the point here) – alancalvitti Jan 26 '13 at 06:07
  • 6
    My comment was made under the assumption that the question was about formal logic, not Mathematica. – André Nicolas Jan 26 '13 at 06:13
  • Are you saying MP is only relevant to formal logic and not math? My question is about trying to understand math from the point of view of formal concept analysis and universal algebra: ie, the interaction of relations and operators. – alancalvitti Jan 26 '13 at 06:16
  • It sounds as if there are two approaches being taken here. This can lead to unnecessary conflict. Let's not get off-topic into a semantic argument. – robjohn Jan 26 '13 at 08:40
  • @robjohn, not trying to spin it into a semantic argument. Lets program a computer to understand this distinction. – alancalvitti Jan 26 '13 at 15:34

1 Answers1

21

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.

Peter Smith
  • 54,743
  • 2
    +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
  • 1
    Maybe I should ask about HA's as a separate Q? – alancalvitti Jan 26 '13 at 17:59
  • @alancalvitti, that would be best –  Jan 26 '13 at 18:29
  • @PeterSmith, in amWhy's answer to this Q: http://math.stackexchange.com/questions/290646/quantifies-predicates-logical-equivalence/, 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 GONE Apr 01 '14 at 12:12