Axioms for the theory of proveit.numbers.negation

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.logic import Forall, Equals
from proveit import a, b, c
from proveit.numbers import Add, Neg, zero, Natural
In [2]:
%begin axioms
Defining axioms for theory 'proveit.numbers.negation'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions
In [3]:
negation_is_injunctive = Forall((a, b), Equals(a, b), condition=[Equals(Neg(a), Neg(b))], domain=Natural)

Negation is defined as the additive inverse of the natural numbers, extending the natural number set to all integer numbers. This will extend to other number sets through the definitions of the operations that extend the set of Integer numbers to other number sets (division for rational numbers, exponentiation for real numbers and complex numbers).

In [4]:
# By default, Add(a, Neg(a)) will display in the subtraction style (the same as subtract(a, a))
neg_def_add_inv = Forall((a, b, c), Equals(Add(c, Neg(a)), b), 
                conditions=[Equals(Add(a, b), c)], 
In [5]:
%end axioms
These axioms may now be imported from the theory package: proveit.numbers.negation