Natural Numbers
We will pay special attention to the definition of natural numbers because it will be our foundation for number theory. Our axioms are chosen based on second-order arithmetic, following Robinson's axioms for numberhood and Frege's axioms for cardinality.
Numberhood
Zero is a natural number. In fact, the natural numbers are zero and the successors.
| Name | Statement |
|---|---|
| ax-nat-no | li no kacna'u |
| ax-succ-std | ro da poi ke'a kacna'u ku'o zo'u ga da du li no gi su'o de zo'u de kacli'e da |
Zero is not a successor. Combined with the above axioms, this constrains the natural numbers to a single tower of successors above zero.
| Name | Statement |
|---|---|
| ax-succ-zero | naku zo'u ko'a kacli'e li no |
While many results do not require it, we also have the Axiom of Successors, which states that the operator/function taking each natural number to its successor is injective.
| Name | Statement |
|---|---|
| ax-baihei-inj | ganai li bai'ei ku'i'a du li bai'ei ku'i'e gi li ku'i'a du li ku'i'e |
Induction over natural numbers is definable in second-order logic.
| Name | Statement |
|---|---|
| ax-nat-ind | ganai ge li no bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a |
Addition
Addition is given via standard axioms.
| Name | Statement |
|---|---|
| ax-plus-zero | li su'i ku'i'a no du li ku'i'a |
| ax-plus-succ | li su'i ku'i'a bai'ei ku'i'e du li bai'ei su'i ku'i'a ku'i'e |
We have not proven many arithmetic results yet.
| Name | Statement |
|---|---|
| 1p0e1 | li su'i pa no du li pa |
Multiplication
Multiplication is also given via standard axioms.
| Name | Statement |
|---|---|
| ax-mul-zero | li pi'i ku'i'a no du li no |
| ax-mul-succ | li pi'i ku'i'a bai'ei ku'i'e du li su'i pi'i ku'i'a ku'i'e ku'i'a |
Ordering
The natural numbers are totally ordered. This order is not realized on its own, but defined recursively.
| Name | Statement |
|---|---|
| ax-gt-zero | naku zo'u ko'a kacme'a li no |
| df-kacmeha | go ko'a kacme'a ko'e gi su'o da poi ke'a kacli'e ko'a zo'u ga da kacme'a ko'e gi da du ko'e |
Cardinality
We also have some axioms of Fregean cardinality.
| Name | Statement |
|---|---|
| ax-card-fun | ganai ko'a .e ko'e kazmi ko'i gi ko'a du ko'e |
| ax-card-ex | go li no kazmi pa ka ce'u bo'a kei gi naku zo'u su'o da zo'u da bo'a |