Re: The Cartoon Guide to Löb's Theorem
On 24 Sep 2014, at 12:00, Alberto G. Corona wrote: I still don't know what this theorem add to common sense. I mean, what it add out of his universe of formalizations in order to better formalize the obvious. It is not obvious at all. Replace p by false, and you get the incompleteness theorem: <>t -> <>[]f (if I am consistent, then it is consistent that I am inconsistent). It is a theorem in the math of self-reference. In the other side, using the curry-howard isomorphism in which for each theorem there is a program: http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html I understand the curry-howard isomorphism for intuitionist logic. For classical logic, there are different extensions of the idea, and I have not yet arrive to a definite opinion. What you describe below seems interesting, and when I have more time, I will take a look. It might not fit with my own way to see the propositions of G and G* as type. This is not an easy subbranch for me. This people found the type of a program in the haskell language that is isomorphic. The loeb formula: loeb :: Functor a => a (a x -> x) -> a x Which indeed can be used to compute spreadsheets using lazy evaluation. That is, to calculate/prove the value of a cell written as an expression that is a function of the values of other cells and so on. Compared with löb : □(□P→P)→□P in the formula 'a' means "the solution for". In this case 'a x' is a list of the values of the cells. and it tells that "if you give me a list of expressions , each one a function of the resulting values, I will return the list of resulting values. That is not uninteresting. The above expression are the types of the parameters The complete formula is: loeb :: Functor a => a (a x -> x) -> a x loeb x = fmap (\a -> a (loeb x)) x where 'fmap' is a haskell function that match with the parameter types and loeb is called recursively. The expression was found almost experimentally, without knowing well what the final result was. I created a real spreadsheet-like program using haskell running in a web browser that uses the loeb expression and it works as expected: It is interesting, senn as some attempt, and I am afraid it could take a lot of time (notably for me) to see the significance of this. Krivine (a french logician) similarly implemented the "Gödel's incompleteness theorem", seen as a type, and a program, but I am not yet well versed in that part of logic to be convinced he got the "natural" part, which in the "theological context of computationalism" the type should be motivated by self-reference and he mind-body problem. The meaning of the Curry-Howard isomorphism still eludes me in the classical logic context. It was a permanent subject of discussion with my late friend Eric Vandenbussche, he was far better than me on that. Bruno http://tryplayg.herokuapp.com/try/spreadsheet.hs/edit 2014-09-22 13:56 GMT+02:00 Telmo Menezes : http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%83%C6%92%C3%86%E2%80%99%C3%83%E2%80%A0%C3%A2%E2%82%AC%E2%84%A2%C3%83%C6%92%C3%A2%E2%82%AC%C5%A1%C3%83%E2%80%9A%C3%82%C2%B6bs_theorem/ -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout. -- Alberto. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout. http://iridia.ulb.ac.be/~marchal/ -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Re: The Cartoon Guide to Löb's Theorem
I still don't know what this theorem add to common sense. I mean, what it add out of his universe of formalizations in order to better formalize the obvious. In the other side, using the curry-howard isomorphism in which for each theorem there is a program: http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html This people found the type of a program in the haskell language that is isomorphic. The loeb formula: loeb :: Functor a => a (a x -> x) -> a x Which indeed can be used to compute spreadsheets using lazy evaluation. That is, to calculate/prove the value of a cell written as an expression that is a function of the values of other cells and so on. Compared with löb : □(□P→P)→□P in the formula 'a' means "the solution for". In this case 'a x' is a list of the values of the cells. and it tells that "if you give me a list of expressions , each one a function of the resulting values, I will return the list of resulting values. The above expression are the types of the parameters The complete formula is: loeb :: Functor a => a (a x -> x) -> a x loeb x = fmap (\a -> a (loeb x)) x where 'fmap' is a haskell function that match with the parameter types and loeb is called recursively. The expression was found almost experimentally, without knowing well what the final result was. I created a real spreadsheet-like program using haskell running in a web browser that uses the loeb expression and it works as expected: http://tryplayg.herokuapp.com/try/spreadsheet.hs/edit 2014-09-22 13:56 GMT+02:00 Telmo Menezes : > > http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%83%C6%92%C3%86%E2%80%99%C3%83%E2%80%A0%C3%A2%E2%82%AC%E2%84%A2%C3%83%C6%92%C3%A2%E2%82%AC%C5%A1%C3%83%E2%80%9A%C3%82%C2%B6bs_theorem/ > > -- > You received this message because you are subscribed to the Google Groups > "Everything List" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to everything-list+unsubscr...@googlegroups.com. > To post to this group, send email to everything-list@googlegroups.com. > Visit this group at http://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/d/optout. > -- Alberto. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Re: The Cartoon Guide to Löb's Theorem + MWI is local
On 23 Sep 2014, at 04:29, LizR wrote: That link doesn't work on Firefox, at least not for me. But it seems OK on chrome... I eventually can see it, but that was hard. It is not so bad, but frankly it helps to study it without those not se easy to read drawing. I appreciate he says "proved by PA" instead of the usual logician's "proved in PA". The first is more correct, and that plays some role in AUDA. I will certainly come back on Löbs theorem. BTW I recommend the following exercise for those who doubt that the MWI reinstates locality: translate the Bennett (and Al.) quantum teleportation experience in the MWI. It helped students to understand this locality issue. In one world such teleportation + reality criterion by Einstein entails real physical action at a distance (or improbable luck!), but it is easy to see the "trick" when seen in the many-world, where the classical bit needed by Bob to get the state of the photon sent by Alice, only inform bet on their common part of the multiverse they both belong. In particular, to send one qubit, Alice need to send 2 classical bit, and this helps Bob to figure out which branch of the universe he belongs among four branches in the multiverse. It is easier than Löb! Everything follows from the linearity of the tensor product. I use teleportation instead of Bell's inequality violation to explain that MWI makes the physical reality local, despite the appearances of non-locality in unique branche(s). This does not prove that MWI reinstates locality, but it seems to me it is enough to ask to those who claims that MWI does not reinstates locality to explain why, and to give an experiment justifying this. Where I still have some problem in the MWI is with the tunneling effect. We might need to discuss this one day. Bruno I'm sure anyone who can follow a "Doctro Who" episode written by Steven Moffat will have no trouble with that proof. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout. http://iridia.ulb.ac.be/~marchal/ -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Re: The Cartoon Guide to Löb's Theorem
That link doesn't work on Firefox, at least not for me. But it seems OK on chrome... I'm sure anyone who can follow a "Doctro Who" episode written by Steven Moffat will have no trouble with that proof. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Re: The Cartoon Guide to Löb's Theorem
(Damn you, fingers. Or even *Doctor* Who...) On 23 September 2014 14:29, LizR wrote: > That link doesn't work on Firefox, at least not for me. But it seems OK on > chrome... > > I'm sure anyone who can follow a "Doctro Who" episode written by Steven > Moffat will have no trouble with that proof. > > -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
The Cartoon Guide to Löb's Theorem
http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%83%C6%92%C3%86%E2%80%99%C3%83%E2%80%A0%C3%A2%E2%82%AC%E2%84%A2%C3%83%C6%92%C3%A2%E2%82%AC%C5%A1%C3%83%E2%80%9A%C3%82%C2%B6bs_theorem/ -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
