On Thursday, November 8, 2018 at 8:36:17 AM UTC-6, John Clark wrote: > > On Wed, Nov 7, 2018 at 9:57 AM Bruno Marchal <[email protected] > <javascript:>> wrote: > > > >> *> Alan Turing used his material brain, yes, but that has nothing to do >> with the fact that he gave a definition of computation* [...] >> > > Definitions be damned! Alan Turing did not become famous because he made a > definition, anybody can do that. Alan Turing became famous by showing > how the laws of physics can produce arithmetic, and not even all the laws > are required, just the laws of classical mechanics are sufficient. And > meanwhile nobody has shown how arithmetic could produce the laws of physics > or even just mechanics. > > >>
I was thinking of how today's Theorem Provers (or Proof Assistants) - like Coq - are *the new universal machines* (in the legacy of Turing). And today there is a focus on Modal Logics (like *GL* and *GLS* - for Gödel, Löb, Solovay) This topic has been in tech news in recent years: *Automating Godel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers* - http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf - pt -- 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.
