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

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import n, x
from proveit.logic import Forall, Equals, InSet, Set, EmptySet
from proveit.core_expr_types import y_1_to_n
from proveit.logic.sets import x_equals_any_y
from proveit.numbers import Natural
%begin axioms
Defining axioms for theory 'proveit.logic.sets.enumeration'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Membership in an enumeration is the same as being equal to any of the contents of the enumeration:

In [2]:
enum_set_def = Forall(n, Forall((x, y_1_to_n), 
                              Equals(InSet(x, Set(y_1_to_n)), 

Define the empty set as an enumerated set with no elements.

In [3]:
empty_set_def = Equals(EmptySet, Set())
In [4]:
# might need an axiom here:
# if 2 enum sets are SetEquiv then they are equal
# see some hard-copy notes/comments from project meeting 2/07/2020
In [ ]:
In [5]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.sets.enumeration