Существование Бога доказано чисто логически ещё Ансельмом Кентерберийским, а в 20-ом веке представлено в современной форме немецким логиком Куртом Гёделем. Гёдель считал это главным делом своей жизни.  В представленной Гёделем форме это доказательство можно подвергать синтаксическому и семантическому анализу, проверять непротиворечивость аксиом и определений, строить модели и вообще применять различные методы работы с доказательствами (в том числе компьютерные).Так в 2014 году доказательство Гёделя проверили на современных компьютерных программах автоматического доказательства теорем высшего порядка и ошибки не обнаружено.
Вот так записывается это доказательство: A1: {P(φ) & □ ∀ x [φ(x) → ψ(x)]} → P(ψ)
A2: P(¬φ) ↔ ¬P(φ)
D1: G(x) ↔ ∀ φ [P(φ) → φ(x)]
A3: P(G)
A4: P(φ) → □ P(φ)
D2: φ ess x ↔ ∀ ψ { ψ(x) → □ ∃ [ φ → ψ ] }
D3: E(x) ↔ φ [ φ ess x → □ ∃ x φ(x) ]
A5: P(E)
T1: P(φ) → ◊ ∃ x φ(x)
T2: ◊ ∃ x G(x)
T3: G(x) → G ess x
T4: □ ∃ x G(x)