%--------------------------------------------------------------------------
% File     : SET004-0 : TPTP v7.2.0. Bugfixed v2.1.0.
% Domain   : Set Theory
% Axioms   : Set theory axioms based on NBG set theory
% Version  : [Qua92] axioms.
% English  :

% Refs     : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% Source   : [Qua92]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :   91 (   8 non-Horn;  29 unit;  62 RR)
%            Number of atoms      :  181 (  39 equality)
%            Maximal clause size  :    5 (   2 average)
%            Number of predicates :   10 (   0 propositional; 1-3 arity)
%            Number of functors   :   38 (   8 constant; 0-3 arity)
%            Number of variables  :  176 (  25 singleton)
%            Maximal term depth   :    6 (   2 average)
% SPC      : 

% Comments :
% Bugfixes : v2.1.0 - Clause compatible4 fixed
%--------------------------------------------------------------------------
%----GROUP 1:          AXIOMS AND BASIC DEFINITIONS.

%----Axiom A-1:  sets are classes (omitted because all objects are
%----classes).

%----Definition of < (subclass).
%----a:x:a:y:((x < y) <=> a:u:((u e x) ==> (u e y))).
cnf(subclass_members,axiom,
    ( ~ subclass(X,Y)
    | ~ member(U,X)
    | member(U,Y) )).

cnf(not_subclass_members1,axiom,
    ( member(not_subclass_element(X,Y),X)
    | subclass(X,Y) )).

cnf(not_subclass_members2,axiom,
    ( ~ member(not_subclass_element(X,Y),Y)
    | subclass(X,Y) )).

%----Axiom A-2: elements of classes are sets.
%----a:x:(x < universal_class).
%----Singleton variables OK.
cnf(class_elements_are_sets,axiom,
    ( subclass(X,universal_class) )).

%----Axiom A-3: principle of extensionality.
%----a:x:a:y:((x = y) <=> (x < y) & (y < x)).
cnf(equal_implies_subclass1,axiom,
    ( X != Y
    | subclass(X,Y) )).

cnf(equal_implies_subclass2,axiom,
    ( X != Y
    | subclass(Y,X) )).

cnf(subclass_implies_equal,axiom,
    ( ~ subclass(X,Y)
    | ~ subclass(Y,X)
    | X = Y )).

%----Axiom A-4: existence of unordered pair.
%----a:u:a:x:a:y:((u e {x, y}) <=> (u e universal_class)
%----& (u = x | u = y)).
%----a:x:a:y:({x, y} e universal_class).
cnf(unordered_pair_member,axiom,
    ( ~ member(U,unordered_pair(X,Y))
    | U = X
    | U = Y )).

%----(x e universal_class), (u = x) --> (u e {x, y}).
%----Singleton variables OK.
cnf(unordered_pair2,axiom,
    ( ~ member(X,universal_class)
    | member(X,unordered_pair(X,Y)) )).

%----(y e universal_class), (u = y) --> (u e {x, y}).
%----Singleton variables OK.
cnf(unordered_pair3,axiom,
    ( ~ member(Y,universal_class)
    | member(Y,unordered_pair(X,Y)) )).

%----Singleton variables OK.
cnf(unordered_pairs_in_universal,axiom,
    ( member(unordered_pair(X,Y),universal_class) )).

%----Definition of singleton set.
%----a:x:({x} = {x, x}).
cnf(singleton_set,axiom,
    ( unordered_pair(X,X) = singleton(X) )).

%----See Theorem (SS6) for memb.

%----Definition of ordered pair.
%----a:x:a:y:([x,y] = {{x}, {x, {y}}}).
cnf(ordered_pair,axiom,
    ( unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y) )).

%----Axiom B-5'a: Cartesian product.
%----a:u:a:v:a:y:(([u,v] e cross_product(x,y)) <=> (u e x) & (v e y)).
%----Singleton variables OK.
cnf(cartesian_product1,axiom,
    ( ~ member(ordered_pair(U,V),cross_product(X,Y))
    | member(U,X) )).

%----Singleton variables OK.
cnf(cartesian_product2,axiom,
    ( ~ member(ordered_pair(U,V),cross_product(X,Y))
    | member(V,Y) )).

cnf(cartesian_product3,axiom,
    ( ~ member(U,X)
    | ~ member(V,Y)
    | member(ordered_pair(U,V),cross_product(X,Y)) )).

%----See Theorem (OP6) for 1st and 2nd.

%----Axiom B-5'b: Cartesian product.
%----a:z:(z e cross_product(x,y) --> ([first(z),second(z)] = z)
%----Singleton variables OK.
cnf(cartesian_product4,axiom,
    ( ~ member(Z,cross_product(X,Y))
    | ordered_pair(first(Z),second(Z)) = Z )).

%----Axiom B-1: E (element relation).
%----(E < cross_product(universal_class,universal_class)).
%----a:x:a:y:(([x,y] e E) <=> ([x,y] e cross_product(universal_class,
%----universal_class)) (x e y)).
cnf(element_relation1,axiom,
    ( subclass(element_relation,cross_product(universal_class,universal_class)) )).

cnf(element_relation2,axiom,
    ( ~ member(ordered_pair(X,Y),element_relation)
    | member(X,Y) )).

cnf(element_relation3,axiom,
    ( ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
    | ~ member(X,Y)
    | member(ordered_pair(X,Y),element_relation) )).

%----Axiom B-2: * (intersection).
%----a:z:a:x:a:y:((z e (x * y)) <=> (z e x) & (z e y)).
%----Singleton variables OK.
cnf(intersection1,axiom,
    ( ~ member(Z,intersection(X,Y))
    | member(Z,X) )).

%----Singleton variables OK.
cnf(intersection2,axiom,
    ( ~ member(Z,intersection(X,Y))
    | member(Z,Y) )).

cnf(intersection3,axiom,
    ( ~ member(Z,X)
    | ~ member(Z,Y)
    | member(Z,intersection(X,Y)) )).

%----Axiom B-3: complement.
%----a:z:a:x:((z e ~(x)) <=> (z e universal_class) & -(z e x)).
cnf(complement1,axiom,
    ( ~ member(Z,complement(X))
    | ~ member(Z,X) )).

cnf(complement2,axiom,
    ( ~ member(Z,universal_class)
    | member(Z,complement(X))
    | member(Z,X) )).

%---- Theorem (SP2) introduces the null class O.

%----Definition of + (union).
%----a:x:a:y:((x + y) = ~((~(x) * ~(y)))).
cnf(union,axiom,
    ( complement(intersection(complement(X),complement(Y))) = union(X,Y) )).

%----Definition of & (exclusive or). (= symmetric difference).
%----a:x:a:y:((x y) = (~(x * y) * ~(~(x) * ~(y)))).
cnf(symmetric_difference,axiom,
    ( intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))) = symmetric_difference(X,Y) )).

%----Definition of restriction.
%----a:x(restrict(xr,x,y) = (xr * cross_product(x,y))).
%----This is extra to the paper
cnf(restriction1,axiom,
    ( intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y) )).

cnf(restriction2,axiom,
    ( intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y) )).

%----Axiom B-4: D (domain_of).
%----a:y:a:z:((z e domain_of(x)) <=> (z e universal_class) &
%---- -(restrict(x,{z},universal_class) = O)).
%----next is subsumed by A-2.
%------> (domain_of(x) < universal_class).
cnf(domain1,axiom,
    ( restrict(X,singleton(Z),universal_class) != null_class
    | ~ member(Z,domain_of(X)) )).

cnf(domain2,axiom,
    ( ~ member(Z,universal_class)
    | restrict(X,singleton(Z),universal_class) = null_class
    | member(Z,domain_of(X)) )).

%----Axiom B-7: rotate.
%----a:x:(rotate(x) <  cross_product(cross_product(universal_class,
%----universal_class),universal_class)).
%----a:x:a:u:a:v:a:w:(([[u,v],w] e rotate(x)) <=> ([[u,v],w]]
%---- e cross_product(cross_product(universal_class,universal_class),
%----universal_class)) & ([[v,w],u]] e x).
%----Singleton variables OK.
cnf(rotate1,axiom,
    ( subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)) )).

cnf(rotate2,axiom,
    ( ~ member(ordered_pair(ordered_pair(U,V),W),rotate(X))
    | member(ordered_pair(ordered_pair(V,W),U),X) )).

cnf(rotate3,axiom,
    ( ~ member(ordered_pair(ordered_pair(V,W),U),X)
    | ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))
    | member(ordered_pair(ordered_pair(U,V),W),rotate(X)) )).

%----Axiom B-8: flip.
%----a:x:(flip(x) <  cross_product(cross_product(universal_class,
%----universal_class),universal_class)).
%----a:z:a:u:a:v:a:w:(([[u,v],w] e flip(x)) <=> ([[u,v],w]
%----e cross_product(cross_product(universal_class,universal_class),
%----universal_class)) & ([[v,u],w] e x).
%----Singleton variables OK.
cnf(flip1,axiom,
    ( subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)) )).

cnf(flip2,axiom,
    ( ~ member(ordered_pair(ordered_pair(U,V),W),flip(X))
    | member(ordered_pair(ordered_pair(V,U),W),X) )).

cnf(flip3,axiom,
    ( ~ member(ordered_pair(ordered_pair(V,U),W),X)
    | ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))
    | member(ordered_pair(ordered_pair(U,V),W),flip(X)) )).

%----Definition of inverse.
%----a:y:(inverse(y) = domain_of(flip(cross_product(y,V)))).
cnf(inverse,axiom,
    ( domain_of(flip(cross_product(Y,universal_class))) = inverse(Y) )).

%----Definition of R (range_of).
%----a:z:(range_of(z) = domain_of(inverse(z))).
cnf(range_of,axiom,
    ( domain_of(inverse(Z)) = range_of(Z) )).

%----Definition of domain.
%----a:z:a:x:a:y:(domain(z,x,y) = first(notsub(restrict(z,x,{y}),O))).
cnf(domain,axiom,
    ( first(not_subclass_element(restrict(Z,X,singleton(Y)),null_class)) = domain(Z,X,Y) )).

%----Definition of range.
%----a:z:a:x:(range(z,x,y) = second(notsub(restrict(z,{x},y),O))).
cnf(range,axiom,
    ( second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)) = range(Z,X,Y) )).

%----Definition of image.
%----a:x:a:xr:((xr image x) = range_of(restrict(xr,x,V))).
cnf(image,axiom,
    ( range_of(restrict(Xr,X,universal_class)) = image(Xr,X) )).

%----Definition of successor.
%----a:x:(successor(x) = (x + {x})).
cnf(successor,axiom,
    ( union(X,singleton(X)) = successor(X) )).

%----Explicit definition of successor_relation.
%------> ((cross_product(V,V) * ~(((E ^ ~(inverse((E + I)))) +
%----(~(E) ^ inverse((E + I)))))) = successor_relation).
%----Definition of successor_relation from the Class Existence Theorem.
%----a:x:a:y:([x,y] e successor_relation <=> x e V & successor(x) = y).
%----The above FOF does not agree with the book
cnf(successor_relation1,axiom,
    ( subclass(successor_relation,cross_product(universal_class,universal_class)) )).

cnf(successor_relation2,axiom,
    ( ~ member(ordered_pair(X,Y),successor_relation)
    | successor(X) = Y )).

%----This is what's in the book and paper. Does not change axiom.
% input_clause(successor_relation3,axiom,
%     [--equal(successor(X),Y),
%      --member(X,universal_class),
%      ++member(ordered_pair(X,Y),successor_relation)]).

%----This is what I got by email from Quaife
cnf(successor_relation3,axiom,
    ( successor(X) != Y
    | ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
    | member(ordered_pair(X,Y),successor_relation) )).

%----Definition of inductive a:x:(inductive(x) <=> null_class
%----e x & (successor_relation image x) < x)).
cnf(inductive1,axiom,
    ( ~ inductive(X)
    | member(null_class,X) )).

cnf(inductive2,axiom,
    ( ~ inductive(X)
    | subclass(image(successor_relation,X),X) )).

cnf(inductive3,axiom,
    ( ~ member(null_class,X)
    | ~ subclass(image(successor_relation,X),X)
    | inductive(X) )).

%----Axiom C-1: infinity.
%----e:x:((x e V) & inductive(x) & a:y:(inductive(y) ==> (x < y))).
%----e:x:((x e V) & (O e x) & ((successor_relation image x) < x)
%----        & a:y:((O e y) & ((successor_relation image y) < y) ==>
%----(x < y))).
cnf(omega_is_inductive1,axiom,
    ( inductive(omega) )).

cnf(omega_is_inductive2,axiom,
    ( ~ inductive(Y)
    | subclass(omega,Y) )).

cnf(omega_in_universal,axiom,
    ( member(omega,universal_class) )).

%----These were commented out in the set Quaife sent me, and are not
%----in the paper true --> (null_class e omega).
%----true --> ((successor_relation image omega) < omega).
%----(null_class e y), ((successor_relation image y) < y) -->
%----(omega < y). true --> (omega e universal_class).

%----Definition of U (sum class).
%----a:x:(sum_class(x) = domain_of(restrict(E,V,x))).
cnf(sum_class_definition,axiom,
    ( domain_of(restrict(element_relation,universal_class,X)) = sum_class(X) )).

%----Axiom C-2: U (sum class).
%----a:x:((x e V) ==> (sum_class(x) e V)).
cnf(sum_class2,axiom,
    ( ~ member(X,universal_class)
    | member(sum_class(X),universal_class) )).

%----Definition of P (power class).
%----a:x:(power_class(x) = ~((E image ~(x)))).
cnf(power_class_definition,axiom,
    ( complement(image(element_relation,complement(X))) = power_class(X) )).

%----Axiom C-3: P (power class).
%----a:u:((u e V) ==> (power_class(u) e V)).
cnf(power_class2,axiom,
    ( ~ member(U,universal_class)
    | member(power_class(U),universal_class) )).

%----Definition of compose.
%----a:xr:a:yr:((yr ^ xr) < cross_product(V,V)).
%----a:u:a:v:a:xr:a:yr:(([u,v] e (yr ^ xr)) <=> ([u,v]
%----e cross_product(V,V)) & (v e (yr image (xr image {u})))).
%----Singleton variables OK.
cnf(compose1,axiom,
    ( subclass(compose(Yr,Xr),cross_product(universal_class,universal_class)) )).

cnf(compose2,axiom,
    ( ~ member(ordered_pair(Y,Z),compose(Yr,Xr))
    | member(Z,image(Yr,image(Xr,singleton(Y)))) )).

cnf(compose3,axiom,
    ( ~ member(Z,image(Yr,image(Xr,singleton(Y))))
    | ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))
    | member(ordered_pair(Y,Z),compose(Yr,Xr)) )).

%----7/21/90 eliminate SINGVAL and just use FUNCTION.
%----Not eliminated in TPTP - I'm following the paper
cnf(single_valued_class1,axiom,
    ( ~ single_valued_class(X)
    | subclass(compose(X,inverse(X)),identity_relation) )).

cnf(single_valued_class2,axiom,
    ( ~ subclass(compose(X,inverse(X)),identity_relation)
    | single_valued_class(X) )).

%----Definition of function.
%----a:xf:(function(xf) <=> (xf < cross_product(V,V)) & ((xf
%----^ inverse(xf)) < identity_relation)).
cnf(function1,axiom,
    ( ~ function(Xf)
    | subclass(Xf,cross_product(universal_class,universal_class)) )).

cnf(function2,axiom,
    ( ~ function(Xf)
    | subclass(compose(Xf,inverse(Xf)),identity_relation) )).

cnf(function3,axiom,
    ( ~ subclass(Xf,cross_product(universal_class,universal_class))
    | ~ subclass(compose(Xf,inverse(Xf)),identity_relation)
    | function(Xf) )).

%----Axiom C-4: replacement.
%----a:x:((x e V) & function(xf) ==> ((xf image x) e V)).
cnf(replacement,axiom,
    ( ~ function(Xf)
    | ~ member(X,universal_class)
    | member(image(Xf,X),universal_class) )).

%----Axiom D: regularity.
%----a:x:(-(x = O) ==> e:u:((u e V) & (u e x) & ((u * x) = O))).
cnf(regularity1,axiom,
    ( X = null_class
    | member(regular(X),X) )).

cnf(regularity2,axiom,
    ( X = null_class
    | intersection(X,regular(X)) = null_class )).

%----Definition of apply (apply).
%----a:xf:a:y:((xf apply y) = sum_class((xf image {y}))).
cnf(apply,axiom,
    ( sum_class(image(Xf,singleton(Y))) = apply(Xf,Y) )).

%----Axiom E: universal choice.
%----e:xf:(function(xf) & a:y:((y e V) ==> (y = null_class) |
%----((xf apply y) e y))).
cnf(choice1,axiom,
    ( function(choice) )).

cnf(choice2,axiom,
    ( ~ member(Y,universal_class)
    | Y = null_class
    | member(apply(choice,Y),Y) )).

%----GROUP 2:             MORE SET THEORY DEFINITIONS.

%----Definition of one_to_one (one-to-one function).
%----a:xf:(one_to_one(xf) <=> function(xf) & function(inverse(xf))).
cnf(one_to_one1,axiom,
    ( ~ one_to_one(Xf)
    | function(Xf) )).

cnf(one_to_one2,axiom,
    ( ~ one_to_one(Xf)
    | function(inverse(Xf)) )).

cnf(one_to_one3,axiom,
    ( ~ function(inverse(Xf))
    | ~ function(Xf)
    | one_to_one(Xf) )).

%----Definition of S (subset relation).
cnf(subset_relation,axiom,
    ( intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))) = subset_relation )).

%----Definition of I (identity relation).
cnf(identity_relation,axiom,
    ( intersection(inverse(subset_relation),subset_relation) = identity_relation )).

%----Definition of diagonalization.
%----a:xr:(diagonalise(xr) = ~(domain_of((identity_relation * xr)))).
cnf(diagonalisation,axiom,
    ( complement(domain_of(intersection(Xr,identity_relation))) = diagonalise(Xr) )).

%----Definition of Cantor class.
cnf(cantor_class,axiom,
    ( intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))) = cantor(X) )).

%----Definition of operation.
%----a:xf:(operation(xf) <=> function(xf) & (cross_product(domain_of(
%----domain_of(xf)),domain_of(domain_of(xf))) = domain_of(xf))
%----& (range_of(xf) < domain_of(domain_of(xf))).
cnf(operation1,axiom,
    ( ~ operation(Xf)
    | function(Xf) )).

cnf(operation2,axiom,
    ( ~ operation(Xf)
    | cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) = domain_of(Xf) )).

cnf(operation3,axiom,
    ( ~ operation(Xf)
    | subclass(range_of(Xf),domain_of(domain_of(Xf))) )).

cnf(operation4,axiom,
    ( ~ function(Xf)
    | cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) != domain_of(Xf)
    | ~ subclass(range_of(Xf),domain_of(domain_of(Xf)))
    | operation(Xf) )).

%----Definition of compatible.
%----a:xh:a:xf1:a:af2: (compatible(xh,xf1,xf2) <=> function(xh)
%----& (domain_of(domain_of(xf1)) = domain_of(xh)) & (range_of(xh)
%----< domain_of(domain_of(xf2)))).
%----Singleton variables OK.
cnf(compatible1,axiom,
    ( ~ compatible(Xh,Xf1,Xf2)
    | function(Xh) )).

%----Singleton variables OK.
cnf(compatible2,axiom,
    ( ~ compatible(Xh,Xf1,Xf2)
    | domain_of(domain_of(Xf1)) = domain_of(Xh) )).

%----Singleton variables OK.
cnf(compatible3,axiom,
    ( ~ compatible(Xh,Xf1,Xf2)
    | subclass(range_of(Xh),domain_of(domain_of(Xf2))) )).

cnf(compatible4,axiom,
    ( ~ function(Xh)
    | domain_of(domain_of(Xf1)) != domain_of(Xh)
    | ~ subclass(range_of(Xh),domain_of(domain_of(Xf2)))
    | compatible(Xh,Xf1,Xf2) )).

%----Definition of homomorphism.
%----a:xh:a:xf1:a:xf2: (homomorphism(xh,xf1,xf2) <=>
%---- operation(xf1) & operation(xf2) & compatible(xh,xf1,xf2) &
%---- a:x:a:y:(([x,y] e domain_of(xf1)) ==> (((xf2 apply [(xh apply x),
%----(xh apply y)]) = (xh apply (xf1 apply [x,y])))).
%----Singleton variables OK.
cnf(homomorphism1,axiom,
    ( ~ homomorphism(Xh,Xf1,Xf2)
    | operation(Xf1) )).

%----Singleton variables OK.
cnf(homomorphism2,axiom,
    ( ~ homomorphism(Xh,Xf1,Xf2)
    | operation(Xf2) )).

cnf(homomorphism3,axiom,
    ( ~ homomorphism(Xh,Xf1,Xf2)
    | compatible(Xh,Xf1,Xf2) )).

cnf(homomorphism4,axiom,
    ( ~ homomorphism(Xh,Xf1,Xf2)
    | ~ member(ordered_pair(X,Y),domain_of(Xf1))
    | apply(Xf2,ordered_pair(apply(Xh,X),apply(Xh,Y))) = apply(Xh,apply(Xf1,ordered_pair(X,Y))) )).

cnf(homomorphism5,axiom,
    ( ~ operation(Xf1)
    | ~ operation(Xf2)
    | ~ compatible(Xh,Xf1,Xf2)
    | member(ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)),domain_of(Xf1))
    | homomorphism(Xh,Xf1,Xf2) )).

cnf(homomorphism6,axiom,
    ( ~ operation(Xf1)
    | ~ operation(Xf2)
    | ~ compatible(Xh,Xf1,Xf2)
    | apply(Xf2,ordered_pair(apply(Xh,not_homomorphism1(Xh,Xf1,Xf2)),apply(Xh,not_homomorphism2(Xh,Xf1,Xf2)))) != apply(Xh,apply(Xf1,ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2))))
    | homomorphism(Xh,Xf1,Xf2) )).

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