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.
