%-------------------------------------------------------------------------- % File : SET183-6 : TPTP v2.1.0. Bugfixed v2.1.0. % Domain : Set Theory % Problem : Subclass property 1 % Version : [Qua92] axioms. % English : % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic: % : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern % Source : [Quaife] % Names : SU1 [Qua92] % Status : unsatisfiable % Rating : ? v2.1.0 % Syntax : Number of clauses : 114 ( 8 non-Horn; 39 unit; 81 RR) % Number of literals : 220 ( 50 equality) % Maximal clause size : 5 ( 1 average) % Number of predicates : 11 ( 0 propositional; 1-3 arity) % Number of functors : 48 ( 14 constant; 0-3 arity) % Number of variables : 214 ( 32 singleton) % Maximal term depth : 6 ( 1 average) % Comments : Quaife proves all these problems by augmenting the axioms with % all previously proved theorems. With a few exceptions (the % problems that correspond to [BL+86] problems), the TPTP has % retained the order in which Quaife presents the problems. The % user may create an augmented version of this problem by adding % all previously proved theorems (the ones that correspond to % [BL+86] are easily identified and positioned using Quaife's % naming scheme). % : tptp2X -f tptp -t rm_equality:rstfp SET183-6.p % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax. % : v2.1.0 - Bugfix in SET004-0.ax. %-------------------------------------------------------------------------- input_clause(subclass_members,axiom, [-- subclass(X, Y), -- member(U, X), ++ member(U, Y)]). input_clause(not_subclass_members1,axiom, [++ member(not_subclass_element(X, Y), X), ++ subclass(X, Y)]). input_clause(not_subclass_members2,axiom, [-- member(not_subclass_element(X, Y), Y), ++ subclass(X, Y)]). input_clause(class_elements_are_sets,axiom, [++ subclass(X, universal_class)]). input_clause(equal_implies_subclass1,axiom, [-- equal(X, Y), ++ subclass(X, Y)]). input_clause(equal_implies_subclass2,axiom, [-- equal(X, Y), ++ subclass(Y, X)]). input_clause(subclass_implies_equal,axiom, [-- subclass(X, Y), -- subclass(Y, X), ++ equal(X, Y)]). input_clause(unordered_pair_member,axiom, [-- member(U, unordered_pair(X, Y)), ++ equal(U, X), ++ equal(U, Y)]). input_clause(unordered_pair2,axiom, [-- member(X, universal_class), ++ member(X, unordered_pair(X, Y))]). input_clause(unordered_pair3,axiom, [-- member(Y, universal_class), ++ member(Y, unordered_pair(X, Y))]). input_clause(unordered_pairs_in_universal,axiom, [++ member(unordered_pair(X, Y), universal_class)]). input_clause(singleton_set,axiom, [++ equal(unordered_pair(X, X), singleton(X))]). input_clause(ordered_pair,axiom, [++ equal(unordered_pair(singleton(X), unordered_pair(X, singleton(Y))), ordered_pair(X, Y))]). input_clause(cartesian_product1,axiom, [-- member(ordered_pair(U, V), cross_product(X, Y)), ++ member(U, X)]). input_clause(cartesian_product2,axiom, [-- member(ordered_pair(U, V), cross_product(X, Y)), ++ member(V, Y)]). input_clause(cartesian_product3,axiom, [-- member(U, X), -- member(V, Y), ++ member(ordered_pair(U, V), cross_product(X, Y))]). input_clause(cartesian_product4,axiom, [-- member(Z, cross_product(X, Y)), ++ equal(ordered_pair(first(Z), second(Z)), Z)]). input_clause(element_relation1,axiom, [++ subclass(element_relation, cross_product(universal_class, universal_class))]). input_clause(element_relation2,axiom, [-- member(ordered_pair(X, Y), element_relation), ++ member(X, Y)]). input_clause(element_relation3,axiom, [-- member(ordered_pair(X, Y), cross_product(universal_class, universal_class)), -- member(X, Y), ++ member(ordered_pair(X, Y), element_relation)]). input_clause(intersection1,axiom, [-- member(Z, intersection(X, Y)), ++ member(Z, X)]). input_clause(intersection2,axiom, [-- member(Z, intersection(X, Y)), ++ member(Z, Y)]). input_clause(intersection3,axiom, [-- member(Z, X), -- member(Z, Y), ++ member(Z, intersection(X, Y))]). input_clause(complement1,axiom, [-- member(Z, complement(X)), -- member(Z, X)]). input_clause(complement2,axiom, [-- member(Z, universal_class), ++ member(Z, complement(X)), ++ member(Z, X)]). input_clause(union,axiom, [++ equal(complement(intersection(complement(X), complement(Y))), union(X, Y))]). input_clause(difference,axiom, [++ equal(intersection(complement(intersection(X, Y)), complement(intersection(complement(X), complement(Y)))), difference(X, Y))]). input_clause(restriction1,axiom, [++ equal(intersection(Xr, cross_product(X, Y)), restrict(Xr, X, Y))]). input_clause(restriction2,axiom, [++ equal(intersection(cross_product(X, Y), Xr), restrict(Xr, X, Y))]). input_clause(domain1,axiom, [-- equal(restrict(X, singleton(Z), universal_class), null_class), -- member(Z, domain_of(X))]). input_clause(domain2,axiom, [-- member(Z, universal_class), ++ equal(restrict(X, singleton(Z), universal_class), null_class), ++ member(Z, domain_of(X))]). input_clause(rotate1,axiom, [++ subclass(rotate(X), cross_product(cross_product(universal_class, universal_class), universal_class))]). input_clause(rotate2,axiom, [-- member(ordered_pair(ordered_pair(U, V), W), rotate(X)), ++ member(ordered_pair(ordered_pair(V, W), U), X)]). input_clause(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))]). input_clause(flip1,axiom, [++ subclass(flip(X), cross_product(cross_product(universal_class, universal_class), universal_class))]). input_clause(flip2,axiom, [-- member(ordered_pair(ordered_pair(U, V), W), flip(X)), ++ member(ordered_pair(ordered_pair(V, U), W), X)]). input_clause(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))]). input_clause(inverse,axiom, [++ equal(domain_of(flip(cross_product(Y, universal_class))), inverse(Y))]). input_clause(range_of,axiom, [++ equal(domain_of(inverse(Z)), range_of(Z))]). input_clause(domain,axiom, [++ equal(first(not_subclass_element(restrict(Z, X, singleton(Y)), null_class)), domain(Z, X, Y))]). input_clause(range,axiom, [++ equal(second(not_subclass_element(restrict(Z, singleton(X), Y), null_class)), range(Z, X, Y))]). input_clause(image,axiom, [++ equal(range_of(restrict(Xr, X, universal_class)), image(Xr, X))]). input_clause(successor,axiom, [++ equal(union(X, singleton(X)), successor(X))]). input_clause(successor_relation1,axiom, [++ subclass(successor_relation, cross_product(universal_class, universal_class))]). input_clause(successor_relation2,axiom, [-- member(ordered_pair(X, Y), successor_relation), ++ equal(successor(X), Y)]). input_clause(successor_relation3,axiom, [-- equal(successor(X), Y), -- member(ordered_pair(X, Y), cross_product(universal_class, universal_class)), ++ member(ordered_pair(X, Y), successor_relation)]). input_clause(inductive1,axiom, [-- inductive(X), ++ member(null_class, X)]). input_clause(inductive2,axiom, [-- inductive(X), ++ subclass(image(successor_relation, X), X)]). input_clause(inductive3,axiom, [-- member(null_class, X), -- subclass(image(successor_relation, X), X), ++ inductive(X)]). input_clause(omega_is_inductive1,axiom, [++ inductive(omega)]). input_clause(omega_is_inductive2,axiom, [-- inductive(Y), ++ subclass(omega, Y)]). input_clause(omega_in_universal,axiom, [++ member(omega, universal_class)]). input_clause(sum_class_definition,axiom, [++ equal(domain_of(restrict(element_relation, universal_class, X)), sum_class(X))]). input_clause(sum_class2,axiom, [-- member(X, universal_class), ++ member(sum_class(X), universal_class)]). input_clause(power_class_definition,axiom, [++ equal(complement(image(element_relation, complement(X))), power_class(X))]). input_clause(power_class2,axiom, [-- member(U, universal_class), ++ member(power_class(U), universal_class)]). input_clause(compose1,axiom, [++ subclass(compose(Yr, Xr), cross_product(universal_class, universal_class))]). input_clause(compose2,axiom, [-- member(ordered_pair(Y, Z), compose(Yr, Xr)), ++ member(Z, image(Yr, image(Xr, singleton(Y))))]). input_clause(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))]). input_clause(single_valued_class1,axiom, [-- single_valued_class(X), ++ subclass(compose(X, inverse(X)), identity_relation)]). input_clause(single_valued_class2,axiom, [-- subclass(compose(X, inverse(X)), identity_relation), ++ single_valued_class(X)]). input_clause(function1,axiom, [-- function(Xf), ++ subclass(Xf, cross_product(universal_class, universal_class))]). input_clause(function2,axiom, [-- function(Xf), ++ subclass(compose(Xf, inverse(Xf)), identity_relation)]). input_clause(function3,axiom, [-- subclass(Xf, cross_product(universal_class, universal_class)), -- subclass(compose(Xf, inverse(Xf)), identity_relation), ++ function(Xf)]). input_clause(replacement,axiom, [-- function(Xf), -- member(X, universal_class), ++ member(image(Xf, X), universal_class)]). input_clause(regularity1,axiom, [++ equal(X, null_class), ++ member(regular(X), X)]). input_clause(regularity2,axiom, [++ equal(X, null_class), ++ equal(intersection(X, regular(X)), null_class)]). input_clause(apply,axiom, [++ equal(sum_class(image(Xf, singleton(Y))), apply(Xf, Y))]). input_clause(choice1,axiom, [++ function(choice)]). input_clause(choice2,axiom, [-- member(Y, universal_class), ++ equal(Y, null_class), ++ member(apply(choice, Y), Y)]). input_clause(one_to_one1,axiom, [-- one_to_one(Xf), ++ function(Xf)]). input_clause(one_to_one2,axiom, [-- one_to_one(Xf), ++ function(inverse(Xf))]). input_clause(one_to_one3,axiom, [-- function(inverse(Xf)), -- function(Xf), ++ one_to_one(Xf)]). input_clause(subset_relation,axiom, [++ equal(intersection(cross_product(universal_class, universal_class), intersection(cross_product(universal_class, universal_class), complement(compose(complement(element_relation), inverse(element_relation))))), subset_relation)]). input_clause(identity_relation,axiom, [++ equal(intersection(inverse(subset_relation), subset_relation), identity_relation)]). input_clause(diagonalisation,axiom, [++ equal(complement(domain_of(intersection(Xr, identity_relation))), diagonalise(Xr))]). input_clause(cantor_class,axiom, [++ equal(intersection(domain_of(X), diagonalise(compose(inverse(element_relation), X))), cantor(X))]). input_clause(operation1,axiom, [-- operation(Xf), ++ function(Xf)]). input_clause(operation2,axiom, [-- operation(Xf), ++ equal(cross_product(domain_of(domain_of(Xf)), domain_of(domain_of(Xf))), domain_of(Xf))]). input_clause(operation3,axiom, [-- operation(Xf), ++ subclass(range_of(Xf), domain_of(domain_of(Xf)))]). input_clause(operation4,axiom, [-- function(Xf), -- equal(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)]). input_clause(compatible1,axiom, [-- compatible(Xh, Xf1, Xf2), ++ function(Xh)]). input_clause(compatible2,axiom, [-- compatible(Xh, Xf1, Xf2), ++ equal(domain_of(domain_of(Xf1)), domain_of(Xh))]). input_clause(compatible3,axiom, [-- compatible(Xh, Xf1, Xf2), ++ subclass(range_of(Xh), domain_of(domain_of(Xf2)))]). input_clause(compatible4,axiom, [-- function(Xh), -- equal(domain_of(domain_of(Xf1)), domain_of(Xh)), -- subclass(range_of(Xh), domain_of(domain_of(Xf2))), ++ compatible(Xh, Xf1, Xf2)]). input_clause(homomorphism1,axiom, [-- homomorphism(Xh, Xf1, Xf2), ++ operation(Xf1)]). input_clause(homomorphism2,axiom, [-- homomorphism(Xh, Xf1, Xf2), ++ operation(Xf2)]). input_clause(homomorphism3,axiom, [-- homomorphism(Xh, Xf1, Xf2), ++ compatible(Xh, Xf1, Xf2)]). input_clause(homomorphism4,axiom, [-- homomorphism(Xh, Xf1, Xf2), -- member(ordered_pair(X, Y), domain_of(Xf1)), ++ equal(apply(Xf2, ordered_pair(apply(Xh, X), apply(Xh, Y))), apply(Xh, apply(Xf1, ordered_pair(X, Y))))]). input_clause(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)]). input_clause(homomorphism6,axiom, [-- operation(Xf1), -- operation(Xf2), -- compatible(Xh, Xf1, Xf2), -- equal(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)]). input_clause(compose_class_definition1,axiom, [++ subclass(compose_class(X), cross_product(universal_class, universal_class))]). input_clause(compose_class_definition2,axiom, [-- member(ordered_pair(Y, Z), compose_class(X)), ++ equal(compose(X, Y), Z)]). input_clause(compose_class_definition3,axiom, [-- member(ordered_pair(Y, Z), cross_product(universal_class, universal_class)), -- equal(compose(X, Y), Z), ++ member(ordered_pair(Y, Z), compose_class(X))]). input_clause(definition_of_composition_function1,axiom, [++ subclass(composition_function, cross_product(universal_class, cross_product(universal_class, universal_class)))]). input_clause(definition_of_composition_function2,axiom, [-- member(ordered_pair(X, ordered_pair(Y, Z)), composition_function), ++ equal(compose(X, Y), Z)]). input_clause(definition_of_composition_function3,axiom, [-- member(ordered_pair(X, Y), cross_product(universal_class, universal_class)), ++ member(ordered_pair(X, ordered_pair(Y, compose(X, Y))), composition_function)]). input_clause(definition_of_domain_relation1,axiom, [++ subclass(domain_relation, cross_product(universal_class, universal_class))]). input_clause(definition_of_domain_relation2,axiom, [-- member(ordered_pair(X, Y), domain_relation), ++ equal(domain_of(X), Y)]). input_clause(definition_of_domain_relation3,axiom, [-- member(X, universal_class), ++ member(ordered_pair(X, domain_of(X)), domain_relation)]). input_clause(single_valued_term_defn1,axiom, [++ equal(first(not_subclass_element(compose(X, inverse(X)), identity_relation)), single_valued1(X))]). input_clause(single_valued_term_defn2,axiom, [++ equal(second(not_subclass_element(compose(X, inverse(X)), identity_relation)), single_valued2(X))]). input_clause(single_valued_term_defn3,axiom, [++ equal(domain(X, image(inverse(X), singleton(single_valued1(X))), single_valued2(X)), single_valued3(X))]). input_clause(compose_can_define_singleton,axiom, [++ equal(intersection(complement(compose(element_relation, complement(identity_relation))), element_relation), singleton_relation)]). input_clause(application_function_defn1,axiom, [++ subclass(application_function, cross_product(universal_class, cross_product(universal_class, universal_class)))]). input_clause(application_function_defn2,axiom, [-- member(ordered_pair(X, ordered_pair(Y, Z)), application_function), ++ member(Y, domain_of(X))]). input_clause(application_function_defn3,axiom, [-- member(ordered_pair(X, ordered_pair(Y, Z)), application_function), ++ equal(apply(X, Y), Z)]). input_clause(application_function_defn4,axiom, [-- member(ordered_pair(X, ordered_pair(Y, Z)), cross_product(universal_class, cross_product(universal_class, universal_class))), -- member(Y, domain_of(X)), ++ member(ordered_pair(X, ordered_pair(Y, apply(X, Y))), application_function)]). input_clause(maps1,axiom, [-- maps(Xf, X, Y), ++ function(Xf)]). input_clause(maps2,axiom, [-- maps(Xf, X, Y), ++ equal(domain_of(Xf), X)]). input_clause(maps3,axiom, [-- maps(Xf, X, Y), ++ subclass(range_of(Xf), Y)]). input_clause(maps4,axiom, [-- function(Xf), -- subclass(range_of(Xf), Y), ++ maps(Xf, domain_of(Xf), Y)]). input_clause(prove_subclass_property1_1,conjecture, [++ subclass(x, y)]). input_clause(prove_subclass_property1_2,conjecture, [-- equal(intersection(x, y), x)]). %--------------------------------------------------------------------------