Le 03-mars-08, à 12:39, <[EMAIL PROTECTED]> 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 [EMAIL PROTECTED]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at 
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---

Reply via email to