On 24 May 2012, at 19:48, meekerdb wrote:

## Advertising

On 5/24/2012 6:42 AM, Bruno Marchal wrote: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 currently considering".Actually, thinking about your thesis, I don't recall you ever once using the symbol =>. Instead, you tend to write a - b 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 trivial. 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 allclose for the rule a => Ba, but virtually none can prove theformulaa -> 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 Kripke models.Isn't "a=>Ba" trivially true since every axiom is a theorem?

"a" alone can be read as "a is true".

`If "a => Ba" was a valid rule, and reading B as provable, it would`

`mean that if a is true then a is provable. Incompleteness provide a`

`counter-example. Dt is true (for PA), but not provable (by PA).`

`So "a => Ba" is not a valid rule, and "a -> Ba" is not always a true`

`proposition (Dt -> BDt is false).`

`Note that a -> Ba is true if a is a sigma_1 proposition, and B is the`

`provability modality of any sigma_1 complete theory.`

`x -> Bx asserts a form of completeness, like Bx -> x asserts a form of`

`correctness or soundness.`

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 atobe true, yet false in some successor world?You are right, but this shows only that "a -> Ba" is false in theworld you are in.I'm confused. ~[a->Ba] means a is true but not provable (i.e. Ba isfalse) in the world you are in? Why is proof relative to the worldyou are in?

`By definition of the Kripke semantics. Truth is relativized to worlds.`

`Then, for the GĂ¶delian provability, it just happens, by Solovay`

`theorem, that it obeys a normal modal logic, (G), which means it has a`

`Kripke semantics. You can interpret a world by a model (in the sense`

`of model theory).`

it means that a is supposed to be valid (for example you havealready prove it), so a, like any theorem, will be true in allworlds, so a will be in particular true in all worlds accessiblefrom anywhere in the model, so Ba will be true in all worlds of themodel, 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. Itis a rule of inference. It means for example that from a proof ofa, you can deduce a proof of Ba.Doesn't that last sentence say Ba=>BBa?

`It does imply it, but if B is self-referential, it is equivalent with`

`Ba -> BBa.`

And this is correct in the Kripke model, because a proof of a makesa true in *all* worlds (of the appropriate Kripke structure).So Ba->a but ~[(a=>Ba)->a]?

This is meaningless, as you can't mix "=>" and "->". ~[(a=>Ba)->a] is neither a formula, nor a rule. Bruno http://iridia.ulb.ac.be/~marchal/ -- You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to everything-list@googlegroups.com. To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.