TPTP Axiom File: SET005+0.ax
%--------------------------------------------------------------------------
% File : SET005+0 : TPTP v2.6.0. Released v2.2.0.
% Domain : Set Theory
% Axioms : Set theory axioms based on NBG set theory
% Version : [Quaife, 1992] axioms : Reduced & Augmented > Complete.
% English :
% Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% Source : [Qua92]
% Names :
% Status :
% Syntax : Number of formulae : 41 ( 16 unit)
% Number of atoms : 93 ( 16 equality)
% Maximal formula depth : 6 ( 3 average)
% Number of connectives : 57 ( 5 ~ ; 3 |; 23 &)
% ( 18 <=>; 8 =>; 0 <=)
% ( 0 <~>; 0 ~|; 0 ~&)
% Number of predicates : 6 ( 0 propositional; 1-2 arity)
% Number of functors : 26 ( 5 constant; 0-3 arity)
% Number of variables : 82 ( 0 singleton; 78 !; 4 ?)
% Maximal term depth : 4 ( 1 average)
% Comments :
%--------------------------------------------------------------------------
%----Axiom A-1: Sets are classes (omitted because all objects are
%----classes).
% input_formula(sets_are_classes,axiom,
% ! [X] :
% (m(X) => cls(X))).
%----Definition of subclass. By doing this early, following axioms are
%----simplified. See A-2 for a clear example. This is what Mendelson does.
input_formula(subclass_defn,axiom,(
! [X,Y] :
( subclass(X,Y)
<=> ! [U] :
( member(U,X)
=> member(U,Y) ) ) )).
%----Axiom A-2: Elements of classes are sets.
input_formula(class_elements_are_sets,axiom,(
! [X] : subclass(X,universal_class) )).
%----Axiom A-3: Principle of extensionality. Quaife notes that this is
%----different from the Boyer version. It is the Mendelson version.
input_formula(extensionality,axiom,(
! [X,Y] :
( equal(X,Y)
<=> ( subclass(X,Y)
& subclass(Y,X) ) ) )).
%----Axiom A-4: Existence of unordered pair
input_formula(unordered_pair_defn,axiom,(
! [U,X,Y] :
( member(U,unordered_pair(X,Y))
<=> ( member(U,universal_class)
& ( equal(U,X)
| equal(U,Y) ) ) ) )).
%----Quaife says "if I were to do it again I'd use ..."
%----McCune recommends not doing this, so I havn't
% input_formula(unordered_pair1,axiom,(
% ! [U,X,Y] :
% ( member(U,unordered_pair(X,Y))
% <=> ( member(U,universal_class)
% & ( equal(U,X)
% | member(U,Y) ) ) ) )).
input_formula(unordered_pair,axiom,(
! [X,Y] : member(unordered_pair(X,Y),universal_class) )).
%----Definition of singleton set, needed for ordered pair.
input_formula(singleton_set_defn,axiom,(
! [X] : equal(singleton(X),unordered_pair(X,X)) )).
%----Definition of ordered pair, needed for B-5
input_formula(ordered_pair_defn,axiom,(
! [X,Y] : equal(ordered_pair(X,Y),unordered_pair(singleton(X),
unordered_pair(X,singleton(Y)))) )).
%----This is different from Goedel where it is
% input_formula(ordered_pair,axiom,(
% ! [X,Y] : equal(ordered_pair(X,Y),unordered_pair(singleton(X),
% unordered_pair(X,Y))) )).
%----This is motivated in Quaife's book p. 30 Section 3.5.
%----Axiom B-5: Cartesian product (not explicitly defined in Goedel)
%----Brought forward so cross_product can be used in B-1
%----In this and some other axioms, Goedel's axioms use existential
%----quantification rather than explicit definition.
input_formula(cross_product_defn,axiom,(
! [U,V,X,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
<=> ( member(U,X)
& member(V,Y) ) ) )).
input_formula(cross_product,axiom,(
! [X,Y,Z] :
( member(Z,cross_product(X,Y))
=> equal(Z,ordered_pair(first(Z),second(Z))) ) )).
%----Axiom B-1: Element relation (not explicitly defined in Goedel)
%----This is an example of undoing a simplification made by Quaife for
%----CNF systems (see book p. 28, Section 3.4).
input_formula(element_relation_defn,axiom,(
! [X,Y] :
( member(ordered_pair(X,Y),element_relation)
<=> ( member(Y,universal_class)
& member(X,Y) ) ) )).
%----Quaife's version included member(X,universal_class) in the RHS of the
%----<=>, but that's not required as member(X,Y) => member(X,universal_class)
%----The equiavlence of the two forms has been proved.
input_formula(element_relation,axiom,(
subclass(element_relation,cross_product(universal_class,
universal_class)) )).
%----Axiom B-2: Intersection (not explicitly defined in Goedel)
input_formula(intersection,axiom,(
! [X,Y,Z] :
( member(Z,intersection(X,Y))
<=> ( member(Z,X)
& member(Z,Y) ) ) )).
%----Axiom B-3: Complement (not explicitly defined in Goedel)
input_formula(complement,axiom,(
! [X,Z] :
( member(Z,complement(X))
<=> ( member(Z,universal_class)
& ~ member(Z,X) ) ) )).
%----Quaife has the definitions for union and symmetric difference in here
%----(about). I have moved union to later where it is needed. Symmetric
%----difference is not needed for Goedel's axioms, so I have moved it to
%----SET005+1.ax
%----Definition of restrict. Needed for B-4 domain_of
input_formula(restrict_defn,axiom,(
! [X,XR,Y] : equal(restrict(XR,X,Y),intersection(XR,
cross_product(X,Y))) )).
%----Definition of null_class. Needed for B-4 domain_of
%----This is dependent, but Plaisted says it's unreasonable to omit it.
input_formula(null_class_defn,axiom,(
! [X] : ~ member(X,null_class) )).
%----Axiom B-4: Domain of (not explicitly defined in Goedel)
input_formula(domain_of,axiom,(
! [X,Z] :
( member(Z,domain_of(X))
<=> ( member(Z,universal_class)
& ~ equal(restrict(X,singleton(Z),universal_class),null_class) ) ) )).
%----Axiom B-5 is earlier as it defines cross_product, used in B-1
%----Axiom B-6 is proved as a theorem
%----Axiom B-7: Existence of rotate (not explicitly defined in Goedel)
input_formula(rotate_defn,axiom,(
! [X,U,V,W] :
( member(ordered_pair(ordered_pair(U,V),W),rotate(X))
<=> ( member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(
universal_class,universal_class),universal_class))
& member(ordered_pair(ordered_pair(V,W),U),X) ) ) )).
input_formula(rotate,axiom,(
! [X] : subclass(rotate(X),cross_product(cross_product(universal_class,
universal_class),universal_class)) )).
%----Axiom B-8: Existence of flip (not explicitly defined in Goedel)
input_formula(flip_defn,axiom,(
! [U,V,W,X] :
( member(ordered_pair(ordered_pair(U,V),W),flip(X))
<=> ( member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(
universal_class,universal_class),universal_class))
& member(ordered_pair(ordered_pair(V,U),W),X) ) ) )).
input_formula(flip,axiom,(
! [X] : subclass(flip(X),cross_product(cross_product(universal_class,
universal_class),universal_class)) )).
%----I have removed the definitions of range and domain to SET005+1
%----as they are not needed for Goedel's axioms.
%----Plaisted's definition of union. Needed for successor
input_formula(union_defn,axiom,(
! [X,Y,Z] :
( member(Z,union(X,Y))
<=> ( member(Z,X)
| member(Z,Y) ) ) )).
%----This is Quaife's original definition of union, which David Plaisted
%----suggested is unnatural ...
% input_formula(union_defn_quaife,axiom,(
% ! [X,Y] : equal(union(X,Y),complement(intersection(complement(X),
% complement(Y)))) )).
%----Quaife's definition can be shown equivalent Plaisted's by showing each is
%----equivalent to this one ...
% input_formula(union_defn_geoff,axiom,(
% ! [X,Y,Z] :
% ( member(Z,union(X,Y))
% <=> member(Z,complement(intersection(complement(X),complement(Y))))) )).
%----as an intermediate
%----Definition of successor. Needed for successor_relation
input_formula(successor_defn,axiom,(
! [X] : equal(successor(X),union(X,singleton(X))) )).
%----Definition of successor_relation. Needed for inductive.
input_formula(successor_relation_defn1,axiom,(
subclass(successor_relation,cross_product(universal_class,
universal_class)) )).
%----This undoes the Quaife simplification from book p.28 Section 3.4
input_formula(successor_relation_defn2,axiom,(
! [X,Y] :
( member(ordered_pair(X,Y),successor_relation)
<=> ( member(X,universal_class)
& member(Y,universal_class)
& equal(successor(X),Y) ) ) )).
%----Definition of inverse (not explicitly defined in Goedel)
%----Needed for range_of
input_formula(inverse_defn,axiom,(
! [Y] : equal(inverse(Y),
domain_of(flip(cross_product(Y,universal_class)))) )).
%----Definition of range_of. Needed for image.
input_formula(range_of_defn,axiom,(
! [Z] : equal(range_of(Z),domain_of(inverse(Z))) )).
%----Definition of image. Needed for inductive.
input_formula(image_defn,axiom,(
! [X,XR] : equal(image(XR,X),
range_of(restrict(XR,X,universal_class))) )).
%----Definition of inductive. Needed for C-1: Infinity
input_formula(inductive_defn,axiom,(
! [X] :
( inductive(X)
<=> ( member(null_class,X)
& subclass(image(successor_relation,X),X) ) ) )).
%----Axiom C-1: Infinity
input_formula(infinity,axiom,(
? [X] :
( member(X,universal_class)
& inductive(X)
& ! [Y] :
( inductive(Y)
=> subclass(X,Y) ) ) )).
%----Axiom C-2: Sum_class (not explicitly defined in Goedel)
input_formula(sum_class_defn,axiom,(
! [U,X] :
( member(U,sum_class(X))
<=> ? [Y] :
( member(U,Y)
& member(Y,X) ) ) )).
%----Here is Quaife's original definition of sum_class, which David Plaisted
%----suggested is unnatural ...
%input_formula(sum_class_defn,axiom,(
% ! [X] : equal(sum_class(X),domain_of(restrict(element_relation,
%universal_class,X))) )).
%----Yunshan Zhu's sum class definition above has been shown equivalent to
%----the original by a longish sequence of equivalences. Boyer et al. also
%----use (a more complicated version of) the above definition.
input_formula(sum_class,axiom,(
! [X] :
( member(X,universal_class)
=> member(sum_class(X),universal_class) ) )).
%----Axiom C-3: Existence of power_class (not explicitly defined in Goedel)
input_formula(power_class_defn,axiom,(
! [U,X] :
( member(U,power_class(X))
<=> ( member(U,universal_class)
& subclass(U,X) ) ) )).
%----Here is Quaife's original definition of power_class, which David Plaisted
%----suggested is unnatural ...
%input_formula(power_class_defn,axiom,(
% ! [X] : equal(power_class(X),complement(image(element_relation,
%complement(X)))) )).
input_formula(power_class,axiom,(
! [U] :
( member(U,universal_class)
=> member(power_class(U),universal_class) ) )).
%----Definition of compose. Needed for function
input_formula(compose_defn1,axiom,(
! [XR,YR] : subclass(compose(YR,XR),cross_product(universal_class,
universal_class)) )).
%----This undoes the Quaife simplification from book p.28 Section 3.4, and
%----then simplifies that by removing a member(V,universal_class) from the RHS
input_formula(compose_defn2,axiom,(
! [XR,YR,U,V] :
( member(ordered_pair(U,V),compose(YR,XR))
<=> ( member(U,universal_class)
& member(V,image(YR,image(YR,singleton(U)))) ) ) )).
%----Definition of single_valued_class. Needed for function
%----Quaife suggests not using this, in his book p.35
%input_formula(single_valued_class_defn,axiom,(
% ! [X] :
% ( single_valued_class(X)
% <=> subclass(compose(X,inverse(X)),identity_relation) ) )).
%----Definition of function. Needed for C-4: replacement
input_formula(function_defn,axiom,(
! [XF] :
( function(XF)
<=> ( subclass(XF,cross_product(universal_class,universal_class))
& subclass(compose(XF,inverse(XF)),identity_relation) ) ) )).
%----Axiom C-4: Replacement
input_formula(replacement,axiom,(
! [X,XF] :
( ( member(X,universal_class)
& function(XF) )
=> member(image(XF,X),universal_class) ) )).
%----Definition of disjoint. This is omitted by Quaife
input_formula(disjoint_defn,axiom,(
! [X,Y] :
( disjoint(X,Y)
<=> ! [U] :
~ ( member(U,X)
& member(U,Y) ) ) )).
%----Axiom D: Regularity
input_formula(regularity,axiom,(
! [X] :
( ~ equal(X,null_class)
=> ? [U] :
( member(U,universal_class)
& member(U,X)
& disjoint(U,X) ) ) )).
%----Definition of apply. Needed for universal choice
input_formula(apply_defn,axiom,(
! [XF,Y] : equal(apply(XF,Y),sum_class(image(XF,singleton(Y)))) )).
%----Axiom E: Universal choice
input_formula(choice,axiom,(
? [XF] :
( function(XF)
& ! [Y] :
( member(Y,universal_class)
=> ( equal(Y,null_class)
| member(apply(XF,Y),Y) ) ) ) )).
%--------------------------------------------------------------------------