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 <mar...@ulb.ac.be 
> <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, 

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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Reply via email to