Re: modal logic KTB (a.k.a. B)
Le 05-mars-08, à 10:19, <[EMAIL PROTECTED]> a écrit : > > Bruno Marchal <[EMAIL PROTECTED]> wrote: >> logic B (KTB) can be used to capture a notion of vagueness, and, by a > >> theorem of Goldblatt, it can be used to formalise classicaly a > minimal >> form of von Neuman quantum logic in a manner similar to the way the >> modal logic S4, or S4Grz, capture intuitionistic logic. > > The Gödel-McKinsey-Tarski translation from intuitionistic logic to S4 > can be defined in different ways. The most concise one is by saying > that one has to insert a [] before every subformula. Can we > reformulate the translation by Goldblatt in a similar way, e.g., by > saying that one has to insert []<> before every subformula ? Hmmm I don't think so but I may be wrong. You seem to know some logic, so perhaps you could try to prove this by yourself (and then let me know :). Here is the transformation by Goldblatt, going from a propositional (non modal) language with & and ~ as connectors, to a modal language, with &, ~, and the box [] (and the usual abbreviation: <> = ~[]~, for example). T(p) = []<>p T(A & B) = T(A) & T(B) T(~A) = [] ~T(A) It is this last line, the case of the negation, which makes me think that just inserting []<> before the subformula will not work. (Actually, even if it works for Goldblatt's purpose, it can certainly not work for the arithmetical quantum logic, because the negation of a Sigma_1 universal sentence like Gödel's "bew" gives a PI_1 sentences, usually not provable by the system. > >>> Suppose the atomic propositions are what I currently know on a >>> physical system. >> >> This does not make sense. > > Really? it made some sense to me... Of course it makes sense. It makes sense for me too ... in everyday life. You should have quoted my whole paragraph which was "This does not make sense. In the way I proceed I will use the arithmetically derived points of view logics (the arithmetical hypostases) to derive the logic of observability, knowability, sensitivity ..." I was supposing that the UDA argument is already grasped, so that the only "atomic sentences" which are usable (assuming comp) correspond to the accessible states of the Universal Dovetailer (aka the Sigma_1 sentences, (with or without oracle). Your supposition was not making sense, because after UDA the term "physical system" has none of its everyday meaning. We don't even know if there is a physical system. We *know* the smell of coffee and things like that, but this refer to first person experiences. > >> Again. Just remember that I am not supposing any physics at all, nor >> any "physical world". > > My initial question was not referring to your work in particular. OK. (of course my answer was referring to it). You could ask the question explicitly to people who have diiferent views like those who believes in absolute self sampling, like Hal Finney, Nick Bostrom ... > However I would be glad to hear more from your point of view. > >> Did you grasp the UDA's point? > > No, but I am interested in and will try to catch up. Perhaps you could read my 16 may 007 post here: http://www.nabble.com/Attempt-toward-a-systematic-description- td10643945.html 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 -~--~~~~--~~--~--~---
Re: modal logic KTB (a.k.a. B)
Bruno Marchal <[EMAIL PROTECTED]> wrote: > logic B (KTB) can be used to capture a notion of vagueness, and, by a > theorem of Goldblatt, it can be used to formalise classicaly a minimal > form of von Neuman quantum logic in a manner similar to the way the > modal logic S4, or S4Grz, capture intuitionistic logic. The Gödel-McKinsey-Tarski translation from intuitionistic logic to S4 can be defined in different ways. The most concise one is by saying that one has to insert a [] before every subformula. Can we reformulate the translation by Goldblatt in a similar way, e.g., by saying that one has to insert []<> before every subformula ? > > Suppose the atomic propositions are what I currently know on a > > physical system. > > This does not make sense. Really? it made some sense to me... > Again. Just remember that I am not supposing any physics at all, nor > any "physical world". My initial question was not referring to your work in particular. However I would be glad to hear more from your point of view. > Did you grasp the UDA's point? No, but I am interested in and will try to catch up. _ Ne gardez plus qu'une seule adresse mail ! Copiez vos mails vers Yahoo! Mail http://mail.yahoo.fr --~--~-~--~~~---~--~~ 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 -~--~~~~--~~--~--~---
Re: modal logic KTB (a.k.a. B)
Le 04-mars-08, à 13:20, <[EMAIL PROTECTED]> a écrit : > >> 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 do not understand. What are the atomic propositions at each world? First order Sigma_1 arithmetical sentences (with intensional nuance driven by the modal logic itself determined by the type of points of view (1-person, 1-person plural, etc.). > Suppose the atomic propositions are what I currently know on a physical > system. This does not make sense. In the way I proceed I will use the arithmetically derived points of view logics (the arithmetical hypostases) to derive the logic of observability, knowability, sensitivity ... > Now suppose that I am in a world where I know (more or less) the > momentum of a particle. I then measure its position and thus move in > another world. It is now unlikely that the particle has the same > momentum > (due the the uncertainty principle). Again. Just remember that I am not supposing any physics at all, nor any "physical world". > Thus, if I measure again its > momentum, I might go back but I cannot be sure I will go back to the > same > previous world. It is true that I can measure again the position and > get > the same result, but it is because of reflexivity, not because of > symmetry. Why do you say this is entailed by symmetry? This might be > because you define the worlds of the frame in another way... Again, I work in the oether direction. I will try to explain you this with more details once I have more time. Note that, relatively to the UDA and its arithmetical version, you are quite above the current discussion. I think that if you grasp the UDA, you will better grasp the role of the (modal) quantum logic, and how to retrieve it from arithmetics and provability logic. Did you grasp the UDA's point? > >> I suggest you consult the Orthologic paper by Goldblatt 1974, if you > are >> interested. > > Unfortunately I have no access to this article. Can you advise me a > paper > available on internet where this idea is discussed? Unfortunately most papers bearing on this are "pre-internet". Try to google on Dalla Chiara, Goldblatt, Quantum Logic, Quantum modal logic, etc. In the worst case I can send to you a copy of some papers. The text by Maria Louisa Dalla Chiara on Quantum Logic in the handbook on philosophical logic is quite good. There exists also complementary works by Abramski. Some makes interesting relations between knot theory, Temperley Lieb Algebra, computation and combinators. In general Abramski and linear logicians (and others) despise quantum logic, but their reasons are not relevant in the context of deriving the comp-physics from comp by self-reference, as UDA shows (or is supposed to show) once we bet on the comp hypothesis. 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 -~--~~~~--~~--~--~---
Re: modal logic KTB (a.k.a. B)
> 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 do not understand. What are the atomic propositions at each world? Suppose the atomic propositions are what I currently know on a physical system. Now suppose that I am in a world where I know (more or less) the momentum of a particle. I then measure its position and thus move in another world. It is now unlikely that the particle has the same momentum (due the the uncertainty principle). Thus, if I measure again its momentum, I might go back but I cannot be sure I will go back to the same previous world. It is true that I can measure again the position and get the same result, but it is because of reflexivity, not because of symmetry. Why do you say this is entailed by symmetry? This might be because you define the worlds of the frame in another way... > I suggest you consult the Orthologic paper by Goldblatt 1974, if you are > interested. Unfortunately I have no access to this article. Can you advise me a paper available on internet where this idea is discussed? _ Ne gardez plus qu'une seule adresse mail ! Copiez vos mails vers Yahoo! Mail http://mail.yahoo.fr --~--~-~--~~~---~--~~ 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 -~--~~~~--~~--~--~---
Re: RE : Re: modal logic KTB (a.k.a. B)
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 -~--~~~
RE : Re: modal logic KTB (a.k.a. B)
Dear Bruno, Thank you for your reply. 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). I know that in the Provability Logic GL, []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". I also know that in S4, []A is to be read as "A is constructively provable": S4, which was shown by Sergei Artemov to be a forgetful projection of the Logic of Proofs LP. Could we also interpret B also in terms of some kind of provability? _ Ne gardez plus qu'une seule adresse mail ! Copiez vos mails vers Yahoo! Mail http://mail.yahoo.fr --~--~-~--~~~---~--~~ 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 -~--~~~~--~~--~--~---
Re: modal logic KTB (a.k.a .B)
Le 29-févr.-08, à 04:55, Zone a écrit : > > Does anyone know of an intuitive interpretation of the modality in the > modal logic KTB (a.k.a .B)? Do you know Kripke models and frames? A class of Kripke frames where T ( Bp -> p) and B, i.e. p -> BDp ) are valid (with B = the box, D = diamond = not box not) are the reflexive frames (each world is accessible from itself, (this is for T) and symmetrical (for B). This means B is valid in the frames where "result of experience" can be verified or repeated, and B is natural for the physical context. The logic B (KTB) can be used to capture a notion of vagueness, and, by a theorem of Goldblatt, it can be used to formalise classicaly a minimal form of von Neuman quantum logic in a manner similar to the way the modal logic S4, or S4Grz, capture intuitionistic logic. In a nutshell, a frame respects B (= makes B true in all worlds for any valuation of the propositional letters) if the accessibility relation is symmetrical (and vice versa). You can always come back to a world you have just leave. Hope this helps, 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 -~--~~~~--~~--~--~---
modal logic KTB (a.k.a .B)
Does anyone know of an intuitive interpretation of the modality in the modal logic KTB (a.k.a .B)? --~--~-~--~~~---~--~~ 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 -~--~~~~--~~--~--~---
