% A Patch to the Possibility Part of Gödel’s Ontological Proof
%
% Formalization for automated proof of the theorem in
% Johan E. Gustafsson ‘A Patch to the Possibility Part of Gödel’s Ontological
% Proof’ Analysis, 80 (2): 229–240, 2020.
% Axioms for Quantified Modal Logic K.
include('Axioms/LCL016^0.ax').
% Positvity
thf(positive_type,type,(
positive: (mu > $i > $o) > $i > $o )).
% Self-difference is not positive.
thf(axiom16,axiom,
( mvalid
@ ( mnot
@ ( positive
@ ^ [X: mu,W: $i] :
(X != X) ) ) )).
% Equivalent properties are alike in positivity
thf(axiom17,axiom,
( mvalid
@ ( mforall_indset
@ ^ [Phi: mu > $i > $o] :
( mforall_indset
@ ^ [Psi: mu > $i > $o] :
( mimplies
@ ( mbox
@ ( mforall_ind
@ ^ [X: mu] :
(mequiv @ (Phi @ X) @ (Psi @ X)) ) )
@ (mequiv @ (positive @ Phi) @ (positive @ Psi)) ) ) ) )).
% The Possible Instantiation of the Positive
thf(theoremT1,conjecture,
( mvalid
@ ( mforall_indset
@ ^ [Phi: mu > $i > $o] :
( mimplies @ (positive @ Phi)
@ ( mdia
@ ( mexists_ind
@ ^ [X: mu] :
(Phi @ X) ) ) ) ) )).