%--------------------------------------------------------------------------
% File     : CAT004-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Category Theory
% Axioms   : Category theory axioms
% Version  : [Sco79] axioms : Reduced > Complete.
% English  :

% Refs     : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% Source   : [ANL]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :   11 (   0 non-Horn;   3 unit;   8 RR)
%            Number of atoms      :   21 (   7 equality)
%            Maximal clause size  :    3 (   2 average)
%            Number of predicates :    3 (   0 propositional; 1-2 arity)
%            Number of functors   :    3 (   0 constant; 1-2 arity)
%            Number of variables  :   19 (   2 singleton)
%            Maximal term depth   :    3 (   2 average)
% SPC      : 

% Comments : The dependent axioms have been removed.
%--------------------------------------------------------------------------
%----Non-standard in that E(x) stands for "x exists", i.e. a system -for
%----intuitionistic logic.  Viewed classically, this can be -taken
%----as a partitioning of models M into elements of E and -other elements
%----of M; then Scott's quantifiers are relativized -to range only over
%----E, whereas free variables range over all of -M.
%----Quaife has this written: (this looks really weird, but results -from
%----having = here stand for equivalence, and it is a strange -fact from
%----Scott's conception that all non-existent things are -equivalent. all
%----x all y ((x = y) | E(x) | E(y))).

%-----Restricted equality axioms
cnf(equivalence_implies_existence1,axiom,
    ( ~ equivalent(X,Y)
    | there_exists(X) )).

cnf(equivalence_implies_existence2,axiom,
    ( ~ equivalent(X,Y)
    | X = Y )).

cnf(existence_and_equality_implies_equivalence1,axiom,
    ( ~ there_exists(X)
    | X != Y
    | equivalent(X,Y) )).

%-----Category theory axioms
cnf(domain_has_elements,axiom,
    ( ~ there_exists(domain(X))
    | there_exists(X) )).

cnf(codomain_has_elements,axiom,
    ( ~ there_exists(codomain(X))
    | there_exists(X) )).

cnf(composition_implies_domain,axiom,
    ( ~ there_exists(compose(X,Y))
    | there_exists(domain(X)) )).

cnf(domain_codomain_composition1,axiom,
    ( ~ there_exists(compose(X,Y))
    | domain(X) = codomain(Y) )).

cnf(domain_codomain_composition2,axiom,
    ( ~ there_exists(domain(X))
    | domain(X) != codomain(Y)
    | there_exists(compose(X,Y)) )).

cnf(associativity_of_compose,axiom,
    ( compose(X,compose(Y,Z)) = compose(compose(X,Y),Z) )).

cnf(compose_domain,axiom,
    ( compose(X,domain(X)) = X )).

cnf(compose_codomain,axiom,
    ( compose(codomain(X),X) = X )).

%--------------------------------------------------------------------------