> On 14 Dec 2018, at 12:01, Philip Thrift <[email protected]> wrote: > > > > On Friday, December 14, 2018 at 4:49:33 AM UTC-6, Bruno Marchal wrote: > >> On 13 Dec 2018, at 21:05, Brent Meeker <[email protected] <javascript:>> >> wrote: >> >> >> >> On 12/13/2018 3:18 AM, Bruno Marchal wrote: >>>> Automating Gödel'’s Ontological Proof of God’s Existence ¨ with >>>> Higher-order Automated Theorem Provers >>>> http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf >>>> <http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf> >>> >>> Gödel took the modal logic S5 for its proof, which is the only logic NOT >>> available for the machines. >> >> What about S5 makes it not available for machines? > > > There are no intensional variant of G leading to S5. > > The axiom “5” is the guilty one (as []p & p obeys S4, and S5 can be defined > by S4 + “5”) > > “5” is <>p -> []<>p (the opposite of incompleteness: <>p -> ~[]<>p, but also > incompatible in the logic X, Z, etc.). > > Bruno > > > > > > How does this relate to the "higher-order theorem provers" that deals with > modal systems like S5? > > > https://www.ijcai.org/Proceedings/16/Papers/137.pdf
Rather interesting. The machine makes the right critics! Not quite serious about theology though. The definition of God by St-Anselme is a bit too much post-529 for the universal machine’s view. But some paragraph, notably the requirement of symmetry, gives me the feeling that the machine’s sensibility mode ([]p & <>t & p) defined in G1* (with 1 being what they called the collapse formula: p -> []p, which does not entail any collapse in arithmetic) might make the first person sensibility “believing” in the God of St-Anselme. It would be interesting to see what aspect of the ONE would correspond to this. Bruno > > - 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] > <mailto:[email protected]>. > To post to this group, send email to [email protected] > <mailto:[email protected]>. > Visit this group at https://groups.google.com/group/everything-list > <https://groups.google.com/group/everything-list>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. -- 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.
