Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument

DOI10.18778/0138-0680.2020.08zbMath1461.03021arXiv1910.08955OpenAlexW3039253002MaRDI QIDQ5126209

Christoph Benzmüller, David Fuenmayor

Publication date: 15 October 2020

Published in: Bulletin of the Section of Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1910.08955

zbMATH Keywords

automated reasoninghigher-order logichigher-order modal logicontological argumentcomputational metaphysicsmodal ultrafilters

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Computational methods for problems pertaining to mathematical logic and foundations (03-08)

Uses Software

• Coq
• Nitpick
• Isabelle/HOL
• Sledgehammer
• Archive Formal Proofs
• GoedelGod

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• Types, tableaus, and Gödel's God
• Isabelle/HOL. A proof assistant for higher-order logic
• A new small emendation of Gödel's ontological proof
• Quantified multimodal logics in simple type theory
• Extending Sledgehammer with SMT solvers
• Interacting with Modal Logics in the Coq Proof Assistant
• Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument