Gödel's God in Isabelle/HOL
Christoph Benzmueller, Bruno Woltzenlogel Paleo · 2013
A1 Either a property or its negation is positive, but not both: ∀φ[P (¬φ)↔ ¬P (φ)] A2 A property necessarily implied by a positive property is positive: ∀φ∀ψ[(P (φ) ∧ ∀x[φ(x)→ ψ(x)])→ P (ψ)] T1 Positive properties are possibly exemplified: ∀φ[P (φ)→ ♦∃xφ(x)] D1 A God-like being possesses all positive properties: G(x)↔ ∀φ[P (φ)→ φ(x)] A3 The property of being God-like is positive: P (G) C Possibly, God exists: ♦∃xG(x) A4 Positive properties are necessarily positive: ∀φ[P (φ)→ P (φ)] D2 An essence of an individual is a property possessed by it and necessarily implying any of its properties: φ ess. x↔ φ(x) ∧ ∀ψ(ψ(x)→ ∀y(φ(y)→ ψ(y))) T2 Being God-like is an essence of any God-like being: ∀x[G(x)→ G ess. x] D3 Necessary existence of an individual is the necessary exemplification of all its essences: NE (x)↔ ∀φ[φ ess. x→ ∃yφ(y)] A5 Necessary existence is a positive property: P (NE ) T3 Necessarily, God exists: ∃xG(x)