On 24 May 2012, at 09:07, Russell Standish wrote:
On Wed, May 23, 2012 at 04:41:56PM +0200, Bruno Marchal wrote:
To be sure I usually use "->" for the material implication, that is
"a -> b" is indeed "not a or b" (or "not(a and not b)").
The IF ... THEN used in math is generally of that type.
I use a => b for "from a I can derive b, in the theory I am
Actually, thinking about your thesis, I don't recall you ever once
using the symbol =>. Instead, you tend to write
I do appreciate the distinction, though!
For any theory having the modus ponens rule, we have that "a -> b"
entails (yet at another meta-level) "a => b". This should be
For many quite standard logics, the reciprocal is correct too, that
is: "a = > b" entails "a -> b". This is usually rather hard to
prove (Herbrand or deduction theorem). It is typically false in
modal logic or in many weak logics. For example the normal modal
logics (those having Kripke semantics, like G, S4, ...) are all
close for the rule a => Ba, but virtually none can prove the formula
a -> Ba. This is a source of many errors.
Simple Exercises (for those remembering Kripke semantics):
1) find a Kripke model falsifying "a -> Ba".
2) explain to yourself why "a => Ba" is always the case in all
I recall that a Kripke model is a set (of "worlds") with a binary
relation (accessibility relation). The key is that Ba is true in a
world Alpha is a is true in all worlds Beta such that (Alpha, Beta)
is in the accessibility relation.
Why is a => Ba true in Kripke models? Surely, it is possible for a to
be true, yet false in some successor world?
You are right, but this shows only that "a -> Ba" is false in the
world you are in.
But "a => Ba" is a valid rule for all logic having a Kripke semantics.
Why? Because it means that a is supposed to be valid (for example you
have already prove it), so a, like any theorem, will be true in all
worlds, so a will be in particular true in all worlds accessible from
anywhere in the model, so Ba will be true in all worlds of the model,
so Ba is also a theorem.
"->" is the implication, but "=>" concerns deduction. In fact "a =>
Ba" should not be said true, or false, only valid, or non valid. It is
a rule of inference. It means for example that from a proof of a, you
can deduce a proof of Ba. And this is correct in the Kripke model,
because a proof of a makes a true in *all* worlds (of the appropriate
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to firstname.lastname@example.org.
To unsubscribe from this group, send email to
For more options, visit this group at