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.


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



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 
For more options, visit this group at 

Reply via email to