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

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 Card, EmptySet, Equals, Union, Set, InSet, NotInSet, Forall
from proveit.numbers import num, Add, Natural
from proveit import x, S
%begin axioms

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

The cardinality of the empty set, $\emptyset$, is zero (the base case of an induction for the cardinality of finite sets):

empty_card = Equals(Card(EmptySet), num(0))

empty_card:

When a new element is added to a finite set, its cardinality increases by one (the induction rule for the cardinality of finite sets):

card_induction = Forall((x, S), Equals(Card(Union(S, Set(x))), 
                                      Add(Card(S), num(1))), conditions=[InSet(Card(S), Natural), NotInSet(x, S)])

card_induction:

The cardinality of inifite sets should be defined via 1-to-1 and onto mappings between them.

%end axioms

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