Axioms for the theory of proveit.numbers.number_sets.integers

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 And, Equals, Forall, Iff, Implies, InSet, SetEquiv, SetOfAll, SubsetProper, Union
from proveit.numbers import Complex, Integer, Interval, Natural, NaturalPos, Neg
from proveit.numbers import Add, greater, Less, LessEq, number_ordering
from proveit.numbers import zero, one, num
from proveit import a, b, n, m, x, y, S
%begin axioms

Defining axioms for theory 'proveit.numbers.number_sets.integers'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Define the set of naturals, $\mathbb{N}$, as, essentially, the minimal set that contains zero and all of its successors:

#naturals_def = Forall(n, Equals(InSet(n, Natural), Forall(S, Implies(And(InSet(zero, S), Forall(x, InSet(Add(x,one), S), domain=S)), InSet(n, S)))))

that is, $n \in \mathbb{N}$ iff n is in all sets that contain zero and all successors.

Define the integers, $\mathbb{Z}$ as the union of the naturals and the negated positive naturals (i.e., the positive and negative forms of all natural numbers where zero is its own negative):

integers_def = Equals(Integer, Union(Natural, SetOfAll(n, Neg(n), domain=NaturalPos)))

integers_def:

Defining properties of individual natural numbers:

#add_by_zero = Forall(x, Equals(Add(x, zero), x), domain=Complex)

Defining properties of an Interval (a set of contiguous integers):

integer_interval_is_subset_of_integers = Forall(
    (a, b),
    SubsetProper(Interval(a, b), Integer),
    domain = Integer)

integer_interval_is_subset_of_integers:

Note: if $b < a$, $\{a~\ldotp \ldotp~b\}$ is equivalent to the empty set.

integer_interval_element_bounds = Forall(
    (a, b),
    Forall(n,
           number_ordering(LessEq(a, n), LessEq(n, b)),
           domain = Interval(a, b)),
    domain = Integer)

integer_interval_element_bounds:

# Consider this as an alternative??
# from proveit import ExprRange
# from proveit.logic import Set
#Forall((a, b), Equals(Interval(a, b), Set(ExprRange(n, n, a, b))), domain=Integer)

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.number_sets.integers