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