### Abstract

Simplified variants of Gödel's ontological argument are explored. Among those is a particularly interesting simplified argument which is (i) valid already in basic modal logics K or KT, (ii) which does not suffer from modal collapse, and (iii) which avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel.

Whether the presented variants increase or decrease the attractiveness and persuasiveness of the ontological argument is a question I would like to pass on to philosophy and theology.

### License

BSD License

### Topics

- Logic/Philosophical aspects
- Logic/General logic/Modal logic

### Session SimplifiedOntologicalArgument

- HOML
- SimplifiedOntologicalArgument
- MFilter
- BaseDefs
- ScottVariant
- UFilterVariant
- SimpleVariant
- SimpleVariantPG
- SimpleVariantSE
- SimpleVariantSEinT
- SimpleVariantHF
- KanckosLethenNo2Possibilist

## Cite

×

SimplifiedOntologicalArgument-AFP

    @article{SimplifiedOntologicalArgument-AFP,
      author  = {Christoph Benzmüller},
      title   = {Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/SimplifiedOntologicalArgument.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 26, 2021 : Isabelle2021