On Monday, November 27, 2017 at 12:19:53 PM UTC-6, Bruno Marchal wrote: > > > On 26 Nov 2017, at 21:56, Lawrence Crowell wrote: > > and in modal logic it is □p → p. > > > No, that is the reflexion formula, typically not provable in general (for > exemple Bf -> f, with f representing the constant falsity, or "0 = 1") > expresses consitency (~Bf), which is not provable. > > Löb's theorem asserts that the machine will say Bp -> p only when she > actually prove p, which is a statement of modesty. Obviously if she proves > p, she can prove Bp -> p, because p / (q -> p) is a valid rule in classical > logic. But the machine, by Löb's theorem says the converse, if ever she > proves Bp -> p, she proves p. > > The formal modal formula is B(Bp -> p) -> Bp. >
You are right, it has been a long time since I looked at this. > > It looks also like wishful thinking. If you succeed in convincing a Löbian > entity (whose beliefs are close for the Löb rule, or having Löb's theorem > for its bewesibar predicate) that if she ever believes that some medication > will work, then it work, then she will believe the medication works! > > It solves Henkin's problem about the status of the proposition asserting > their own provability: p <-> Bp. We know with Gödel that those asserting > their own non-provability to a consistent system must be true and > unprovable by the system, that is not obvious for the Löbian sentences, as > they could a priori be false and non provable, or true and provable, but it > happens that they are always true (and provable). > > The modus tolens is ⌐p → ⌐□p (⌐ = NOT) which is not the same as p → □p. > The □ means necessarily and ⌐□⌐ means not necessarily not or possibly > abbreviated as ◊ and so ⌐p → ◊⌐p. Godel's theorem illustrates a case where > p → □p is false; > > > Indeed: ~Bf -> ~B (~Bf) (consistency implies non-provability of > consistency). > And so this is an aspect of Gödel's theorem or one way of thinking about it. I will be honest with physics and information theory I have found the computation or Turing machine approach more useful. I has been a while again since I looked at Penrose's approach to these matters. As I recall he leans heavily on the Cantor diagonalization. Turing's demonstration of no universal Turing machine and the Gödel first theorem on predicates enumerating their Gödel numbers are a form of diagonalization. What does concern me is that these mathematics involve infinite systems, and with physics we can only measure finite quantities. I has been a thought that somehow physical systems might in effect approximate Univeral TMs or Gödel's theorem in a truncated or finite manner. This might be at the intersection of P vs NP and prvability vs undecidability. I am though not versed enough in these matters to push on with it. LC > > > a proposition about an math system is true, but is not necessarily or > provably true. > > > Well the Löbian systems are completely captured by G, for the provable > statement on provability, and G* for the true statement on provability. > > G has axioms > > B(p -> q) -> (Bp -> Bq) > Bp -> BBp (redundant, follows from Löb). > B(Bp -> p) -> Bp (Löb) > > With the rule of modus ponens and necessitation a/Ba. > > G* has as axioms all theorem of G, + > Bp -> p > > But lost the necessitation rule. I let you show that G* is inconsistent if > you add the necessitation rule. > > > > If that is false then ⌐□p → ⌐p is false or ◊⌐p → ⌐p is false. We can then > only say that p being true is "possible." This seems to have some > connection with quantum measurement and the update on knowledge of a system > with prior probabilities = plausible estimates. > > I wrote a paper involving Gödel's theorem, but it was not that well > received. I will take a look at the paper on the web. I have a certain > cautionary issue with these sorts of issues. I have learned lots of > physicists take some umbrage with it. > > > Penrose has repeated old errors in the field, already well addressed in > the literature. That a great mathematician could be wrong on Gödel wary a > bit the physicists. I decided to do mathematics and mathematical logic to > masteries metamathematics, as it solved already many problem I was > interested in in biology and genetics. I can give you reference on this. > Gödel's theorem is only a first big theorem in a very rich field, and it > has important relation with computer science, and, by consequence, in the > computationalist approach of the mind-body problem. > > Bruno > > > > > LC > > ... -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
