Le 03-mars-08, à 12:39, <dfzone-everything.domain.name.hidden> a écrit :
> You wrote that 'B is valid in the frames where "result
> of experience" can be verified or repeated'. Can you
> be more explicit because I cannot see the relation
> with the fact that the accessibility relation is
> reflexive and symmetric (a proximity relation).
The idea is to identify an accessible world with possible results of
experiments. Symmetry then entails that if you do an experiment which
gives some result, you can repeat the experience and get those results
again. You can come back in the world you leave. It is an intuitive and
informal idea which is discussed from time to time in the literature. I
suggest you consult the Orthologic paper by Goldblatt 1974, if you are
interested.
>
> I know that in the Provability Logic GL,
(For the others: "GL" is another name of G, like GLS is another name
for G*. G = Goedel; L = Loeb, S = Solovay).
I use G like Smullyan and Boolos 1979, and like Solovay. It fits better
when the starification (G ===> G*) is seen as a sort of functor.
> []A is to be
> read as "A is provable". (I write [] for Box). "A is
> provable" does not mean that I have an explicit proof
> of A. Indeed, in the context of the first-order
> arithmetic, "A is provable" only means that "there
> exists a number which is a code of a proof of A".
Yes, it *is* the classical provABILITY predicate. It asserts that there
exist a proof, and this can sometimes been proved in a non constructive
way.
That is also why []f (provable false) can be consistent with Peano
Arithmetic. In my "theological" context, most proofs are non
constructive, like in a big part of theoretical computer science.
>
> I also know that in S4, []A is to be read as "A is
> constructively provable":
Yes. Since Goedel 1933 (ref in my thesis) we know that S4 can be used
to formalize intuitionist or constructive logic.
> S4, which was shown by
> Sergei Artemov to be a forgetful projection of the
> Logic of Proofs LP.
Yes. Unfortunately, for the reason mentionned above, I cannot use
(directly) the LP logic. But I do use "Artemov thesis" for capturing
the first person or the knower associated to a self-referentially
correct machine. That this can work has been seen by Goldblatt and
Boolos (and Kusnetzov with Muravitski). Those results have been
extended by Artemov (see the ref in my thesis). All this is directly
related to what I call the Theaetetus (in Plato) idea of defining
knowledge by true opinion. And this moves can be explained either by
the dream experience in the comp frame, or even just by thought
experiments involving dream or video-games, or virtual reality, etc.
But LP? It is not obvious how to use it in this "theological" context.
I think that constructive logic is the logic of "conventional
programming" (where you have a deadline for finishing a working
product), in opposition to "artificial intelligence" where in principle
you can (or should be able to) work without deadline, like on Platonia,
... or earth (probably: at least if we accept Darwin ...).
>
> Could we also interpret B also in terms of some kind
> of provability?
You mean the box of the B logic? What I show and use (in my thesis) is
that you can define a new predicate of provability, extensionnaly
equivalent to the Godel's beweisbar provability, which is obeying,
well, not the logic B, but the logic B weakened by disallowing the
general use of the necessitation rule (and then some other axioms which
has been isolated by a student of mine. See the Vandenbusch's notes on
my web page if you want see more). The new provability predicate
obeying B^minus (say) is given by both a intensional weakening and a
extensional strengthening of the Goedel provability predicate. You have
to define a new box [°]p by []p & <>p (or equivalently []p & <>t),
with p limited to the sigma_1 sentences. (I identify []p with its
arithmetical realization/interpretation). The UD Argument motivates why
we have to make this restriction on the sigma_1 sentences, which
captures the accessible computational states of a universal machine.
OK?
Another logic also obeys a B^minus logic: define [°°]p by []p & <>t &
p, still with p sigma_1 (or add the axiom p -> []p). Those two logics
should gives the arithmetical observability and the quasi-arithmetical
sensibility (like []p gives the provability and []p & p gives
knowability).
All that provides the arithmetical interpretation of the Plotinus
hypostases (see my Plotinus paper for more on this).
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.domain.name.hidden
To unsubscribe from this group, send email to everything-list-unsubscribe.domain.name.hidden
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Mon Mar 03 2008 - 10:32:49 PST