logo

Axioms for the theory of proveit.numbers.numerals.decimals

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 Literal
from proveit import n, x
from proveit.logic import Equals, Forall, And, InSet
from proveit.numbers import num, zero, one, Add, LessEq, Natural
from proveit.numbers.numerals.decimals import DecimalSequence, Digits
In [2]:
%begin axioms
Defining axioms for theory 'proveit.numbers.numerals.decimals'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions
In [3]:
one_def = Equals(num(1), Add(zero, one))
one_def:
In [4]:
two_def = Equals(num(2), Add(one, one))
two_def:
In [5]:
three_def = Equals(num(3), Add(num(2), one))
three_def:
In [6]:
four_def = Equals(num(4), Add(num(3), one))
four_def:
In [7]:
five_def = Equals(num(5), Add(num(4), one))
five_def:
In [8]:
six_def = Equals(num(6), Add(num(5), one))
six_def:
In [9]:
seven_def = Equals(num(7), Add(num(6), one))
seven_def:
In [10]:
eight_def = Equals(num(8), Add(num(7), one))
eight_def:
In [11]:
nine_def = Equals(num(9), Add(num(8), one))
nine_def:
In [12]:
#\forall_{n} (n \in N_{\leq 9}) = (n \in N and n \leq 9)
In [13]:
N_leq_9_def = Forall(n, Equals(InSet(n, Digits), And(InSet(n, Natural), LessEq(n, num(9)))))
N_leq_9_def:
In [14]:
single_digit_reduction = Forall(n, Equals(DecimalSequence(n), n), domain=Digits)
single_digit_reduction:
In [15]:
%end axioms
These axioms may now be imported from the theory package: proveit.numbers.numerals.decimals