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

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

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

% Being godlike entails having all positive properties necessarily
thf(axiomC3star,definition,
    ! [X: individual] :
      ( ( godlike @ X )
     => ! [Phi: individual > $o] :
          ( ( positive @ Phi )
         => ( {$necessary} @ ( Phi @ X ) ) ) ) ).

% The individual of being godlike is positive.
thf(axiomC4,axiom,
    positive @ godlike ).

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