Axioms for the theory of proveit.logic.sets.intersection

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Forall, Exists, And, Equals, InSet, Intersect, IntersectAll
from proveit import m, n, x, Q, R
from proveit.core_expr_types import y_1_to_n, A_1_to_m, Q__y_1_to_n, R__y_1_to_n, S_1_to_n
from proveit.logic.sets import x_in_every_A, general_intersectall_Ryn
from proveit.numbers import NaturalPos
%begin axioms

Defining axioms for theory 'proveit.logic.sets.intersection'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Membership in the intersection of sets is the same as having membership in all of the sets being intersected:

intersection_def = Forall(m, Forall((x, A_1_to_m), 
                                   Equals(InSet(x, Intersect(A_1_to_m)),
                                          x_in_every_A).with_wrap_after_operator()), 
                         domain=NaturalPos)

intersection_def:

We can intersect over all instances of sets under some criteria, but there must be at least one set (we cannot allow a universal set -- we cannot allow a set to contain itself or we will be subject to Russel's paradox):

intersect_all_def = Forall(n, 
                           Forall((S_1_to_n, Q, R, x), 
                                  Equals(InSet(x, general_intersectall_Ryn),
                                         Forall(y_1_to_n, InSet(x, R__y_1_to_n), 
                                                domains=[S_1_to_n], conditions=[Q__y_1_to_n]))
                                  .with_wrap_before_operator(),
                                  condition=Exists(y_1_to_n, Q__y_1_to_n,domains=[S_1_to_n])),
                          domain=NaturalPos)

intersect_all_def:

%end axioms

These axioms may now be imported from the theory package: proveit.logic.sets.intersection