\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{PHI001$\wedge$0.ax} Axioms for Goedel's Ontological Proof of the Existence of God






$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{god}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{god\_tp},\mbox{type})$

$\mbox{essence}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{essence\_tp},\mbox{type})$

$\mbox{necessary\_existence}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{necessary\_existence\_tp},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mequiv}@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) )@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ x )@ ( \mbox{psi}@ x ) ) ) ) )@ ( \mbox{positive}@ \mbox{psi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_2,\mbox{axiom})$

$\mbox{god} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{phi}@ x ) ) ) )\qquad\mbox{thf}(\mbox{defD}_1,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{god} )\qquad\mbox{thf}(\mbox{axA}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_4,\mbox{axiom})$

$\mbox{essence} = ( \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o},x{:}\;\mbox{mu}{:}\;( \mbox{mand}@ ( \mbox{phi}@ x )@ ( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{psi}@ x )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ y )@ ( \mbox{psi}@ y ) ) ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_2,\mbox{definition})$

$\mbox{necessary\_existence} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{essence}@ \mbox{phi}@ x )@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{phi}@ y ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_3,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{necessary\_existence} )\qquad\mbox{thf}(\mbox{axA}_5,\mbox{axiom})$

\medskip\textbf{PHI004$\wedge$1.p} Being God-like is an essence of any God-like being






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/PHI001\string^0.ax'})$

$\mbox{mvalid}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{god}@ x )@ ( \mbox{essence}@ \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{thmT}_2,\mbox{conjecture})$

\medskip\textbf{PHI005$\wedge$3.p} Necessarily, God exists

Trying to prove T3 with only K - not possible.




$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/PHI001\string^0.ax'})$

$\mbox{mvalid}@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{thmT}_3,\mbox{conjecture})$

\medskip\textbf{PHI006$\wedge$5.p} Inconsistency of the axioms in Goedel's original manuscript






$\mbox{include}(\mbox{'Axioms/LCL017\string^0.ax'})$

$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{god}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{god\_tp},\mbox{type})$

$\mbox{essence}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{essence\_tp},\mbox{type})$

$\mbox{necessary\_existence}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{necessary\_existence\_tp},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) )@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA1a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) )@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) ) ) )\qquad\mbox{thf}(\mbox{axA1b},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ x )@ ( \mbox{psi}@ x ) ) ) ) )@ ( \mbox{positive}@ \mbox{psi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_2,\mbox{axiom})$

$\mbox{essence} = ( \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o},x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{psi}@ x )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ y )@ ( \mbox{psi}@ y ) ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_2,\mbox{definition})$

$\mbox{necessary\_existence} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{essence}@ \mbox{phi}@ x )@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{phi}@ y ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_3,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{necessary\_existence} )\qquad\mbox{thf}(\mbox{axA}_5,\mbox{axiom})$

$\mbox{\$false}\qquad\mbox{thf}(\mbox{conj},\mbox{conjecture})$

\medskip\textbf{PHI008$\wedge$4.p} Modal Collapse of Goedel's ontological argument in Scott's variant






$\mbox{qML\_mu}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{qML\_i}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5U\_\_Oi},\mbox{type})$

$\mbox{scott\_G}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_OG},\mbox{type})$

$\mbox{scott\_NE\_QML\_mu}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_ONE\_001t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{scott\_P}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_OP},\mbox{type})$

$\mbox{scott\_ess\_QML\_mu}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_Oess\_001t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{scott\_G} = ( \lambda x{:}\;\mbox{qML\_mu}{:}\;\lambda w{:}\;\mbox{qML\_i}{:}\;\forall y{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}{:}\;( ( \mbox{scott\_P}@ y@ w ) \ \Rightarrow \ ( y@ x@ w ) ) )\qquad\mbox{thf}(\mbox{fact\_0\_G\_\_def},\mbox{axiom})$

\medskip\textbf{PHI001$\wedge$1.p} Axioms for Goedel's Ontological Proof of the Existence of God






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL016\string^1.ax'})$

$\mbox{include}(\mbox{'Axioms/PHI001\string^0.ax'})$

\medskip\textbf{PHI005$\wedge$1.p} Necessarily, God exists






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL016\string^1.ax'})$

$\mbox{include}(\mbox{'Axioms/PHI001\string^0.ax'})$

$\mbox{mvalid}@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{thmT}_3,\mbox{conjecture})$

\medskip\textbf{PHI003$\wedge$2.p} Possibly, God exists






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{god}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{god\_tp},\mbox{type})$

$\mbox{god} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{phi}@ x ) ) ) )\qquad\mbox{thf}(\mbox{defD}_1,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{god} )\qquad\mbox{thf}(\mbox{axA}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mdia}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{phi}@ x ) ) ) ) )\qquad\mbox{thf}(\mbox{thmT}_1,\mbox{lemma})$

$\mbox{mvalid}@ ( \mbox{mdia}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{corC},\mbox{conjecture})$

\medskip\textbf{PHI004$\wedge$4.p} Being God-like is an essence of any God-like being






$\mbox{qML\_mu}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{qML\_i}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5U\_\_Oi},\mbox{type})$

$\mbox{scott\_G}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_OG},\mbox{type})$

$\mbox{scott\_NE\_QML\_mu}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_ONE\_001t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{scott\_P}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_OP},\mbox{type})$

$\mbox{scott\_ess\_QML\_mu}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_Oess\_001t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{scott\_G} = ( \lambda x{:}\;\mbox{qML\_mu}{:}\;\lambda w{:}\;\mbox{qML\_i}{:}\;\forall y{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}{:}\;( ( \mbox{scott\_P}@ y@ w ) \ \Rightarrow \ ( y@ x@ w ) ) )\qquad\mbox{thf}(\mbox{fact\_0\_G\_\_def},\mbox{axiom})$

\medskip\textbf{PHI002$\wedge$2.p} Positive properties are possibly exemplified






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mequiv}@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) )@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ x )@ ( \mbox{psi}@ x ) ) ) ) )@ ( \mbox{positive}@ \mbox{psi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mdia}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{phi}@ x ) ) ) ) )\qquad\mbox{thf}(\mbox{thmT}_1,\mbox{conjecture})$

\medskip\textbf{PHI005$\wedge$2.p} Necessarily, God exists






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL016\string^1.ax'})$

$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{god}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{god\_tp},\mbox{type})$

$\mbox{essence}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{essence\_tp},\mbox{type})$

$\mbox{necessary\_existence}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{necessary\_existence\_tp},\mbox{type})$

$\mbox{god} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{phi}@ x ) ) ) )\qquad\mbox{thf}(\mbox{defD}_1,\mbox{definition})$

$\mbox{necessary\_existence} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{essence}@ \mbox{phi}@ x )@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{phi}@ y ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_3,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{necessary\_existence} )\qquad\mbox{thf}(\mbox{axA}_5,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mdia}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{corC},\mbox{lemma})$

$\mbox{mvalid}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{god}@ x )@ ( \mbox{essence}@ \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{thmT}_2,\mbox{lemma})$

$\mbox{mvalid}@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{thmT}_3,\mbox{conjecture})$

\medskip\textbf{PHI007$\wedge$5.p} Inconsistency of the axioms in Goedel's original manuscript

Scott's variant without the conjunct in the definition of essence.




$\mbox{qML\_mu}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{qML\_i}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5\_\_Oi},\mbox{type})$

$\mbox{inconsistency\_G}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Inconsistency\_\_S5\_OG},\mbox{type})$

$\mbox{incons1905966852QML\_mu}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Inconsistency\_\_S5\_ONE\_001t\_\_QML\_\_\_\_S5\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{inconsistency\_P}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Inconsistency\_\_S5\_OP},\mbox{type})$

$\mbox{incons1389517216QML\_mu}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Inconsistency\_\_S5\_Oess\_001t\_\_QML\_\_\_\_S5\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{qML\_r}{:}\;\mbox{qML\_i}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_QML\_\_S5\_Or},\mbox{type})$

$\forall w{:}\;\mbox{qML\_i},x{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}{:}\;( ( \mbox{inconsistency\_P}@ \lambda y{:}\;\mbox{qML\_mu}{:}\;\lambda z{:}\;\mbox{qML\_i}{:}\;\neg\,x@ y@ z@ w ) \ \Rightarrow \ \neg\,\mbox{inconsistency\_P}@ x@ w )\qquad\mbox{thf}(\mbox{fact\_0\_A1a},\mbox{axiom})$

\medskip\textbf{PHI005$\wedge$4.p} Necessarily, God exists






$\mbox{qML\_mu}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{qML\_i}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_\_QML\_\_\_\_S5U\_\_Oi},\mbox{type})$

$\mbox{scott\_G}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_OG},\mbox{type})$

$\mbox{scott\_NE\_QML\_mu}{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_ONE\_001t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{scott\_P}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_OP},\mbox{type})$

$\mbox{scott\_ess\_QML\_mu}{:}\;( \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o} )\to \mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Scott\_\_S5U\_Oess\_001t\_\_QML\_\_\_\_S5U\_\_O\_\_092\_\_060mu\_}_{062},\mbox{type})$

$\mbox{scott\_G} = ( \lambda x{:}\;\mbox{qML\_mu}{:}\;\lambda w{:}\;\mbox{qML\_i}{:}\;\forall y{:}\;\mbox{qML\_mu}\to \mbox{qML\_i}\to \mbox{\$o}{:}\;( ( \mbox{scott\_P}@ y@ w ) \ \Rightarrow \ ( y@ x@ w ) ) )\qquad\mbox{thf}(\mbox{fact\_0\_G\_\_def},\mbox{axiom})$

\medskip\textbf{PHI004$\wedge$2.p} Being God-like is an essence of any God-like being






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{god}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{god\_tp},\mbox{type})$

$\mbox{essence}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{essence\_tp},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mequiv}@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) )@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_1,\mbox{axiom})$

$\mbox{god} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{phi}@ x ) ) ) )\qquad\mbox{thf}(\mbox{defD}_1,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_4,\mbox{axiom})$

$\mbox{essence} = ( \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o},x{:}\;\mbox{mu}{:}\;( \mbox{mand}@ ( \mbox{phi}@ x )@ ( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{psi}@ x )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ y )@ ( \mbox{psi}@ y ) ) ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_2,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{god}@ x )@ ( \mbox{essence}@ \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{thmT}_2,\mbox{conjecture})$

\medskip\textbf{PHI002$\wedge$1.p} Positive properties are possibly exemplified






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/PHI001\string^0.ax'})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mdia}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{phi}@ x ) ) ) ) )\qquad\mbox{thf}(\mbox{thmT}_1,\mbox{conjecture})$

\medskip\textbf{PHI003$\wedge$1.p} Possibly, God exists






$\mbox{include}(\mbox{'Axioms/LCL016\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/PHI001\string^0.ax'})$

$\mbox{mvalid}@ ( \mbox{mdia}@ ( \mbox{mexists\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{god}@ x ) ) )\qquad\mbox{thf}(\mbox{corC},\mbox{conjecture})$

\medskip\textbf{PHI006$\wedge$4.p} Inconsistency of the axioms in Goedel's original manuscript






$\mbox{include}(\mbox{'Axioms/LCL017\string^0.ax'})$

$\mbox{positive}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{positive\_tp},\mbox{type})$

$\mbox{god}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{god\_tp},\mbox{type})$

$\mbox{essence}{:}\;( \mbox{mu}\to \mbox{\$i}\to \mbox{\$o} )\to \mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{essence\_tp},\mbox{type})$

$\mbox{necessary\_existence}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{necessary\_existence\_tp},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) )@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA1a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mnot}@ ( \mbox{positive}@ \mbox{phi} ) )@ ( \mbox{positive}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{phi}@ x ) ) ) ) )\qquad\mbox{thf}(\mbox{axA1b},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ x )@ ( \mbox{psi}@ x ) ) ) ) )@ ( \mbox{positive}@ \mbox{psi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_2,\mbox{axiom})$

$\mbox{god} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{phi}@ x ) ) ) )\qquad\mbox{thf}(\mbox{defD}_1,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{god} )\qquad\mbox{thf}(\mbox{axA}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{positive}@ \mbox{phi} )@ ( \mbox{mbox}@ ( \mbox{positive}@ \mbox{phi} ) ) ) )\qquad\mbox{thf}(\mbox{axA}_4,\mbox{axiom})$

$\mbox{essence} = ( \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o},x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{psi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{psi}@ x )@ ( \mbox{mbox}@ ( \mbox{mforall\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{phi}@ y )@ ( \mbox{psi}@ y ) ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_2,\mbox{definition})$

$\mbox{necessary\_existence} = ( \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mforall\_indset}@ \lambda \mbox{phi}{:}\;\mbox{mu}\to \mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{essence}@ \mbox{phi}@ x )@ ( \mbox{mbox}@ ( \mbox{mexists\_ind}@ \lambda y{:}\;\mbox{mu}{:}\;( \mbox{phi}@ y ) ) ) ) ) )\qquad\mbox{thf}(\mbox{defD}_3,\mbox{definition})$

$\mbox{mvalid}@ ( \mbox{positive}@ \mbox{necessary\_existence} )\qquad\mbox{thf}(\mbox{axA}_5,\mbox{axiom})$

$\mbox{\$false}\qquad\mbox{thf}(\mbox{conj},\mbox{conjecture})$

\medskip
\end{document}