% A Godelian Ontological Proof with More Plausible Axiological Principles:
% Theorem 2 weakened by replacing (V1) with (V1*) and (V3) with (V3*)
%
% Formalization for automated proof of the weakened 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 ).

% A individual equivalent and the contradictory individual are alike in 
% positivity
thf(axiomV1star,axiom,
    ! [Phi: individual > $o] :
      ( ( {$necessary}
        @ ( ! [X: individual] :
              ( ( exists @ X )
             => ( ( Phi @ X )
              <=> ( ^ [Y: individual] :
                      ( ( Phi @ Y )
                      & ~ ( Phi @ Y ) )
                  @ X ) ) ) ) )
     => ( ( positive @ Phi )
      <=> ( positive
          @ ^ [Y: individual] :
              ( ( Phi @ Y )
              & ~ ( Phi @ Y ) ) ) ) ) ).

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

% Being godlike entails having all positive properties necessarily
thf(axiomV3star,axiom,
    ! [X: individual] :
      ( ( exists @ X )
     => ( ( godlike @ X )
       => ! [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(theoremV6,conjecture,
    ? [X: individual] :
      ( ( exists @ X )
      & ( godlike @ X ) ) ).