% A Godelian Ontological Proof with More Plausible Axiological Principles:
% Corollary 1
%
% Formalization for automated proof of Corollary 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 ).

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

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

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

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

% Something godlike exists
thf(theoremC6,conjecture,
    ? [X: individual] : ( godlike @ X ) ).