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 > > > 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 - 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.
