> On 13 Dec 2018, at 21:05, Brent Meeker <[email protected]> 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 > > Brent > > -- > 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.
