% A Godelian Ontological Proof with More Plausible Axiological Principles:
% Theorem 2
%
% Formalization for automated proof of Theorem 2 in
% Johan E. Gustafsson 'A Godelian Ontological Proof with More Plausible
% Axiological Principles' Ergo 13 (20): 599-619, 2026,
% DOI: https://doi.org/10.3998/ergo.9866
%
% Author: Johan E. Gustafsson
% Date: June 30, 2026
% Web page: johanegustafsson.net

thf(semantics,logic,
    $modal == 
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_KB ] ).

thf(individual_type,type,
    individual: $tType ).

% Positvity type
thf(positive_decl,type,
    positive: ( individual > $o ) > $o ).

% Godlike type
thf(godlike_decl,type,
    godlike: individual > $o ).

% Concretely exists type
thf(exists_decl,type,
    exists: individual > $o ).

% Equivalent properties are alike in positivity
thf(axiomV1,axiom,
    ! [Phi: individual > $o,Psi: individual > $o] :
      ( ( {$necessary}
        @ ( ! [X: individual] :
              ( ( exists @ X )
             => ( ( Phi @ X )
              <=> ( Psi @ X ) ) ) ) )
     => ( ( positive @ Phi )
      <=> ( positive @ Psi ) ) ) ).

% Contradictory properties are not positive.
thf(axiomV2,axiom,
    ! [Phi: individual > $o] :
      ~ ( positive
        @ ^ [X: individual] :
            ( ( Phi @ X )
            & ~ ( Phi @ X ) ) ) ).

% Definition of being godlike as having all positive properties necessarily
thf(definitionV3,definition,
    ( godlike
    = ( ^ [X: individual] :
        ! [Phi: individual > $o] :
          ( ( positive @ Phi )
         => ( {$necessary} @ ( Phi @ X ) ) ) ) ) ).

% Definition of exists
thf(definitionE,definition,
    ( exists
    = ( ^ [X: individual] :
        ? [Y: individual] :
          ( ( exists @ Y )
          & ( X = Y ) ) ) ) ).

% The individual of being godlike is positive.
thf(axiomV4,axiom,
    ( positive
    @ ^ [X: individual] :
        ( ( godlike @ X )
        & ( exists @ X ) ) ) ).

% Necessarily something godlike exists.
thf(theoremV5,conjecture,
    ( {$necessary}
    @ ( ? [X: individual] :
          ( ( exists @ X )
          & ( godlike @ X ) ) ) ) ).