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