#-------------------------------------------------------------------------- # File : NUM094-1 : TPTP v2.1.0. Bugfixed v2.1.0. # Domain : Number Theory (Ordinals) # Problem : Sections property 3 # Version : [Qua92] axioms. # English : # Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern # Source : [Quaife] # Names : SE3.1 [Quaife] # Status : unknown # Rating : ? v2.1.0 # Syntax : Number of clauses : 162 ( 12 non-Horn; 50 unit; 123 RR) # Number of literals : 326 ( 72 equality) # Maximal clause size : 5 ( 2 average) # Number of predicates : 17 ( 0 propositional; 1-3 arity) # Number of functors : 65 ( 21 constant; 0-3 arity) # Number of variables : 303 ( 40 singleton) # Maximal term depth : 6 ( 1 average) # Comments : Not in [Qua92]. Theorem SE3.1 in [Quaife]. # : Quaife proves all these problems by augmenting the axioms with # all previously proved theorems. The user may create an augmented # version of this problem by adding all previously proved theorems. # These include all of [Qua92]'s set theory and Boolean algebra # theorems, available from the SET domain. # : tptp2X -f setheo:sign -t rm_equality:rstfp NUM094-1.p # Bugfixes : v1.0.1 - Bugfix in SET004-1.ax. # : v2.1.0 - Bugfix in SET004-0.ax. #-------------------------------------------------------------------------- # subclass_members, axiom. member(U, Y) <- subclass(X, Y), member(U, X). # not_subclass_members1, axiom. member(not_subclass_element(X, Y), X); subclass(X, Y) <- . # not_subclass_members2, axiom. subclass(X, Y) <- member(not_subclass_element(X, Y), Y). # class_elements_are_sets, axiom. subclass(X, universal_class) <- . # equal_implies_subclass1, axiom. subclass(X, Y) <- equal(X, Y). # equal_implies_subclass2, axiom. subclass(Y, X) <- equal(X, Y). # subclass_implies_equal, axiom. equal(X, Y) <- subclass(X, Y), subclass(Y, X). # unordered_pair_member, axiom. equal(U, X); equal(U, Y) <- member(U, unordered_pair(X, Y)). # unordered_pair2, axiom. member(X, unordered_pair(X, Y)) <- member(X, universal_class). # unordered_pair3, axiom. member(Y, unordered_pair(X, Y)) <- member(Y, universal_class). # unordered_pairs_in_universal, axiom. member(unordered_pair(X, Y), universal_class) <- . # singleton_set, axiom. equal(unordered_pair(X, X), singleton(X)) <- . # ordered_pair, axiom. equal(unordered_pair(singleton(X), unordered_pair(X, singleton(Y))), ordered_pair(X, Y)) <- . # cartesian_product1, axiom. member(U, X) <- member(ordered_pair(U, V), cross_product(X, Y)). # cartesian_product2, axiom. member(V, Y) <- member(ordered_pair(U, V), cross_product(X, Y)). # cartesian_product3, axiom. member(ordered_pair(U, V), cross_product(X, Y)) <- member(U, X), member(V, Y). # cartesian_product4, axiom. equal(ordered_pair(first(Z), second(Z)), Z) <- member(Z, cross_product(X, Y)). # element_relation1, axiom. subclass(element_relation, cross_product(universal_class, universal_class)) <- . # element_relation2, axiom. member(X, Y) <- member(ordered_pair(X, Y), element_relation). # element_relation3, axiom. member(ordered_pair(X, Y), element_relation) <- member(ordered_pair(X, Y), cross_product(universal_class, universal_class)), member(X, Y). # intersection1, axiom. member(Z, X) <- member(Z, intersection(X, Y)). # intersection2, axiom. member(Z, Y) <- member(Z, intersection(X, Y)). # intersection3, axiom. member(Z, intersection(X, Y)) <- member(Z, X), member(Z, Y). # complement1, axiom. <- member(Z, complement(X)), member(Z, X). # complement2, axiom. member(Z, complement(X)); member(Z, X) <- member(Z, universal_class). # union, axiom. equal(complement(intersection(complement(X), complement(Y))), union(X, Y)) <- . # difference, axiom. equal(intersection(complement(intersection(X, Y)), complement(intersection(complement(X), complement(Y)))), difference(X, Y)) <- . # restriction1, axiom. equal(intersection(Xr, cross_product(X, Y)), restrict(Xr, X, Y)) <- . # restriction2, axiom. equal(intersection(cross_product(X, Y), Xr), restrict(Xr, X, Y)) <- . # domain1, axiom. <- equal(restrict(X, singleton(Z), universal_class), null_class), member(Z, domain_of(X)). # domain2, axiom. equal(restrict(X, singleton(Z), universal_class), null_class); member(Z, domain_of(X)) <- member(Z, universal_class). # rotate1, axiom. subclass(rotate(X), cross_product(cross_product(universal_class, universal_class), universal_class)) <- . # rotate2, axiom. member(ordered_pair(ordered_pair(V, W), U), X) <- member(ordered_pair(ordered_pair(U, V), W), rotate(X)). # rotate3, axiom. member(ordered_pair(ordered_pair(U, V), W), rotate(X)) <- 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)). # flip1, axiom. subclass(flip(X), cross_product(cross_product(universal_class, universal_class), universal_class)) <- . # flip2, axiom. member(ordered_pair(ordered_pair(V, U), W), X) <- member(ordered_pair(ordered_pair(U, V), W), flip(X)). # flip3, axiom. member(ordered_pair(ordered_pair(U, V), W), flip(X)) <- 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)). # inverse, axiom. equal(domain_of(flip(cross_product(Y, universal_class))), inverse(Y)) <- . # range_of, axiom. equal(domain_of(inverse(Z)), range_of(Z)) <- . # domain, axiom. equal(first(not_subclass_element(restrict(Z, X, singleton(Y)), null_class)), domain(Z, X, Y)) <- . # range, axiom. equal(second(not_subclass_element(restrict(Z, singleton(X), Y), null_class)), range(Z, X, Y)) <- . # image, axiom. equal(range_of(restrict(Xr, X, universal_class)), image(Xr, X)) <- . # successor, axiom. equal(union(X, singleton(X)), successor(X)) <- . # successor_relation1, axiom. subclass(successor_relation, cross_product(universal_class, universal_class)) <- . # successor_relation2, axiom. equal(successor(X), Y) <- member(ordered_pair(X, Y), successor_relation). # successor_relation3, axiom. member(ordered_pair(X, Y), successor_relation) <- equal(successor(X), Y), member(ordered_pair(X, Y), cross_product(universal_class, universal_class)). # inductive1, axiom. member(null_class, X) <- inductive(X). # inductive2, axiom. subclass(image(successor_relation, X), X) <- inductive(X). # inductive3, axiom. inductive(X) <- member(null_class, X), subclass(image(successor_relation, X), X). # omega_is_inductive1, axiom. inductive(omega) <- . # omega_is_inductive2, axiom. subclass(omega, Y) <- inductive(Y). # omega_in_universal, axiom. member(omega, universal_class) <- . # sum_class_definition, axiom. equal(domain_of(restrict(element_relation, universal_class, X)), sum_class(X)) <- . # sum_class2, axiom. member(sum_class(X), universal_class) <- member(X, universal_class). # power_class_definition, axiom. equal(complement(image(element_relation, complement(X))), power_class(X)) <- . # power_class2, axiom. member(power_class(U), universal_class) <- member(U, universal_class). # compose1, axiom. subclass(compose(Yr, Xr), cross_product(universal_class, universal_class)) <- . # compose2, axiom. member(Z, image(Yr, image(Xr, singleton(Y)))) <- member(ordered_pair(Y, Z), compose(Yr, Xr)). # compose3, axiom. member(ordered_pair(Y, Z), compose(Yr, Xr)) <- member(Z, image(Yr, image(Xr, singleton(Y)))), member(ordered_pair(Y, Z), cross_product(universal_class, universal_class)). # single_valued_class1, axiom. subclass(compose(X, inverse(X)), identity_relation) <- single_valued_class(X). # single_valued_class2, axiom. single_valued_class(X) <- subclass(compose(X, inverse(X)), identity_relation). # function1, axiom. subclass(Xf, cross_product(universal_class, universal_class)) <- function(Xf). # function2, axiom. subclass(compose(Xf, inverse(Xf)), identity_relation) <- function(Xf). # function3, axiom. function(Xf) <- subclass(Xf, cross_product(universal_class, universal_class)), subclass(compose(Xf, inverse(Xf)), identity_relation). # replacement, axiom. member(image(Xf, X), universal_class) <- function(Xf), member(X, universal_class). # regularity1, axiom. equal(X, null_class); member(regular(X), X) <- . # regularity2, axiom. equal(X, null_class); equal(intersection(X, regular(X)), null_class) <- . # apply, axiom. equal(sum_class(image(Xf, singleton(Y))), apply(Xf, Y)) <- . # choice1, axiom. function(choice) <- . # choice2, axiom. equal(Y, null_class); member(apply(choice, Y), Y) <- member(Y, universal_class). # one_to_one1, axiom. function(Xf) <- one_to_one(Xf). # one_to_one2, axiom. function(inverse(Xf)) <- one_to_one(Xf). # one_to_one3, axiom. one_to_one(Xf) <- function(inverse(Xf)), function(Xf). # 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) <- . # identity_relation, axiom. equal(intersection(inverse(subset_relation), subset_relation), identity_relation) <- . # diagonalisation, axiom. equal(complement(domain_of(intersection(Xr, identity_relation))), diagonalise(Xr)) <- . # cantor_class, axiom. equal(intersection(domain_of(X), diagonalise(compose(inverse(element_relation), X))), cantor(X)) <- . # operation1, axiom. function(Xf) <- operation(Xf). # operation2, axiom. equal(cross_product(domain_of(domain_of(Xf)), domain_of(domain_of(Xf))), domain_of(Xf)) <- operation(Xf). # operation3, axiom. subclass(range_of(Xf), domain_of(domain_of(Xf))) <- operation(Xf). # operation4, axiom. operation(Xf) <- 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))). # compatible1, axiom. function(Xh) <- compatible(Xh, Xf1, Xf2). # compatible2, axiom. equal(domain_of(domain_of(Xf1)), domain_of(Xh)) <- compatible(Xh, Xf1, Xf2). # compatible3, axiom. subclass(range_of(Xh), domain_of(domain_of(Xf2))) <- compatible(Xh, Xf1, Xf2). # compatible4, axiom. compatible(Xh, Xf1, Xf2) <- function(Xh), equal(domain_of(domain_of(Xf1)), domain_of(Xh)), subclass(range_of(Xh), domain_of(domain_of(Xf2))). # homomorphism1, axiom. operation(Xf1) <- homomorphism(Xh, Xf1, Xf2). # homomorphism2, axiom. operation(Xf2) <- homomorphism(Xh, Xf1, Xf2). # homomorphism3, axiom. compatible(Xh, Xf1, Xf2) <- homomorphism(Xh, Xf1, Xf2). # homomorphism4, axiom. equal(apply(Xf2, ordered_pair(apply(Xh, X), apply(Xh, Y))), apply(Xh, apply(Xf1, ordered_pair(X, Y)))) <- homomorphism(Xh, Xf1, Xf2), member(ordered_pair(X, Y), domain_of(Xf1)). # homomorphism5, axiom. member(ordered_pair(not_homomorphism1(Xh, Xf1, Xf2), not_homomorphism2(Xh, Xf1, Xf2)), domain_of(Xf1)); homomorphism(Xh, Xf1, Xf2) <- operation(Xf1), operation(Xf2), compatible(Xh, Xf1, Xf2). # homomorphism6, axiom. homomorphism(Xh, Xf1, Xf2) <- 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))))). # compose_class_definition1, axiom. subclass(compose_class(X), cross_product(universal_class, universal_class)) <- . # compose_class_definition2, axiom. equal(compose(X, Y), Z) <- member(ordered_pair(Y, Z), compose_class(X)). # compose_class_definition3, axiom. member(ordered_pair(Y, Z), compose_class(X)) <- member(ordered_pair(Y, Z), cross_product(universal_class, universal_class)), equal(compose(X, Y), Z). # definition_of_composition_function1, axiom. subclass(composition_function, cross_product(universal_class, cross_product(universal_class, universal_class))) <- . # definition_of_composition_function2, axiom. equal(compose(X, Y), Z) <- member(ordered_pair(X, ordered_pair(Y, Z)), composition_function). # definition_of_composition_function3, axiom. member(ordered_pair(X, ordered_pair(Y, compose(X, Y))), composition_function) <- member(ordered_pair(X, Y), cross_product(universal_class, universal_class)). # definition_of_domain_relation1, axiom. subclass(domain_relation, cross_product(universal_class, universal_class)) <- . # definition_of_domain_relation2, axiom. equal(domain_of(X), Y) <- member(ordered_pair(X, Y), domain_relation). # definition_of_domain_relation3, axiom. member(ordered_pair(X, domain_of(X)), domain_relation) <- member(X, universal_class). # single_valued_term_defn1, axiom. equal(first(not_subclass_element(compose(X, inverse(X)), identity_relation)), single_valued1(X)) <- . # single_valued_term_defn2, axiom. equal(second(not_subclass_element(compose(X, inverse(X)), identity_relation)), single_valued2(X)) <- . # single_valued_term_defn3, axiom. equal(domain(X, image(inverse(X), singleton(single_valued1(X))), single_valued2(X)), single_valued3(X)) <- . # compose_can_define_singleton, axiom. equal(intersection(complement(compose(element_relation, complement(identity_relation))), element_relation), singleton_relation) <- . # application_function_defn1, axiom. subclass(application_function, cross_product(universal_class, cross_product(universal_class, universal_class))) <- . # application_function_defn2, axiom. member(Y, domain_of(X)) <- member(ordered_pair(X, ordered_pair(Y, Z)), application_function). # application_function_defn3, axiom. equal(apply(X, Y), Z) <- member(ordered_pair(X, ordered_pair(Y, Z)), application_function). # application_function_defn4, axiom. member(ordered_pair(X, ordered_pair(Y, apply(X, Y))), application_function) <- member(ordered_pair(X, ordered_pair(Y, Z)), cross_product(universal_class, cross_product(universal_class, universal_class))), member(Y, domain_of(X)). # maps1, axiom. function(Xf) <- maps(Xf, X, Y). # maps2, axiom. equal(domain_of(Xf), X) <- maps(Xf, X, Y). # maps3, axiom. subclass(range_of(Xf), Y) <- maps(Xf, X, Y). # maps4, axiom. maps(Xf, domain_of(Xf), Y) <- function(Xf), subclass(range_of(Xf), Y). # symmetrization, axiom. equal(union(X, inverse(X)), symmetrization_of(X)) <- . # irreflexive1, axiom. subclass(restrict(X, Y, Y), complement(identity_relation)) <- irreflexive(X, Y). # irreflexive2, axiom. irreflexive(X, Y) <- subclass(restrict(X, Y, Y), complement(identity_relation)). # connected1, axiom. subclass(cross_product(Y, Y), union(identity_relation, symmetrization_of(X))) <- connected(X, Y). # connected2, axiom. connected(X, Y) <- subclass(cross_product(Y, Y), union(identity_relation, symmetrization_of(X))). # transitive1, axiom. subclass(compose(restrict(Xr, Y, Y), restrict(Xr, Y, Y)), restrict(Xr, Y, Y)) <- transitive(Xr, Y). # transitive2, axiom. transitive(Xr, Y) <- subclass(compose(restrict(Xr, Y, Y), restrict(Xr, Y, Y)), restrict(Xr, Y, Y)). # asymmetric1, axiom. equal(restrict(intersection(Xr, inverse(Xr)), Y, Y), null_class) <- asymmetric(Xr, Y). # asymmetric2, axiom. asymmetric(Xr, Y) <- equal(restrict(intersection(Xr, inverse(Xr)), Y, Y), null_class). # segment, axiom. equal(segment(Xr, Y, Z), domain_of(restrict(Xr, Y, singleton(Z)))) <- . # well_ordering1, axiom. connected(X, Y) <- well_ordering(X, Y). # well_ordering2, axiom. equal(U, null_class); member(least(Xr, U), U) <- well_ordering(Xr, Y), subclass(U, Y). # well_ordering3, axiom. member(least(Xr, U), U) <- well_ordering(Xr, Y), subclass(U, Y), member(V, U). # well_ordering4, axiom. equal(segment(Xr, U, least(Xr, U)), null_class) <- well_ordering(Xr, Y), subclass(U, Y). # well_ordering5, axiom. <- well_ordering(Xr, Y), subclass(U, Y), member(V, U), member(ordered_pair(V, least(Xr, U)), Xr). # well_ordering6, axiom. well_ordering(Xr, Y) <- connected(Xr, Y), equal(not_well_ordering(Xr, Y), null_class). # well_ordering7, axiom. subclass(not_well_ordering(Xr, Y), Y); well_ordering(Xr, Y) <- connected(Xr, Y). # well_ordering8, axiom. well_ordering(Xr, Y) <- member(V, not_well_ordering(Xr, Y)), equal(segment(Xr, not_well_ordering(Xr, Y), V), null_class), connected(Xr, Y). # section1, axiom. subclass(Y, Z) <- section(Xr, Y, Z). # section2, axiom. subclass(domain_of(restrict(Xr, Z, Y)), Y) <- section(Xr, Y, Z). # section3, axiom. section(Xr, Y, Z) <- subclass(Y, Z), subclass(domain_of(restrict(Xr, Z, Y)), Y). # ordinal_numbers1, axiom. well_ordering(element_relation, X) <- member(X, ordinal_numbers). # ordinal_numbers2, axiom. subclass(sum_class(X), X) <- member(X, ordinal_numbers). # ordinal_numbers3, axiom. member(X, ordinal_numbers) <- well_ordering(element_relation, X), subclass(sum_class(X), X), member(X, universal_class). # ordinal_numbers4, axiom. member(X, ordinal_numbers); equal(X, ordinal_numbers) <- well_ordering(element_relation, X), subclass(sum_class(X), X). # kind_1_ordinals, axiom. equal(union(singleton(null_class), image(successor_relation, ordinal_numbers)), kind_1_ordinals) <- . # limit_ordinals, axiom. equal(intersection(complement(kind_1_ordinals), ordinal_numbers), limit_ordinals) <- . # rest_of1, axiom. subclass(rest_of(X), cross_product(universal_class, universal_class)) <- . # rest_of2, axiom. member(U, domain_of(X)) <- member(ordered_pair(U, V), rest_of(X)). # rest_of3, axiom. equal(restrict(X, U, universal_class), V) <- member(ordered_pair(U, V), rest_of(X)). # rest_of4, axiom. member(ordered_pair(U, V), rest_of(X)) <- member(U, domain_of(X)), equal(restrict(X, U, universal_class), V). # rest_relation1, axiom. subclass(rest_relation, cross_product(universal_class, universal_class)) <- . # rest_relation2, axiom. equal(rest_of(X), Y) <- member(ordered_pair(X, Y), rest_relation). # rest_relation3, axiom. member(ordered_pair(X, rest_of(X)), rest_relation) <- member(X, universal_class). # recursion_equation_functions1, axiom. function(Z) <- member(X, recursion_equation_functions(Z)). # recursion_equation_functions2, axiom. function(X) <- member(X, recursion_equation_functions(Z)). # recursion_equation_functions3, axiom. member(domain_of(X), ordinal_numbers) <- member(X, recursion_equation_functions(Z)). # recursion_equation_functions4, axiom. equal(compose(Z, rest_of(X)), X) <- member(X, recursion_equation_functions(Z)). # recursion_equation_functions5, axiom. member(X, recursion_equation_functions(Z)) <- function(Z), function(X), member(domain_of(X), ordinal_numbers), equal(compose(Z, rest_of(X)), X). # union_of_range_map1, axiom. subclass(union_of_range_map, cross_product(universal_class, universal_class)) <- . # union_of_range_map2, axiom. equal(sum_class(range_of(X)), Y) <- member(ordered_pair(X, Y), union_of_range_map). # union_of_range_map3, axiom. member(ordered_pair(X, Y), union_of_range_map) <- member(ordered_pair(X, Y), cross_product(universal_class, universal_class)), equal(sum_class(range_of(X)), Y). # ordinal_addition, axiom. equal(apply(recursion(X, successor_relation, union_of_range_map), Y), ordinal_add(X, Y)) <- . # ordinal_multiplication, axiom. equal(recursion(null_class, apply(add_relation, X), union_of_range_map), ordinal_multiply(X, Y)) <- . # integer_function1, axiom. equal(integer_of(X), X) <- member(X, omega). # integer_function2, axiom. member(X, omega); equal(integer_of(X), null_class) <- . # prove_sections_property3_1, conjecture. well_ordering(xr, y) <- . # prove_sections_property3_2, conjecture. section(xr, w, y) <- . # prove_sections_property3_3, conjecture. <- member(least(xr, intersection(complement(w), y)), y). # prove_sections_property3_4, conjecture. <- equal(y, w). #--------------------------------------------------------------------------