On 27 May 2012, at 12:15, Russell Standish wrote:

On Thu, May 24, 2012 at 03:42:15PM +0200, Bruno Marchal wrote: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.I still don't follow. If I have proved a is true in some world, why should I infer that it is true in all worlds? What am I missing?

1) You might be missing the soundness theorem, perhaps.

`I give an example with classical propositional logic. Suppose that you`

`prove some formula, like (p & q)->q, then automatically the formula is`

`true in all propositional worlds (which are given by the valuation of`

`the atomic propositions).`

`Indeed you can verify that (p & q)->q is true in the four type of`

`possible worlds (those with p true and q true, p true and q false, p`

`false and q true, and p false and q false).`

`That is related to the idea that a valid proof does not depend on the`

`world, or interpretations, or contexts, etc. So if you prove something`

`it has to be true in all world, and that is why logicians favor`

`theories having a semantics such that they can prove a soundness`

`theorem. Of course they are even more happy when they have a theory`

`with a completeness theorem, which provides the opposite: all`

`proposition true in all interpretations (model, worlds, ...) can be`

`proved in the theory. This is the case for all first order theory. So`

`RA, PA, ZF are complete in that sense. M proves p iff p is true in all`

`models (interpretation, worlds) of p. Of course they are incomplete in`

`the "incompleteness" sense. Gödel proved the completeness theory PA,`

`and actually of all first order theories (in his PhD thesis, 1930),`

`and the incompleteness of PA (actually of PM, 1931).`

`So completeness in "completeness theorem and incompleteness theorem",`

`is used in different sense:`

`Keep in mind that the completeness theorem asserts that if M proves p,`

`then p is true in all models of M.`

OK?

`2) You might perhaps also be missing, or not taking into account`

`consciously enough, Kripke semantics. In that case we have the same`

`language as propositional calculus, + the unary connector or operator B.`

`Unlike ~p, whose truth value depends only of the value of p, Bp value`

`is not functionally dependent of the truth value of p.`

`Now, a modal logic theory which has the formula K (for Kripke) B(p->q)-`

`>(Bp->Bp), and whose set of theorems is closed for the modus ponens`

`rule (a, a->b) / b, but also the necessitation rule (p / Bp), can be`

`given a so called Kripke semantics (due indeed to Kripke, around 1968,`

`I think). [I write (p/BP) instead of p => Bp, to avoid confusion with`

`"->"].`

`In that semantics, you have a referential (any set with a binary`

`relation). The elements of the set are called world and designate by`

`greek letters, and the relation is called accessibility relation,`

`often designated by R, and if (alpha, beta) belongs to R, we write as`

`usual "alpha R beta".`

`That referential becomes a model when, on each world, you give a`

`valuation on the atomic sentences p, q, r, ... and you extend, as in`

`propositional logic the value of the compound formula. All worlds`

`"obeys" classical propositional logic, so to speak. If a is true in`

`alpha, and if b is true in alpha, we will have (a & b) is true in alpha.`

`But this will not provide a valuation for Bp, as Bp does not truth-`

`functionally depend on the value of p.`

`Kripke defined the truth of Bp in the world alpha, by the truth of p`

`in all the worlds accessible from alpha.`

`Bp is true is everywhere I will find myself, p is true. It is natural`

`with most known modalities (where Bp/Dp ([ ]/<>), with Dp = ~B~p,`

`corresponds to Necessity/Possibility, Obligation/Permission,`

`Everywhere/Somewhere, Always/Once, For-all/It-exists, etc.).`

`If Bp means that p is true in all worlds accessible from the world I`

`am in, Dp meaning ~B~p, will mean that it is false that ~p is true in`

`all worlds accessible, and thus that there is a world where p is true.`

`So, Dp is true in alpha if it exists a world beta with p true in beta`

`and (alpha R beta).`

`So here, like provability above, "Bp" is related to true in all`

`(accessible) worlds.`

Then you have the completeness theorem for many modal logic.

`K4 proves A iff A is true in all models with R transitive (4 = Bp ->`

`BBp)`

KTproves A iff A is true in all models with R réflexive (T = Bp -> p)

`KTB proves A iff A is true in all models with R réflexive and`

`symmetrical`

and

`G proves A iff A is true in all finite models with R irreflexive and`

`realist (realist means that all transitory world accesses to cul-de-`

`sac, and a world is transitory if it is a not a cul-de-sac, and of`

`course a cul-de-sac world is a world alpha such that there are no beta`

`such that alpha R beta.`

`3) A relation between modal logic and provability by PA (or any Lobian`

`machine) has been made more precise by Solovay theorem.`

`Provability (of a rich (Löbian)) machine or axiomatizable theory, like`

`PA to fix the thing, obeys a modal logic, indeed G, in the following`

`sense:`

We map the modal logic language on arithmetic, by

`1) mapping the atomic sentence letters p, q, r, by arithmetical`

`proposition (p = "1+1=2", q = "Fermat theorem", etc.)`

`That basic low level mapping is called the realization (for using it`

`below). In AUDA, comp and the UD is modeled later by restricting this`

`mapping to the sigma-1 arithmetical propositions.`

`2) extending this realization to the more complex boolean formula in`

`the obvious sense (p&q will be mapped on "1+1=2 & Fermat theorem", for`

`example, ... of course written with only "s" and "0" and "+" and "*"`

`and the logical symbols.`

`3) extending this to Bp by mapping it on Beweisbar('p'), that is Gödel`

`*arithmetical* provability predicate, and 'p' being the Gödel number`

`encoding of p.`

`And we can do this for any modal logic, of course, but if we do this`

`to the modal logic G and G*, we have the two theorems of Solovay (1976):`

`G prove A iff for all realisations of the atomic formula, PA proves`

`m(A), with m(A) the mapping described above.`

And the "cerise sur le gateau":

`G* prove A iff for all realisations of the atomic formula, m(A) is`

`true, again with m(A) the mapping described above.`

`So G axiomatizes what Löbian machine can prove about their provability`

`ability, and G* axiomatizes the truth about them, being provable or`

`unprovable by the machine.`

`Is this a reason to identify the models of PA with the Kripke worlds?`

`Not really. But there are relations which are interesting, but`

`technically long to be described.`

`Note that at the modal propositional level G and G* are decidable,`

`making obvious that a self-observing/inferring machine can produce`

`many truth about herself despite not being able to prove them. Ideally`

`correct self-observing/inferring machine get mystical, in that sense.`

`Unavoidably.`

`The gap between proof and truth, for machine, gives sense to the`

`Theaetetus definition of the knower, thanks to`

(Bp <-> Bp & p) belongs to G* minus G. True but not provable.

`If you map Bp, no more on Beweisbar('p'), but on (Beweisbar('p') & p),`

`you get a knower associated to the machine. It is a knower, in the`

`sense that it obeys to the classical logic S4. Indeed it obeys to the`

`system S4Grz. And the machine cannot give any description of that`

`knower, so that it verifies well the "mystic theory of knowledge" (by`

`Brouwer, notably, but also Plotinus and Plato).`

Oops... I might have been a bit long, sorry. It sums a bit AUDA. 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.