See discussions, stats, and author profiles for this publication at: [Link]

net/publication/308200059

The Nature of Natural Numbers - Peano Axioms and Arithmetics: A Formal

Development in PowerEpsilon

Working Paper · October 2012

DOI: 10.13140/RG.2.2.28839.96164

CITATIONS READS

0 2,651

1 author:

Ming-Yuan Zhu
CoreTek Systems, Inc., Beijing, People's Republic of China
141 PUBLICATIONS 517 CITATIONS

SEE PROFILE

Some of the authors of this publication are also working on these related projects:

The Formal Semantics of Programming Languages and Compiler Constructions View project

Mechanical Theorem Proof Development System - PowerEpsilon View project

All content following this page was uploaded by Ming-Yuan Zhu on 17 September 2016.

The user has requested enhancement of the downloaded file.

 The Nature of Natural Numbers -
Peano Axioms and Arithmetics:
A Formal Development in PowerEpsilon
Ming-Yuan Zhu
CoreTek Systems, Inc.
11th Floor, 1109, CEC Building
6 South Zhongguancun Street
Beijing 100086
People’s Republic of China
September 25, 2012

This article is dedicated to the 87th birthday of my father.

He has contributed his whole life to the development of science and technology of China.
He will always live in my memory for his dedication, courage, spirit and love.

Abstract PowerEpsilon is my own development of mathematical theorem proof development system. It belongs to a
large family of computer-based tools whose purpose is to help in proving theorems, namely, Automath, COQ, Nqthm,
Mizar, LCF, Nuprl, Isabelle, Lego, HOL, PVS and ACL2. In this paper, we will present a formal investigation of
natural numbers, Peano axioms and arithmetics using PowerEpsilon.

1 Introduction
We all know about natural numbers. We are using natural numbers everyday for counting and ordering. However what is the
nature of natural numbers and how the natural numbers are formed? These questions are concerned by mathematicians for
several hundred years. Properties of the natural numbers related to divisibility, such as the distribution of prime numbers,
are studied in number theory. Problems concerning counting and ordering, such as partition enumeration, are studied in
combinatorics. Historically, the precise mathematical definition of the natural numbers developed with some difficulty.
The Peano axioms state conditions that any successful definition must satisfy. Certain constructions show that, given set
theory, models of the Peano postulates must exist. In this paper, we will provide a deep investigation of formal definition
of natural numbers in type theory1 .
PowerEpsilon, currently developed by author, is a strongly-typed polymorphic functional programming language based
on Martin-Löf’s type theory [10, 8, 9] and the calculus of constructions [5]. In PowerEpsilon, the concept of limit of type
universe hierarchies and a scheme for inductive define types are introduced. The system can be used as both a programming
language with a very rich set of data structures and a metalanguage for formalizing constructive mathematics. The system
has been implemented using the software development system AUTOSTAR constructed by author [12]. PowerEpsilon
is a proof checker much similar to other mechanical proof checkers, such as ACL2[2], COQ[4, 1], LCF[6], Isabelle[11],
Nuprl[3] and HOL[7], which are completely formal user-controlled systems. However, PowerEpsilon is more powerful
than LCF and Nuprl, in which the equality and induction rules for arbitrary inductive types are definable.
1 This work is supported in part by the TRUSTIE Project of Hi-Tech Research and Development Program of China (863 Program)

under Grant No. 2007AA010304, by the Open Fund of the State Key Laboratory of Software Development Environment under Grant
No. SKLSDE-2010KF-0X, Beijing University of Aeronautics and Astronautics, and by the National Basic Research Program of China
(973 Program) under Grant No. 2005CB321901

1
2 Peano Axioms
2.1 History of Peano Axioms
In mathematical logic, the Peano axioms, also known as the Dedekind-Peano axioms or the Peano postulates, are a set
of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms
have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental
questions of consistency and completeness of number theory.
The need for formalism in arithmetic was not well appreciated until the work of Hermann Grassmann, who showed
in the 1860s that many facts in arithmetic could be derived from more basic facts about the successor operation and
induction. In 1881, Charles Sanders Peirce provided an axiomatization of natural-number arithmetic. In 1888, Richard
Dedekind proposed a collection of axioms about the numbers, and in 1889 Peano published a more precisely formulated
version of them as a collection of axioms in his book, The principles of arithmetic presented by a new method (Latin:
Arithmetices principia, nova methodo exposita).
The Peano axioms contain three types of statements. The first axiom asserts the existence of at least one member of
the set “number”. The next four are general statements about equality; in modern treatments these are often considered
axioms of the “underlying logic”. The next three axioms are first-order statements about natural numbers expressing the
fundamental properties of the successor operation. The ninth, final axiom is a second order statement of the principle
of mathematical induction over the natural numbers. A weaker first-order system called Peano arithmetic is obtained by
explicitly adding the addition and multiplication operation symbols and replacing the second-order induction axiom with
a first-order axiom schema.
Peano formulated his axioms, the language of mathematical logic was in its infancy. The system of logical notation
he created to present the axioms did not prove to be popular, although it was the genesis of the modern notation for set
membership (∈, which is from Peano’s ϵ) and implication (⊃, which is from Peano’s reversed ‘C’.) Peano maintained a
clear distinction between mathematical and logical symbols, which was not yet common in mathematics; such a separation
had first been introduced in the Begriffsschrift by Gottlob Frege, published in 1879. Peano was unaware of Frege’s work
and independently recreated his logical apparatus based on the work of Boole and Schröder.

2.2 Formulation of Peano Axioms

The Peano axioms define the arithmetical properties of natural numbers, usually represented as a set N or The signature
(a formal language’s non-logical symbols) for the axioms includes a constant symbol 0 and a unary function symbol S.
The constant 0 is assumed to be a natural number:
1. 0 is a natural number.
The next four axioms describe the equality relation.
2. For every natural number x, x = x. That is, equality is reflexive.
3. For all natural numbers x and y, if x = y, then y = x. That is, equality is symmetric.
4. For all natural numbers x, y and z, if x = y and y = z, then x = z. That is, equality is transitive.
5. For all a and b, if a is a natural number and a = b, then b is also a natural number. That is, the natural numbers
are closed under equality.
The remaining axioms define the arithmetical properties of the natural numbers. The naturals are assumed to be closed
under a single-valued “successor” function S.
6. For every natural number n, S(n) is a natural number.
Peano’s original formulation of the axioms used 1 instead of 0 as the “first” natural number. This choice is arbitrary, as
axiom 1 does not endow the constant 0 with any additional properties. However, because 0 is the additive identity in
arithmetic, most modern formulations of the Peano axioms start from 0. Axioms 1 and 6 define a unary representation
of the natural numbers: the number 1 is S(0), 2 is S(S(0)) (which is also S(1)), and, in general, any natural number n is
S n (0). The next two axioms define the properties of this representation.
7. For every natural number n, S(n) = 0 is False. That is, there is no natural number whose successor is 0.
8. For all natural numbers m and n, if S(m) = S(n), then m = n. That is, S is an injection.
Axioms 1, 6, 7 and 8 imply that the set of natural numbers is infinite, because it contains at least the infinite subset
{0, S(0), S(S(0)), . . .}, each element of which differs from the rest. To show that every natural number is included in this
set requires an additional axiom, which is sometimes called the axiom of induction. This axiom provides a method for
reasoning about the set of all natural numbers.

2
 9. If K is a set such that:
• 0 is in K, and
• for every natural number n, if n is in K, then S(n) is in K,
then K contains every natural number.
The induction axiom is sometimes stated in the following form:
9. If ϕ is a unary predicate such that:
• ϕ(0) is true, and
• for every natural number n, if ϕ(n) is true, then ϕ(S(n)) is true,
then ϕ(n) is true for every natural number n.
In Peano’s original formulation, the induction axiom is a second-order axiom. It is now common to replace this second-
order principle with a weaker first-order induction scheme. There are important differences between the second-order and
first-order formulations, as discussed in the section below. Without the axiom of induction, the remaining Peano axioms
give a theory equivalent to Robinson arithmetic, which can be expressed without second-order logic.

2.3 Natural Number in Type Theory

2.3.1 Definition of Nat
Inductive Type Nat

def Nat = !(T : Prop) [T -> [T -> T] -> T];

Constructors of Nat

def OO =
\(T : Prop, x : T, y : [T -> T])
x;

def SS =
\(t : Nat, T : Prop, x : T, y : [T -> T])
@(y, @(t, T, x, y));

Canonical Functions of Nat

def IS_ZERO = \(n : Nat) @(n, Bool, TT, \(x : Bool) FF);

def ADD =
\(n1 : Nat, n2 : Nat)
@(n1, Nat, n2, SS);

def TIMES =
\(n1 : Nat, n2 : Nat)
@(n1, Nat, OO, @(ADD, n2));

def EXP =
\(n1 : Nat, n2 : Nat)
@(n1, Nat, @(SS, OO), @(TIMES, n2));

def EQUAL =
\(n1 : Nat, n2 : Nat)

3
 @(BIF_THEN_ELSE,
@(IS_ZERO, n1),
@(IS_ZERO, n2),
@(BIF_THEN_ELSE,
@(IS_ZERO, n2),
FF,
@(EQUAL, @(PP, n1), @(PP, n2))));

def LESS =
\(n1 : Nat, n2 : Nat)
@(BIF_THEN_ELSE,
@(IS_ZERO, n1),
@(BIF_THEN_ELSE,
@(IS_ZERO, n2),
FF,
TT),
@(BIF_THEN_ELSE,
@(IS_ZERO, n2),
FF,
@(LESS, @(PP, n1), @(PP, n2))));

def LESSEQ =
\(n1 : Nat, n2 : Nat)
@(BIF_THEN_ELSE,
@(IS_ZERO, n1),
TT,
@(BIF_THEN_ELSE,
@(IS_ZERO, n2),
FF,
@(LESSEQ, @(PP, n1), @(PP, n2))));

def NLE =
\(n1 : Nat, n2 : Nat)
@(OR, @(LESS, n1, n2), @(EQUAL, n1, n2));

def NGE =
\(n1 : Nat, n2 : Nat)
@(NLE, n2, n1);

Predecessor Function
Inductive Definition of Predecessor Function

def T = \(x : Nat, y : Nat) x;

def F = \(x : Nat, y : Nat) y;

def PP =
\(n : Nat)
@(n,
[[Nat -> Nat -> Nat] -> Nat],
\(u : [Nat -> Nat -> Nat]) @(u, OO, OO),
\(p : [[Nat -> Nat -> Nat] -> Nat],
v : [Nat -> Nat -> Nat])
@(v, @(SS, @(p, T)), @(p, T)),
F);

4
Predecessor Function Defined by Pattern Matching

dec PP : [Nat -> Nat];

def PP =
\(n : Nat)
pattern n is
OO => OO;
@(SS, m) => m
end;

Strong Specification of Predecessor Function

def PredSpec =
\(n : Nat)
?(m : Nat)
@(Or,
@(And, @(Equal, Nat, n, OO), @(Equal, Nat, m, OO)),
@(Equal, Nat, n, @(SS, m)));

def MkPredSpec =
\(n : Nat,
m : Nat,
p : @(Or,
@(And, @(Equal, Nat, n, OO), @(Equal, Nat, m, OO)),
@(Equal, Nat, n, @(SS, m))))
<m, p>;

dec PRED : !(n : Nat) @(PredSpec, n);

dec PredLem1 : @(PredSpec, OO);

def PredLem1 =
let n = OO,
m = OO,
p = @(Refl_Eq, Nat, n),
q = @(Refl_Eq, Nat, m) in
@(MkPredSpec,
n,
m,
@(INJ1,
@(And, @(Equal, Nat, n, OO), @(Equal, Nat, m, OO)),
@(Equal, Nat, n, @(SS, m)),
@(ANDS, @(Equal, Nat, n, OO), @(Equal, Nat, m, OO), p, q)));

dec PredLem2 :
!(n : Nat)
[@(PredSpec, n) -> @(PredSpec, @(SS, n))];

def PredLem2 =
\(n : Nat)
\(H : @(PredSpec, n))
let m = @(FST, H),
p = @(SND, H) in
@(WHEN0,

5
 @(And, @(Equal, Nat, n, OO), @(Equal, Nat, m, OO)),
@(Equal, Nat, n, @(SS, m)),
@(PredSpec, @(SS, n)),
p,
\(q : @(And, @(Equal, Nat, n, OO), @(Equal, Nat, m, OO)))
let P1 = @(Equal, Nat, n, OO),
P2 = @(Equal, Nat, m, OO) in
let p1 = @(PJ1, P1, P2, q),
p2 = @(PJ2, P1, P2, q) in
let u1 = @(Symm_Eq, Nat, m, OO, p2),
u2 = @(Tran_Eq, Nat, n, OO, m, p1, u1) in
let Q = \(z : Nat)
@(Equal, Nat, @(SS, n), @(SS, z)) in
let u3 = @(u2, Q, @(Refl_Eq, Nat, @(SS, n))) in
@(MkPredSpec,
@(SS, n),
m,
@(INJ2,
@(And, @(Equal, Nat, @(SS, n), OO), @(Equal, Nat, m, OO)),
@(Equal, Nat, @(SS, n), @(SS, m)),
u3)),
\(q : @(Equal, Nat, n, @(SS, m)))
let Q = \(z : Nat)
@(Equal, Nat, @(SS, n), @(SS, z)) in
let u = @(q, Q, @(Refl_Eq, Nat, @(SS, n))) in
@(MkPredSpec,
@(SS, n),
@(SS, m),
@(INJ2,
@(And, @(Equal, Nat, @(SS, n), OO), @(Equal, Nat, @(SS, m), OO)),
@(Equal, Nat, @(SS, n), @(SS, @(SS, m))),
u)));

def PRED =
@(NatInduct0,
PredSpec,
PredLem1,
PredLem2);

def PP = \(n : Nat) @(FST, @(PRED, n));

Properties of PP

dec PPSSEqLem1 :
!(n : Nat) @(Equal, Nat, @(PP, @(SS, n)), n);

def PPSSEqLem1 =
\(n : Nat) @(Refl_Eq, Nat, @(PP, @(SS, n)));

dec PPSSEqLem2 :
!(n : Nat)
@(Equal, Nat, @(SS, @(PP, @(SS, n))), @(SS, n));

def PPSSEqLem2 =
\(n : Nat)

6
 @(Refl_Eq, Nat, @(SS, @(PP, @(SS, n))));

Induction Rules

dec NatInduct :
!(P : [Nat -> Prop])
[@(P, OO) ->
!(u : Nat) [@(P, u) -> @(P, @(SS, u))] ->
!(n : Nat)
@(P, n)];

def NatInduct =
\(P : [Nat -> Prop])
\(a : @(P, OO))
\(f : !(u : Nat) [@(P, u) -> @(P, @(SS, u))])
\(*n : Nat)
@(*n,
@(P, *n),
a,
@(f, *n));

dec PatternMatch :
!(P : [Nat -> Prop])
[@(P, OO) ->
!(p : Nat) @(P, @(SS, p)) ->
!(n : Nat)
@(P, n)];

def PatternMatch =
\(P : [Nat -> Prop])
\(a : @(P, OO), b : !(p : Nat) @(P, @(SS, p)))
\(*n : Nat)
@(*n,
@(P, *n),
a,
\(x : @(P, *n)) @(b, *n));

3 Peano Arithmetic
The Peano axioms can be augmented with the operations of addition and multiplication and the usual total (linear)
ordering on N . The respective functions and relations are constructed in second-order logic, and are shown to be unique
using the Peano axioms.

3.1 Addition
Addition is the function +: N × N → N (written in the usual infix notation, mapping elements of N to other elements
of N ), defined recursively as:
a+0 = a
a + S(b) = S(a + b)
For example,
a + 1 = a + S(0) = S(a + 0) = S(a).
The structure (N , +) is a commutative semigroup with identity element 0. (N , +) is also a cancellative magma, and thus
embeddable in a group. The smallest group embedding N is the integers.

7
3.1.1 Basic Properties of Addition

0+n=n

dec AddLLem0 :
!(n : Nat)
@(Equal, Nat, @(ADD, OO, n), n);

(n + 1) + m = (n + m) + 1

dec AddLLem1 :
!(m : Nat, n : Nat)
@(Equal, Nat, @(ADD, @(SS, n), m), @(SS, @(ADD, n, m)));

n+0=n

dec AddRLem0 :
!(n : Nat)
@(Equal, Nat, @(ADD, n, OO), n);

m + (n + 1) + m = (m + n) + 1

dec AddRLem1 :
!(m : Nat, n : Nat)
@(Equal, Nat, @(ADD, m, @(SS, n)), @(SS, @(ADD, m, n)));

Proofs of AddLLem0
The proof of AddLLem0 is conducted by induction on n.

dec AddL0BasLem : @(Equal, Nat, @(ADD, OO, OO), OO);

def AddL0BasLem = @(Refl_Eq, Nat, @(ADD, OO, OO));

dec AddL0IndLem :
let P = \(n : Nat)
@(Equal, Nat, @(ADD, OO, n), n) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

def AddL0IndLem =
let P = \(n : Nat)
@(Equal, Nat, @(ADD, OO, n), n) in
\(n : Nat, p : @(P, n))
@(Tran_Eq,
Nat,
@(ADD, OO, @(SS, n)),
@(SS, @(ADD, OO, n)),
@(SS, n),

8
 @(AddRLem1, OO, n),
@(Congr_Eq, Nat, Nat, @(ADD, OO, n), n, SS, p));

def AddLLem0 =
let P = \(n : Nat)
@(Equal, Nat, @(ADD, OO, n), n) in
@(NatInduct, P, AddL0BasLem, AddL0IndLem);

A simplified proof using reflexivity of ADD directly.

def AddLLem0 =
\(n : Nat)
@(Refl_Eq, Nat, @(ADD, OO, n));

Proofs of AddRLem0
The proof of AddRLem0 is conducted by induction on n.

dec AddR0BasLem : @(Equal, Nat, @(ADD, OO, OO), OO);

def AddR0BasLem = @(Refl_Eq, Nat, @(ADD, OO, OO));

dec AddR0IndLem :
let P = \(n : Nat)
@(Equal, Nat, @(ADD, n, OO), n) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

def AddR0IndLem =
let P = \(n : Nat)
@(Equal, Nat, @(ADD, n, OO), n) in
\(n : Nat, p : @(P, n))
@(Tran_Eq,
Nat,
@(ADD, @(SS, n), OO),
@(SS, @(ADD, n, OO)),
@(SS, n),
@(AddLLem1, OO, n),
@(Congr_Eq, Nat, Nat, @(ADD, n, OO), n, SS, p));

def AddRLem0 =
let P = \(n : Nat)
@(Equal, Nat, @(ADD, n, OO), n) in
@(NatInduct, P, AddR0BasLem, AddR0IndLem);

Proofs of AddLLem1
The proof of AddLLem1 is conducted by induction on m.

dec AddL1BasLem :
!(n : Nat)
@(Equal, Nat, @(ADD, @(SS, n), OO), @(SS, @(ADD, n, OO)));

def AddL1BasLem =
\(n : Nat)

9
 @(Tran_Eq,
Nat,
@(ADD, @(SS, n), OO),
@(SS, n),
@(SS, @(ADD, n, OO)),
@(AddRLem0, @(SS, n)),
@(Congr_Eq,
Nat,
Nat,
n,
@(ADD, n, OO),
SS,
@(Symm_Eq, Nat, @(ADD, n, OO), n, @(AddRLem0, n))));

dec AddL1IndLem :
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(ADD, @(SS, n), m), @(SS, @(ADD, n, m))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def AddL1IndLem =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(ADD, @(SS, n), m), @(SS, @(ADD, n, m))) in
\(m : Nat, p : @(P, m), n : Nat)
@(Tran_Eq4,
Nat,
@(ADD, @(SS, n), @(SS, m)),
@(SS, @(ADD, @(SS, n), m)),
@(SS, @(SS, @(ADD, n, m))),
@(SS, @(ADD, n, @(SS, m))),
@(AddRLem1, @(SS, n), m),
@(Congr_Eq, Nat, Nat, @(ADD, @(SS, n), m), @(SS, @(ADD, n, m)), SS, @(p, n)),
@(Congr_Eq,
Nat,
Nat,
@(SS, @(ADD, n, m)),
@(ADD, n, @(SS, m)),
SS,
@(Symm_Eq, Nat, @(ADD, n, @(SS, m)), @(SS, @(ADD, n, m)), @(AddRLem1, n, m))));

def AddLLem1 =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(ADD, @(SS, n), m), @(SS, @(ADD, n, m))) in
@(NatInduct, P, AddL1BasLem, AddL1IndLem);

Proofs of AddRLem1
The proof of AddRLem1 is conducted by induction on m.

dec AddR1BasLem :
!(n : Nat)
@(Equal, Nat, @(ADD, OO, @(SS, n)), @(SS, @(ADD, OO, n)));

10
 def AddR1BasLem =
\(n : Nat)
@(Refl_Eq, Nat, @(ADD, OO, @(SS, n)));

dec AddR1IndLem :
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(ADD, m, @(SS, n)), @(SS, @(ADD, m, n))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def AddR1IndLem =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(ADD, m, @(SS, n)), @(SS, @(ADD, m, n))) in
\(m : Nat, p : @(P, m), n : Nat)
@(Tran_Eq4,
Nat,
@(ADD, @(SS, m), @(SS, n)),
@(SS, @(ADD, m, @(SS, n))),
@(SS, @(SS, @(ADD, m, n))),
@(SS, @(ADD, @(SS, m), n)),
@(AddLLem1, @(SS, n), m),
@(Congr_Eq, Nat, Nat, @(ADD, m, @(SS, n)), @(SS, @(ADD, m, n)), SS, @(p, n)),
@(Congr_Eq,
Nat,
Nat,
@(SS, @(ADD, m, n)),
@(ADD, @(SS, m), n),
SS,
@(Symm_Eq, Nat, @(ADD, @(SS, m), n), @(SS, @(ADD, m, n)), @(AddLLem1, n, m))));

def AddRLem1 =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(ADD, m, @(SS, n)), @(SS, @(ADD, m, n))) in
@(NatInduct, P, AddR1BasLem, AddR1IndLem);

3.1.2 Commutativity of Addition

a+b=b+c

dec AddCommLem :
!(n : Nat, m : Nat)
@(Equal, Nat, @(ADD, n, m), @(ADD, m, n));

dec AddCommLem1 :
!(m : Nat)
@(Equal, Nat, @(ADD, OO, m), @(ADD, m, OO));

def AddCommLem1 =
\(n : Nat)
@(Tran_Eq,
Nat,
@(ADD, OO, n),

11
 n,
@(ADD, n, OO),
@(AddLLem0, n),
@(Symm_Eq, Nat, @(ADD, n, OO), n, @(AddRLem0, n)));

dec AddCommLem2 :
let P = \(n : Nat)
!(m : Nat)
@(Equal, Nat, @(ADD, n, m), @(ADD, m, n)) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

def AddCommLem2 =
let P = \(n : Nat)
!(m : Nat)
@(Equal, Nat, @(ADD, n, m), @(ADD, m, n)) in
\(n : Nat)
\(p : @(P, n))
\(m : Nat)
@(Tran_Eq4,
Nat,
@(ADD, @(SS, n), m),
@(SS, @(ADD, n, m)),
@(SS, @(ADD, m, n)),
@(ADD, m, @(SS, n)),
@(AddLLem1, m, n),
@(Congr_Eq, Nat, Nat, @(ADD, n, m), @(ADD, m, n), SS, @(p, m)),
@(Symm_Eq, Nat, @(ADD, m, @(SS, n)), @(SS, @(ADD, m, n)), @(AddRLem1, m, n)));

def AddCommLem =
let P = \(n : Nat)
!(m : Nat)
@(Equal, Nat, @(ADD, n, m), @(ADD, m, n)) in
@(NatInduct,
P,
AddCommLem1,
AddCommLem2);

3.1.3 Associativity of Addition

(a + b) + c = a + (b + c)

dec AddAssoLem :
!(m : Nat, n : Nat, e : Nat)
@(Equal, Nat, @(ADD, @(ADD, m, n), e), @(ADD, m, @(ADD, n, e)));

dec AssoBasLem :
!(n : Nat, e : Nat)
@(Equal, Nat, @(ADD, @(ADD, OO, n), e), @(ADD, OO, @(ADD, n, e)));

def AssoBaseLem =
\(n : Nat, e : Nat)
@(Tran_Eq,
Nat,
@(ADD, @(ADD, OO, n), e),

12
 @(ADD, n, e),
@(ADD, OO, @(ADD, n, e)),
@(Congr_Eq, Nat, Nat, @(ADD, OO, n), n, \(m : Nat) @(ADD, m, e), @(AddLLem0, n)),
@(Symm_Eq, Nat, @(ADD, OO, @(ADD, n, e)), @(ADD, n, e), @(AddLLem0, @(ADD, n, e))));

dec AssoIndLem :
let P = \(m : Nat)
!(n : Nat, e : Nat)
@(Equal, Nat, @(ADD, @(ADD, m, n), e), @(ADD, m, @(ADD, n, e))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def AssoIndLem =
let P = \(m : Nat)
!(n : Nat, e : Nat)
@(Equal, Nat, @(ADD, @(ADD, m, n), e), @(ADD, m, @(ADD, n, e))) in
\(m : Nat, p : @(P, m), n : Nat, e : Nat)
@(Tran_Eq4,
Nat,
@(ADD, @(ADD, @(SS, m), n), e),
@(SS, @(ADD, @(ADD, m, n), e)),
@(SS, @(ADD, m, @(ADD, n, e))),
@(ADD, @(SS, m), @(ADD, n, e)),
@(Tran_Eq,
Nat,
@(ADD, @(ADD, @(SS, m), n), e),
@(ADD, @(SS, @(ADD, m, n)), e),
@(SS, @(ADD, @(ADD, m, n), e)),
@(Congr_Eq,
Nat,
Nat,
@(ADD, @(SS, m), n),
@(SS, @(ADD, m, n)),
\(m : Nat) @(ADD, m, e),
@(AddLLem1, n, m)),
@(AddLLem1, e, @(ADD, m, n))),
@(Congr_Eq, Nat, Nat, @(ADD, @(ADD, m, n), e), @(ADD, m, @(ADD, n, e)), SS, @(p, n, e)),
@(Symm_Eq,
Nat,
@(ADD, @(SS, m), @(ADD, n, e)),
@(SS, @(ADD, m, @(ADD, n, e))),
@(AddLLem1, @(ADD, n, e), m)));

def AddAssoLem =
let P = \(m : Nat)
!(n : Nat, e : Nat)
@(Equal,
Nat,
@(ADD, @(ADD, m, n), e),
@(ADD, m, @(ADD, n, e))) in
@(NatInduct, P, AssoBasLem, AssoIndLem);

a + (b + c) = b + (a + c)

dec AddAssComLem :

13
 !(m : Nat, n : Nat, e : Nat)
@(Equal, Nat, @(ADD, m, @(ADD, n, e)), @(ADD, n, @(ADD, m, e)));

def AddAssComLem =
\(m : Nat, n : Nat, e : Nat)
let p1 = @(AddAssoLem, m, n, e),
p2 = @(Symm_Eq, Nat, @(ADD, @(ADD, m, n), e), @(ADD, m, @(ADD, n, e)), p1),
p3 = @(AddCommLem, m, n),
p4 = @(Congr_Eq, Nat, Nat, @(ADD, m, n), @(ADD, n, m), \(z : Nat) @(ADD, z, e), p3),
p5 = @(AddAssoLem, n, m, e),
p6 = @(Tran_Eq4,
Nat,
@(ADD, m, @(ADD, n, e)),
@(ADD, @(ADD, m, n), e),
@(ADD, @(ADD, n, m), e),
@(ADD, n, @(ADD, m, e)),
p2,
p4,
p5) in
p6;

3.1.4 Identity of Addition

OO is an identity element for ADD.

dec AddUnitLLem :
!(n : Nat)
@(Equal, Nat, @(ADD, OO, n), n);

def AddUnitLLem = AddLLem0;

dec AddUnitRLem :
!(n : Nat)
@(Equal, Nat, @(ADD, n, OO), n);

def AddUnitRLem = AddRLem0;

3.1.5 Nat with ADD as a Semi-Group

def SMGProof =
\(c : Nat, a : Nat, b : Nat)
@(Symm_Eq,
Nat,
@(ADD, @(ADD, a, b), c),
@(ADD, a, @(ADD, b, c)),
@(AddAssoLem, a, b, c));

def NatSMG = @(SG_Gen, <Nat, ADD>, SMGProof);

3.1.6 Nat with ADD as a Monoi

def MOProof =
@(ANDS,

14
 @(Ass_ax, Nat, ADD),
@(Ide_ax, Nat, OO, ADD),
\(c : Nat, a : Nat, b : Nat)
@(Symm_Eq,
Nat,
@(ADD, @(ADD, a, b), c),
@(ADD, a, @(ADD, b, c)),
@(AddAssoLem, a, b, c)),
\(n : Nat)
@(ANDS,
@(Equal, Nat, @(ADD, n, OO), n),
@(Equal, Nat, @(ADD, OO, n), n),
@(AddUnitRLem, n),
@(AddUnitLLem, n)));

def NatMonoi = @(MO_Gen, <Nat, OO, ADD>, MOProof);

3.1.7 Nat with ADD as a Commutative Monoi

def CMOProof =
let P1 = @(Ass_ax, Nat, ADD),
P2 = @(Com_ax, Nat, ADD),
P3 = @(Ide_ax, Nat, OO, ADD) in
let p1 = \(c : Nat, a : Nat, b : Nat)
@(Symm_Eq,
Nat,
@(ADD, @(ADD, a, b), c),
@(ADD, a, @(ADD, b, c)),
@(AddAssoLem, a, b, c)),
p2 = AddCommLem,
p3 = \(n : Nat)
@(ANDS,
@(Equal, Nat, @(ADD, n, OO), n),
@(Equal, Nat, @(ADD, OO, n), n),
@(AddUnitRLem, n),
@(AddUnitLLem, n)) in
@(ANDS, P3, @(And, P1, P2), p3, @(ANDS, P1, P2, p1, p2));

def NatCMonoi = @(CMO_Gen, Nat, OO, ADD, CMOProof);

3.2 Multiplication
Given addition, multiplication is the function ·: N × N → N defined recursively as:

a×0 = 0
a × S(b) = a + S(a × b)

It is easy to see that 1 is the multiplicative identity:

a · 1 = a · S(0) = a + (a · 0) = a + 0 = a

Moreover, multiplication distributes over addition:

a · (b + c) = (a · b) + (a · c).

Thus, (N , +, 0, ·, 1) is a commutative semi-ring.

15
3.2.1 Basic Properties of Multiplication

0·n=0

dec TimesLLem0 :
!(n : Nat)
@(Equal, Nat, @(TIMES, OO, n), OO);

(n + 1) · m = m + (n · m)

dec TimesLLem1 :
!(m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, @(SS, n), m), @(ADD, m, @(TIMES, n, m)));

n·0=0

dec TimesRLem0 :
!(n : Nat)
@(Equal, Nat, @(TIMES, n, OO), OO);

m · (n + 1) = m + (m · n)

dec TimesRLem1 :
!(m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, m, @(SS, n)), @(ADD, m, @(TIMES, m, n)));

Proofs of TimesLLem0

def TimesLLem0 =
\(n : Nat)
@(Refl_Eq, Nat, @(TIMES, OO, n));

Proofs of TimesLLem1

dec TimesLBasLem1 :
!(n : Nat)
@(Equal, Nat, @(TIMES, @(SS, n), OO), @(ADD, OO, @(TIMES, n, OO)));

def TimesLBasLem1 =
\(n : Nat)
let p1 = @(TimesRLem0, @(SS, n)),
p2 = @(Congr_Eq,
Nat,
Nat,
@(TIMES, n, OO),
OO,
\(z : Nat) @(ADD, OO, z),

16
 @(TimesRLem0, n)),
p3 = @(Symm_Eq, Nat, @(ADD, OO, @(TIMES, n, OO)), OO, p2) in
@(Tran_Eq, Nat, @(TIMES, @(SS, n), OO), OO, @(ADD, OO, @(TIMES, n, OO)), p1, p3);

dec TimesLIndLem1 :
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(TIMES, @(SS, n), m), @(ADD, m, @(TIMES, n, m))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def TimesLIndLem1 =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(TIMES, @(SS, n), m), @(ADD, m, @(TIMES, n, m))) in
\(m : Nat, p : @(P, m), n : Nat)
let p1 = @(TimesRLem1, @(SS, n), m),
p2 = @(AddLLem1, @(TIMES, @(SS, n), m), n),
p3 = @(Congr_Eq,
Nat,
Nat,
@(TIMES, @(SS, n), m),
@(ADD, m, @(TIMES, n, m)),
\(z : Nat) @(SS, @(ADD, n, z)),
@(p, n)),
p4 = @(Tran_Eq4,
Nat,
@(TIMES, @(SS, n), @(SS, m)),
@(ADD, @(SS, n), @(TIMES, @(SS, n), m)),
@(SS, @(ADD, n, @(TIMES, @(SS, n), m))),
@(SS, @(ADD, n, @(ADD, m, @(TIMES, n, m)))),
p1,
p2,
p3),
p5 = @(AddAssComLem, n, m, @(TIMES, n, m)),
p6 = @(Congr_Eq,
Nat,
Nat,
@(ADD, n, @(ADD, m, @(TIMES, n, m))),
@(ADD, m, @(ADD, n, @(TIMES, n, m))),
SS,
p5),
p7 = @(Tran_Eq,
Nat,
@(TIMES, @(SS, n), @(SS, m)),
@(SS, @(ADD, n, @(ADD, m, @(TIMES, n, m)))),
@(SS, @(ADD, m, @(ADD, n, @(TIMES, n, m)))),
p4,
p6),
p8 = @(TimesRLem1, n, m),
p9 = @(Symm_Eq, Nat, @(TIMES, n, @(SS, m)), @(ADD, n, @(TIMES, n, m)), p8),
pA = @(Congr_Eq,
Nat,
Nat,
@(ADD, n, @(TIMES, n, m)),
@(TIMES, n, @(SS, m)),
\(z : Nat) @(SS, @(ADD, m, z)),

17
 p9),
pB = @(Tran_Eq,
Nat,
@(TIMES, @(SS, n), @(SS, m)),
@(SS, @(ADD, m, @(ADD, n, @(TIMES, n, m)))),
@(SS, @(ADD, m, @(TIMES, n, @(SS, m)))),
p7,
pA) in
pB;

def TimesLLem1 =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(TIMES, @(SS, n), m), @(ADD, m, @(TIMES, n, m))) in
@(NatInduct, P, TimesLBasLem1, TimesLIndLem1);

Proofs of TimesRLem0

dec TimesRBasLem0 : @(Equal, Nat, @(TIMES, OO, OO), OO);

def TimesRBasLem0 = @(Refl_Eq, Nat, @(TIMES, OO, OO));

dec TimesRIndLem0 :
let P = \(n : Nat)
@(Equal, Nat, @(TIMES, n, OO), OO) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

def TimesRIndLem0 =
let P = \(n : Nat)
@(Equal, Nat, @(TIMES, n, OO), OO) in
\(n : Nat)
\(p : @(P, n))
let p1 = @(TimesLLem1, OO, n),
p2 = @(Tran_Eq,
Nat,
@(TIMES, @(SS, n), OO),
@(ADD, OO, @(TIMES, n, OO)),
OO,
p1,
p) in
p2;

def TimesRLem0 =
let P = \(n : Nat)
@(Equal, Nat, @(TIMES, n, OO), OO) in
@(NatInduct, P, TimesRBasLem0, TimesRIndLem0);

Proofs of TimesRLem1

dec TimesRBasLem1 :
!(n : Nat)
@(Equal, Nat, @(TIMES, OO, @(SS, n)), @(ADD, OO, @(TIMES, OO, n)));

18
def TimesRBasLem1 =
\(n : Nat)
let p1 = @(TimesLLem0, @(SS, n)),
p2 = @(Congr_Eq,
Nat,
Nat,
@(TIMES, OO, n),
OO,
\(z : Nat) @(ADD, OO, z),
@(TimesLLem0, n)),
p3 = @(Symm_Eq, Nat, @(ADD, OO, @(TIMES, OO, n)), OO, p2) in
@(Tran_Eq, Nat, @(TIMES, OO, @(SS, n)), OO, @(ADD, OO, @(TIMES, OO, n)), p1, p3);

dec TimesRIndLem1 :
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(TIMES, m, @(SS, n)), @(ADD, m, @(TIMES, m, n))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def TimesRIndLem1 =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(TIMES, m, @(SS, n)), @(ADD, m, @(TIMES, m, n))) in
\(m : Nat, p : @(P, m), n : Nat)
let p1 = @(TimesLLem1, @(SS, n), m),
p2 = @(AddLLem1, @(TIMES, m, @(SS, n)), n),
p3 = @(Congr_Eq,
Nat,
Nat,
@(TIMES, m, @(SS, n)),
@(ADD, m, @(TIMES, m, n)),
\(z : Nat) @(SS, @(ADD, n, z)),
@(p, n)),
p4 = @(Tran_Eq4,
Nat,
@(TIMES, @(SS, m), @(SS, n)),
@(ADD, @(SS, n), @(TIMES, m, @(SS, n))),
@(SS, @(ADD, n, @(TIMES, m, @(SS, n)))),
@(SS, @(ADD, n, @(ADD, m, @(TIMES, m, n)))),
p1,
p2,
p3),
p5 = @(AddAssComLem, n, m, @(TIMES, m, n)),
p6 = @(Congr_Eq,
Nat,
Nat,
@(ADD, n, @(ADD, m, @(TIMES, m, n))),
@(ADD, m, @(ADD, n, @(TIMES, m, n))),
SS,
p5),
p7 = @(Tran_Eq,
Nat,
@(TIMES, @(SS, m), @(SS, n)),
@(SS, @(ADD, n, @(ADD, m, @(TIMES, m, n)))),
@(SS, @(ADD, m, @(ADD, n, @(TIMES, m, n)))),
p4,

19
 p6),
p8 = @(TimesLLem1, n, m),
p9 = @(Symm_Eq, Nat, @(TIMES, @(SS, m), n), @(ADD, n, @(TIMES, m, n)), p8),
pA = @(Congr_Eq,
Nat,
Nat,
@(ADD, n, @(TIMES, m, n)),
@(TIMES, @(SS, m), n),
\(z : Nat) @(SS, @(ADD, m, z)),
p9),
pB = @(Tran_Eq,
Nat,
@(TIMES, @(SS, m), @(SS, n)),
@(SS, @(ADD, m, @(ADD, n, @(TIMES, m, n)))),
@(SS, @(ADD, m, @(TIMES, @(SS, m), n))),
p7,
pA) in
pB;

def TimesRLem1 =
let P = \(m : Nat)
!(n : Nat)
@(Equal, Nat, @(TIMES, m, @(SS, n)), @(ADD, m, @(TIMES, m, n))) in
@(NatInduct, P, TimesRBasLem1, TimesRIndLem1);

3.2.2 Commutativity of Addition

dec TimesCommLem :
!(n : Nat, m : Nat)
@(Equal, Nat, @(TIMES, n, m), @(TIMES, m, n));

dec TimesCommLem1 :
!(m : Nat)
@(Equal, Nat, @(TIMES, OO, m), @(TIMES, m, OO));

def TimesCommLem1 =
\(n : Nat)
@(Tran_Eq,
Nat,
@(TIMES, OO, n),
OO,
@(TIMES, n, OO),
@(TimesLLem0, n),
@(Symm_Eq, Nat, @(TIMES, n, OO), OO, @(TimesRLem0, n)));

dec TimesCommLem2 :
let P = \(n : Nat)
!(m : Nat)
@(Equal, Nat, @(TIMES, n, m), @(TIMES, m, n)) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

def TimesCommLem2 =
let P = \(n : Nat)
!(m : Nat)

20
 @(Equal, Nat, @(TIMES, n, m), @(TIMES, m, n)) in
\(n : Nat)
\(p : @(P, n))
\(m : Nat)
@(Tran_Eq4,
Nat,
@(TIMES, @(SS, n), m),
@(ADD, m, @(TIMES, n, m)),
@(ADD, m, @(TIMES, m, n)),
@(TIMES, m, @(SS, n)),
@(TimesLLem1, m, n),
@(Congr_Eq, Nat, Nat, @(TIMES, n, m), @(TIMES, m, n), @(ADD, m), @(p, m)),
@(Symm_Eq,
Nat,
@(TIMES, m, @(SS, n)),
@(ADD, m, @(TIMES, m, n)),
@(TimesRLem1, m, n)));

def TimesCommLem =
let P = \(n : Nat)
!(m : Nat)
@(Equal, Nat, @(TIMES, n, m), @(TIMES, m, n)) in
@(NatInduct,
P,
TimesCommLem1,
TimesCommLem2)

3.2.3 Associativity of Multiplication

(a · b) · c = a · (b · c)

dec TimesAssoLem :
!(m : Nat, n : Nat, e : Nat)
@(Equal, Nat, @(TIMES, @(TIMES, m, n), e), @(TIMES, m, @(TIMES, n, e)));

dec TAssoBasLem :
!(n : Nat, e : Nat)
@(Equal, Nat, @(TIMES, @(TIMES, OO, n), e), @(TIMES, OO, @(TIMES, n, e)));

def TAssoBaseLem =
\(n : Nat, e : Nat)
@(Tran_Eq,
Nat,
@(TIMES, @(TIMES, OO, n), e),
@(TIMES, OO, e),
@(TIMES, OO, @(TIMES, n, e)),
@(Congr_Eq, Nat, Nat, @(TIMES, OO, n), OO, \(m : Nat) @(TIMES, m, e), @(TimesLLem0, n)),
@(Symm_Eq, Nat, @(TIMES, OO, @(TIMES, n, e)), OO, @(TimesLLem0, @(TIMES, n, e))));

dec TAssoIndLem :
let P = \(m : Nat)
!(n : Nat, e : Nat)
@(Equal, Nat, @(TIMES, @(TIMES, m, n), e), @(TIMES, m, @(TIMES, n, e))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

21
def TAssoIndLem =
let P = \(m : Nat)
!(n : Nat, e : Nat)
@(Equal, Nat, @(TIMES, @(TIMES, m, n), e), @(TIMES, m, @(TIMES, n, e))) in
\(m : Nat, p : @(P, m), n : Nat, e : Nat)
let u1 = @(TimesLLem1, n, m),
u2 = @(Congr_Eq,
Nat,
Nat,
@(TIMES, @(SS, m), n),
@(ADD, n, @(TIMES, m, n)),
\(z : Nat) @(TIMES, z, e),
u1),
u3 = @(DistrRLem, e, n, @(TIMES, m, n)),
u4 = @(Tran_Eq,
Nat,
@(TIMES, @(TIMES, @(SS, m), n), e),
@(TIMES, @(ADD, n, @(TIMES, m, n)), e),
@(ADD, @(TIMES, n, e), @(TIMES, @(TIMES, m, n), e)),
u2,
u3),
u5 = @(AddCommLem, @(TIMES, n, e), @(TIMES, @(TIMES, m, n), e)),
u6 = @(Tran_Eq,
Nat,
@(TIMES, @(TIMES, @(SS, m), n), e),
@(ADD, @(TIMES, n, e), @(TIMES, @(TIMES, m, n), e)),
@(ADD, @(TIMES, @(TIMES, m, n), e), @(TIMES, n, e)),
u4,
u5) in
let Q = \(z : Nat)
@(Equal,
Nat,
@(ADD, @(TIMES, @(TIMES, m, n), e), @(TIMES, n, e)),
@(ADD, z, @(TIMES, n, e))) in
let u7 = @(p,
n,
e,
Q,
@(Refl_Eq, Nat, @(ADD, @(TIMES, @(TIMES, m, n), e), @(TIMES, n, e)))),
u8 = @(Tran_Eq,
Nat,
@(TIMES, @(TIMES, @(SS, m), n), e),
@(ADD, @(TIMES, @(TIMES, m, n), e), @(TIMES, n, e)),
@(ADD, @(TIMES, m, @(TIMES, n, e)), @(TIMES, n, e)),
u6,
u7),
u9 = @(AddCommLem, @(TIMES, m, @(TIMES, n, e)), @(TIMES, n, e)),
uA = @(Tran_Eq,
Nat,
@(TIMES, @(TIMES, @(SS, m), n), e),
@(ADD, @(TIMES, m, @(TIMES, n, e)), @(TIMES, n, e)),
@(ADD, @(TIMES, n, e), @(TIMES, m, @(TIMES, n, e))),
u8,
u9) in
uA;

22
 def TimesAssoLem =
let P = \(m : Nat)
!(n : Nat, e : Nat)
@(Equal,
Nat,
@(TIMES, @(TIMES, m, n), e),
@(TIMES, m, @(TIMES, n, e))) in
@(NatInduct, P, TAssoBasLem, TAssoIndLem);

3.2.4 Identity of Multiplication

@(SS, OO) is an identity element for TIMES.

dec TimesUnitLLem :
!(n : Nat)
@(Equal, Nat, @(TIMES, @(SS, OO), n), n);

def TimesUnitLLem =
\(n : Nat)
let p = @(TimesLLem1, n, OO) in
let q = @(AddCommLem, n, OO) in
@(Tran_Eq,
Nat,
@(TIMES, @(SS, OO), n),
@(ADD, n, @(TIMES, OO, n)),
n,
p,
q);

dec TimesUnitRLem :
!(n : Nat)
@(Equal, Nat, @(TIMES, n, @(SS, OO)), n);

def TimesUnitRLem =
\(n : Nat)
let p1 = @(TimesCommLem, n, @(SS, OO)),
p2 = @(TimesUnitLLem, n) in
@(Tran_Eq,
Nat,
@(TIMES, n, @(SS, OO)),
@(TIMES, @(SS, OO), n),
n,
p1,
p2);

3.2.5 Distribution of Multiplication over Addition

l · (m + n) = (l · m) + (l · n)

dec DistrLLem :
!(l : Nat, m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, l, @(ADD, m, n)), @(ADD, @(TIMES, l, m), @(TIMES, l, n)));

dec DistrLLem1 :
!(m : Nat, n : Nat)

23
 @(Equal, Nat, @(TIMES, OO, @(ADD, m, n)), @(ADD, @(TIMES, OO, m), @(TIMES, OO, n)));

def DistrLLem1 =
\(m : Nat, n : Nat)
let p1 = @(Refl_Eq, Nat, @(TIMES, OO, @(ADD, m, n))),
p2 = @(Refl_Eq, Nat, @(ADD, @(TIMES, OO, m), @(TIMES, OO, n))) in
@(Tran_Eq,
Nat, @(TIMES, OO, @(ADD, m, n)), OO, @(ADD, @(TIMES, OO, m), @(TIMES, OO, n)), p1, p2);

dec DistrLLem2 :
let P = \(l : Nat)
!(m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, l, @(ADD, m, n)), @(ADD, @(TIMES, l, m), @(TIMES, l, n))) in
!(l : Nat)
[@(P, l) -> @(P, @(SS, l))];

dec AddTimesDistLem1 :
!(l : Nat, m : Nat, n : Nat)
@(Equal,
Nat,
@(ADD, @(ADD, m, n), @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
@(ADD, @(ADD, m, @(TIMES, l, m)), @(ADD, n, @(TIMES, l, n))));

def AddTimesDistLem1 =
\(l : Nat, m : Nat, n : Nat)
let p1 = @(AddAssoLem, m, n, @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
p2 = @(AddAssoLem, n, @(TIMES, l, m), @(TIMES, l, n)),
p3 = @(Symm_Eq,
Nat,
@(ADD, @(ADD, n, @(TIMES, l, m)), @(TIMES, l, n)),
@(ADD, n, @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
p2),
p4 = @(Congr_Eq,
Nat,
Nat,
@(ADD, n, @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
@(ADD, @(ADD, n, @(TIMES, l, m)), @(TIMES, l, n)),
\(z : Nat)
@(ADD, m, z),
p3),
p5 = @(Tran_Eq,
Nat,
@(ADD, @(ADD, m, n), @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
@(ADD, m, @(ADD, n, @(ADD, @(TIMES, l, m), @(TIMES, l, n)))),
@(ADD, m, @(ADD, @(ADD, n, @(TIMES, l, m)), @(TIMES, l, n))),
p1,
p4),
p6 = @(AddCommLem, n, @(TIMES, l, m)),
p7 = @(Congr_Eq,
Nat,
Nat,
@(ADD, n, @(TIMES, l, m)),
@(ADD, @(TIMES, l, m), n),
\(z : Nat) @(ADD, z, @(TIMES, l, n)),
p6),
p8 = @(Congr_Eq,
Nat,

24
 Nat,
@(ADD, @(ADD, n, @(TIMES, l, m)), @(TIMES, l, n)),
@(ADD, @(ADD, @(TIMES, l, m), n), @(TIMES, l, n)),
\(z : Nat) @(ADD, m, z),
p7),
p9 = @(AddAssoLem, @(TIMES, l, m), n, @(TIMES, l, n)),
pA = @(Congr_Eq,
Nat,
Nat,
@(ADD, @(ADD, @(TIMES, l, m), n), @(TIMES, l, n)),
@(ADD, @(TIMES, l, m), @(ADD, n, @(TIMES, l, n))),
\(z : Nat) @(ADD, m, z),
p9),
pB = @(Tran_Eq4,
Nat,
@(ADD, @(ADD, m, n), @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
@(ADD, m, @(ADD, @(ADD, n, @(TIMES, l, m)), @(TIMES, l, n))),
@(ADD, m, @(ADD, @(ADD, @(TIMES, l, m), n), @(TIMES, l, n))),
@(ADD, m, @(ADD, @(TIMES, l, m), @(ADD, n, @(TIMES, l, n)))),
p5,
p8,
pA),
pC = @(AddAssoLem, m, @(TIMES, l, m), @(ADD, n, @(TIMES, l, n))),
pD = @(Symm_Eq,
Nat,
@(ADD, @(ADD, m, @(TIMES, l, m)), @(ADD, n, @(TIMES, l, n))),
@(ADD, m, @(ADD, @(TIMES, l, m), @(ADD, n, @(TIMES, l, n)))),
pC),
pE = @(Tran_Eq,
Nat,
@(ADD, @(ADD, m, n), @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
@(ADD, m, @(ADD, @(TIMES, l, m), @(ADD, n, @(TIMES, l, n)))),
@(ADD, @(ADD, m, @(TIMES, l, m)), @(ADD, n, @(TIMES, l, n))),
pB,
pD) in
pE;

dec AddTimesDistLem2 :
!(l : Nat, m : Nat, n : Nat)
@(Equal,
Nat,
@(ADD, @(ADD, m, @(TIMES, l, m)), @(ADD, n, @(TIMES, l, n))),
@(ADD, @(TIMES, @(SS, l), m), @(TIMES, @(SS, l), n)));

dec AddEqLem :
!(a1 : Nat, b1 : Nat, a2 : Nat, b2 : Nat)
[@(Equal, Nat, a1, b1) ->
@(Equal, Nat, a2, b2) ->
@(Equal, Nat, @(ADD, a1, a2), @(ADD, b1, b2))];

def AddEqLem =
\(a1 : Nat, b1 : Nat, a2 : Nat, b2 : Nat)
\(p1 : @(Equal, Nat, a1, b1),
p2 : @(Equal, Nat, a2, b2))
let Q = \(z : Nat)
@(Equal, Nat, @(ADD, a1, a2), @(ADD, z, a2)) in
let q = @(p1, Q, @(Refl_Eq, Nat, @(ADD, a1, a2))) in

25
 let P = \(z : Nat)
@(Equal, Nat, @(ADD, a1, a2), @(ADD, b1, z)) in
@(p2, P, q);

def AddTimesDistLem2 =
\(l : Nat, m : Nat, n : Nat)
let p1 = @(TimesLLem1, m, l),
p2 = @(TimesLLem1, n, l),
p3 = @(Symm_Eq, Nat, @(TIMES, @(SS, l), m), @(ADD, m, @(TIMES, l, m)), p1),
p4 = @(Symm_Eq, Nat, @(TIMES, @(SS, l), n), @(ADD, n, @(TIMES, l, n)), p2) in
@(AddEqLem,
@(ADD, m, @(TIMES, l, m)),
@(TIMES, @(SS, l), m),
@(ADD, n, @(TIMES, l, n)),
@(TIMES, @(SS, l), n),
p3,
p4);

def DistrLLem2 =
let P = \(l : Nat)
!(m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, l, @(ADD, m, n)), @(ADD, @(TIMES, l, m), @(TIMES, l, n))) in
\(l : Nat, p : @(P, l), m : Nat, n : Nat)
let p1 = @(TimesLLem1, @(ADD, m, n), l) in
let Q = \(z : Nat)
@(Equal,
Nat,
@(ADD, @(ADD, m, n), @(TIMES, l, @(ADD, m, n))),
@(ADD, @(ADD, m, n), z)) in
let p2 = @(p, m, n, Q, @(Refl_Eq, Nat, @(ADD, @(ADD, m, n), @(TIMES, l, @(ADD, m, n))))),
p3 = @(Tran_Eq,
Nat,
@(TIMES, @(SS, l), @(ADD, m, n)),
@(ADD, @(ADD, m, n), @(TIMES, l, @(ADD, m, n))),
@(ADD, @(ADD, m, n), @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
p1,
p2),
p4 = @(AddTimesDistLem1, l, m, n),
p5 = @(AddTimesDistLem2, l, m, n),
p6 = @(Tran_Eq4,
Nat,
@(TIMES, @(SS, l), @(ADD, m, n)),
@(ADD, @(ADD, m, n), @(ADD, @(TIMES, l, m), @(TIMES, l, n))),
@(ADD, @(ADD, m, @(TIMES, l, m)), @(ADD, n, @(TIMES, l, n))),
@(ADD, @(TIMES, @(SS, l), m), @(TIMES, @(SS, l), n)),
p3,
p4,
p5) in
p6;

def DistrLLem =
let P = \(l : Nat)
!(m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, l, @(ADD, m, n)), @(ADD, @(TIMES, l, m), @(TIMES, l, n))) in
@(NatInduct,
P,
DistrLLem1,

26
 DistrLLem2);

(m + n) · l = (m · l) + (n · l)

dec DistrRLem :
!(l : Nat, m : Nat, n : Nat)
@(Equal, Nat, @(TIMES, @(ADD, m, n), l), @(ADD, @(TIMES, m, l), @(TIMES, n, l)));

dec AddLREqLem :
!(a1 : Nat, b1 : Nat, a2 : Nat, b2 : Nat)
[@(Equal, Nat, a1, a2) ->
@(Equal, Nat, b1, b2) ->
@(Equal, Nat, @(ADD, a1, b1), @(ADD, a2, b2))];

def AddLREqLem =
\(a1 : Nat, b1 : Nat, a2 : Nat, b2 : Nat)
\(p1 : @(Equal, Nat, a1, a2),
p2 : @(Equal, Nat, b1, b2))
let Q1 = \(a : Nat)
!(b : Nat)
@(Equal, Nat, @(ADD, a1, b), @(ADD, a, b)) in
let q = @(p1, Q1, \(b : Nat) @(Refl_Eq, Nat, @(ADD, a1, b))) in
let Q2 = \(b : Nat)
@(Equal, Nat, @(ADD, a1, b1), @(ADD, a2, b)) in
@(p2, Q2, @(q, b1));

def DistrRLem =
\(l : Nat, m : Nat, n : Nat)
let p = @(DistrLLem, l, m, n) in
let q1 = @(TimesCommLem, @(ADD, m, n), l),
q2 = @(Tran_Eq,
Nat,
@(TIMES, @(ADD, m, n), l),
@(TIMES, l, @(ADD, m, n)),
@(ADD, @(TIMES, l, m), @(TIMES, l, n)),
q1,
p),
q3 = @(TimesCommLem, l, m),
q4 = @(TimesCommLem, l, n),
q5 = @(AddLREqLem,
@(TIMES, l, m),
@(TIMES, l, n),
@(TIMES, m, l),
@(TIMES, n, l),
q3,
q4) in
@(Tran_Eq,
Nat,
@(TIMES, @(ADD, m, n), l),
@(ADD, @(TIMES, l, m), @(TIMES, l, n)),
@(ADD, @(TIMES, m, l), @(TIMES, n, l)),
q2,
q5);

27
3.2.6 Nat with TIMES as a Monoi

def TMOProof =
@(ANDS,
@(Ass_ax, Nat, TIMES),
@(Ide_ax, Nat, II, TIMES),
\(c : Nat, a : Nat, b : Nat)
@(Symm_Eq,
Nat,
@(TIMES, @(TIMES, a, b), c),
@(TIMES, a, @(TIMES, b, c)),
@(TimesAssoLem, a, b, c)),
\(n : Nat)
@(ANDS,
@(Equal, Nat, @(TIMES, n, II), n),
@(Equal, Nat, @(TIMES, II, n), n),
@(TimesUnitRLem, n),
@(TimesUnitLLem, n)));

def NatTimesMonoi = @(MO_Gen, <Nat, II, TIMES>, TMOProof);

3.2.7 Nat with ADD and TIMES as a Semi-Ring

def SMRProof =
let P1 = @(Ax_CMO, Nat, OO, ADD),
P2 = @(Ax_MO2, Nat, II, TIMES),
P3 = @(Dis_ax, Nat, ADD, TIMES),
P4 = @(Zero_ax, Nat, OO, TIMES) in
let p1 = CMOProof,
p2 = TMOProof,
p3 = \(a : Nat, b : Nat, c : Nat)
let P1 = @(Equal,
Nat,
@(TIMES, a, @(ADD, b, c)),
@(ADD, @(TIMES, a, b), @(TIMES, a, c))),
P2 = @(Equal,
Nat,
@(TIMES, @(ADD, a, b), c),
@(ADD, @(TIMES, a, c), @(TIMES, b, c))) in
let p1 = @(DistrLLem, a, b, c),
p2 = @(DistrRLem, c, a, b) in
@(ANDS, P1, P2, p1, p2),
p4 = \(n : Nat)
@(ANDS,
@(Equal, Nat, @(TIMES, OO, n), OO),
@(Equal, Nat, @(TIMES, n, OO), OO),
@(TimesLLem0, n),
@(TimesRLem0, n)) in
@(ANDS,
P1,
@(And, P2, @(And, P3, P4)),
p1,
@(ANDS,
P2,
@(And, P3, P4),

28
 p2,
@(ANDS, P3, P4, p3, p4)));

def NatSemiRing = @(SMRingGen, <Nat, OO, II, ADD, TIMES>, SMRProof);

3.3 Equality
Two natural numbers are equal if and only if they are exactly the same in every way. This defines a binary relation,
equality, marked by the sign of equality “=” in such a way that the statement “x = y ′′ means that x and y are equal.

3.3.1 Equality Defined as Reflexive Relation

3.3.2 Definition of NatEq

def NatEq =
\(n : Nat, m : Nat)
!(T : [Nat -> Nat -> Prop])
[!(n : Nat) @(T, n, n) -> @(T, n, m)];

3.3.3 Production Rule of NatEq

dec NatEqN : !(n : Nat) @(NatEq, n, n);

def NatEqN =
\(n : Nat)
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n))
@(x, n);

3.3.4 Induction Rule of NatEq

dec NatEqInduct :
!(x : Nat, P : [Nat -> Prop])
[@(P, x) ->
!(y : Nat)
[@(NatEq, y, x) -> @(P, y)]];

def NatEqInduct =
\(x : Nat, P : [Nat -> Prop])
\(p : @(P, x))
\(y : Nat)
\(q : @(NatEq, y, x))
let T = \(a : Nat, b : Nat)
[@(P, b) -> @(P, a)] in
let u = @(q,
T,
\(a : Nat, r : @(P, a)) r) in
@(u, p);

29
3.3.5 Equivalence Properties
Reflexive Property of NatEq

dec NatEqReflLem : !(n : Nat) @(NatEq, n, n);

def NatEqReflLem = NatEqN;

Symmetrical Property of NatEq

dec NatEqSymmLem :
!(x : Nat, y : Nat)
[@(NatEq, x, y) -> @(NatEq, y, x)];

def NatEqSymmLem =
\(x : Nat, y : Nat)
\(H : @(NatEq, x, y))
let P = \(z : Nat)
@(NatEq, y, z) in
@(NatEqInduct,
y,
P,
@(NatEqReflLem, y),
x,
H);

Transitivity Property of NatEq

dec NatEqTranLem :
!(x : Nat, y : Nat, z : Nat)
[@(NatEq, x, y) -> @(NatEq, y, z) -> @(NatEq, x, z)];

def NatEqTranLem =
\(x : Nat, y : Nat, z : Nat)
\(H1 : @(NatEq, x, y), H2 : @(NatEq, y, z))
let P = \(w : Nat)
@(And, @(NatEq, x, w), @(NatEq, w, z)) in
let u = @(NatEqInduct,
y,
P,
@(ANDS, @(NatEq, x, y), @(NatEq, y, z), H1, H2),
z,
@(NatEqSymmLem, y, z, H2)) in
@(PJ1, @(NatEq, x, z), @(NatEq, z, z), u);

3.3.6 Successor Lemma for NatEq

NatEqSuccLem is inhabited. However, I don’t know why it has to be used as a definition in COQ.

dec NatEqSuccLem :
!(n : Nat, m : Nat)
[@(NatEq, n, m) -> @(NatEq, @(SS, n), @(SS, m))];

30
 def NatEqSuccLem =
\(n : Nat, m : Nat)
\(H : @(NatEq, n, m))
let P = \(z : Nat) @(NatEq, @(SS, n), @(SS, z)) in
@(NatEqInduct,
n,
P,
@(NatEqReflLem, @(SS, n)),
m,
@(NatEqSymmLem, n, m, H));

3.3.7 Function Application Lemma for NatEq

dec NatEqFunLem :
!(f : [Nat -> Nat])
!(x : Nat, y : Nat)
[@(NatEq, x, y) -> @(NatEq, @(f, x), @(f, y))];

def NatEqFunLem =
\(f : [Nat -> Nat])
\(x : Nat, y : Nat)
\(H : @(NatEq, x, y))
let P = \(z : Nat)
@(NatEq, @(f, x), @(f, z)) in
@(NatEqInduct,
x,
P,
@(NatEqReflLem, @(f, x)),
y,
@(NatEqSymmLem, x, y, H));

3.3.8 Equality Negation Lemma for NatEq

dec NegNatEqLem :
!(x : Nat, y : Nat)
[@(Neg, @(NatEq, x, y)) -> @(Neg, @(NatEq, y, x))];

def NegNatEqLem =
\(x : Nat, y : Nat)
\(H : @(Neg, @(NatEq, x, y)))
\(p : @(NatEq, y, x))
@(H, @(NatEqSymmLem, y, x, p));

3.3.9 Successor Lemma for @(Equal, Nat)

dec EqNatSuccLem :
!(n : Nat, m : Nat)
[@(Equal, Nat, n, m) -> @(Equal, Nat, @(SS, n), @(SS, m))];

def EqNatSuccLem =

31
 \(n : Nat, m : Nat)
\(h : @(Equal, Nat, n, m))
let P = \(z : Nat)
@(Equal, Nat, @(SS, n), @(SS, z)) in
@(h, P, @(Refl_Eq, Nat, @(SS, n)));

3.3.10 Equivalence of NatEq and @(Equal, Nat)

dec NatEq2EqNatLem :
!(n : Nat, m : Nat)
[@(NatEq, n, m) -> @(Equal, Nat, n, m)];

def NatEq2EqNatLem =
\(n : Nat, m : Nat)
\(h : @(NatEq, n, m))
@(h, @(Equal, Nat), @(Refl_Eq, Nat));

dec EqNat2NatEqLem :
!(n : Nat, m : Nat)
[@(Equal, Nat, n, m) -> @(NatEq, n, m)];

def EqNat2NatEqLem =
\(n : Nat, m : Nat)
\(h : @(Equal, Nat, n, m))
let P = \(z : Nat) @(NatEq, n, z) in
@(h, P, @(NatEqReflLem, n));

3.4 Inequalities ≤
The usual total order relation ≤: N × N can be defined as follows, assuming 0 is a natural number: For all a, b ∈ N , a ≤ b
if and only if there exists some c ∈ N such that a + c = b.
This relation is stable under addition and multiplication: for, if a ≤ b, then:

a + c ≤ b + c,

and
a · c ≤ b · c.
Thus, the structure (N , +, ·, 1, 0, ≤) is an ordered semi-ring; because there is no natural number between 0 and 1, it is a
discrete ordered semi-ring. The axiom of induction is sometimes stated in the following strong form, making use of the ≤
order:
For any predicate ϕ, if
• ϕ(0) is true, and
• for every n, k ∈ N , if k ≤ n implies ϕ(k) is true, then ϕ(S(n)) is true,
then for every n ∈ N , ϕ(n) is true.
This form of the induction axiom is a simple consequence of the standard formulation, but is often better suited for
reasoning about the ≤ order. For example, to show that the naturals are well-orderedevery nonempty subset of N has a
least elementone can reason as follows.
Let a nonempty X ⊆ N be given and assume X has no least element.
• Because 0 is the least element of N , it must be that 0 ̸∈ X.
• For any n ∈ N , suppose for every k ≤ n, k ̸∈ X. Then S(n) ̸∈ X, for otherwise it would be the least element of X.
Thus, by the strong induction principle, for every n ∈ N , n ̸∈ X. Thus, X ∩ N = ∅, which contradicts X being a nonempty
subset of N . Thus X has a least element.

32
3.4.1 Inequality Defined as a Reflexive Relation
3.4.2 Inductive Definition of NatLe

def NatLe =
\(n : Nat, m : Nat)
!(T : [Nat -> Nat -> Prop])
[!(n : Nat) @(T, n, n) ->
!(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))] ->
@(T, n, m)];

3.4.3 Production Rules of NatLe

dec NatLeN : !(n : Nat) @(NatLe, n, n);

def NatLeN =
\(n : Nat)
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(x, n);

dec NatLeS :
!(n : Nat, m : Nat)
[@(NatLe, n, m) -> @(NatLe, n, @(SS, m))];

def NatLeS =
\(n : Nat, m : Nat, p : @(NatLe, n, m))
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, n, m, @(p, T, x, y));

3.4.4 Conditions for NatLe

For all a, b ∈ N , a ≤ b if and only if there exists some c ∈ N such that a + c = b.

def NatLeCond1 =
\(n : Nat, m : Nat)
[@(NatLe, n, m) ->
?(d : Nat)
@(Equal, Nat, m, @(ADD, n, d))];

def MkNatLeCond1 =
\(n : Nat, m : Nat)
\(H : @(NatLe, n, m))
\(d : Nat,
p : @(Equal, Nat, m, @(ADD, n, d)))
<d, p>;

def NatLeCond2 =
\(n : Nat, m : Nat)

33
 [?(d : Nat)
@(Equal, Nat, m, @(ADD, n, d)) ->
@(NatLe, n, m)];

def NatLeCond =
\(n : Nat, m : Nat)
@(And, @(NatLeCond1, n, m), @(NatLeCond2, n, m));

dec NatLeCondLem :
!(n : Nat, m : Nat)
@(NatLeCond, n, m);

dec NatLeCondLem1 :
!(n : Nat, m : Nat)
@(NatLeCond1, n, m);

dec NatLeCondLem11 :
!(m : Nat)
@(NatLeCond1, OO, m);

dec NatLeCondLem110 :
!(m : Nat)
[@(NatLe, OO, m) ->
let d = m in
@(Equal, Nat, m, @(ADD, OO, d))];

def NatLeCondLem110 =
\(m : Nat)
\(h : @(NatLe, OO, m))
let d = m in
@(Refl_Eq, Nat, @(ADD, OO, d));

def NatLeCondLem11 =
\(m : Nat)
\(H : @(NatLe, OO, m))
let d = m in
let q = @(NatLeCondLem110, m, H) in
@(MkNatLeCond1, OO, m, H, d, q);

dec NatLeCondLem12 :
let P = \(n : Nat) !(m : Nat) @(NatLeCond1, n, m) in
!(n : Nat) [@(P, n) -> @(P, @(SS, n))];

dec NatLeSSLeLem :
!(n : Nat, m : Nat)
[@(NatLe, @(SS, n), m) -> @(NatLe, n, m)];

dec SnNatLeNegEq0Lem :
!(n : Nat, m : Nat, d : Nat)
[@(NatLe, @(SS, n), m) ->
@(Equal, Nat, m, @(ADD, n, d)) ->
@(Neg, @(Equal, Nat, d, OO))];

dec NatAddSSPPEqLem :
!(n : Nat, d : Nat)
[@(Neg, @(Equal, Nat, d, OO)) -> @(Equal, Nat, @(ADD, n, d), @(ADD, @(SS, n), @(PP, d)))];

34
dec NatLeCondLem120 :
let P = \(n : Nat) !(m : Nat) @(NatLeCond1, n, m) in
!(n : Nat)
!(h : @(P, n))
!(m : Nat)
!(p : @(NatLe, @(SS, n), m))
let q = @(h, m, @(NatLeSSLeLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let ds = @(PP, d) in
@(Equal, Nat, m, @(ADD, @(SS, n), ds));

def NatLtCondLem120 =
let P = \(n : Nat) !(m : Nat) @(NatLeCond1, n, m) in
\(n : Nat)
\(h : @(P, n))
\(m : Nat)
\(p : @(NatLe, @(SS, n), m))
let q = @(h, m, @(NatLeSSLeLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let ds = @(PP, d) in
let Q = \(z : Nat) @(Equal, Nat, m, z) in
let u0 = @(SnNatLeNegEq0Lem, n, m, d, p, r),
u1 = @(NatAddSSPPEqLem, n, d, u0) in
@(u1, Q, r);

def NatLtCondLem12 =
let P = \(n : Nat) !(m : Nat) @(NatLeCond1, n, m) in
\(n : Nat)
\(h : @(P, n))
\(m : Nat)
\(p : @(NatLe, @(SS, n), m))
let q = @(h, m, @(NatLeSSLeLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let ds = @(PP, d) in
let u = @(NatLeCondLem120, n, h, m, p) in
@(MkNatLeCond1, @(SS, n), m, p, ds, u);

def NatLeCondLem1 =
let P = \(n : Nat) !(m : Nat) @(NatLeCond1, n, m) in
@(NatInduct0,
P,
NatLeCondLem11,
NatLeCondLem12);

dec NatLeCondLem2 :
!(n : Nat, m : Nat)
@(NatLeCond2, n, m);

dec nNatLeAddnLem :
!(n : Nat, d : Nat)
@(NatLe, n, @(ADD, n, d));

def NatLeCondLem2 =
\(n : Nat, m : Nat)
\(p : ?(d : Nat)
@(Equal, Nat, m, @(ADD, n, d)))
let d = @(FST, p), q = @(SND, p) in

35
 let P = \(z : Nat)
@(NatLe, n, z) in
let r = @(Symm_Eq, Nat, m, @(ADD, n, d), q) in
@(r, P, @(nNatLeAddnLem, n, d));

def NatLeCondLem =
\(n : Nat, m : Nat)
let P1 = @(NatLeCond1, n, m),
P2 = @(NatLeCond2, n, m) in
let p1 = @(NatLeCondLem1, n, m),
p2 = @(NatLeCondLem2, n, m) in
@(ANDS, P1, P2, p1, p2);

3.4.5 Induction Rule of NatLe

NatLeInduct is interpreted as follows: assume that P be a set and y is in P, if for every x, x ≤ y then x is in P.

dec NatLeInduct :
!(y : Nat, P : [Nat -> Prop])
[@(P, y) ->
!(x : Nat)
[@(NatLe, x, y) -> @(P, x)]];

def NatLeInduct =
\(*y : Nat, P : [Nat -> Prop])
\(h : @(P, *y))
\(x : Nat)
\(p : @(NatLe, x, *y))
h;

def NatLeInduct =
\(y : Nat, P : [Nat -> Prop])
\(p : @(P, y))
\(x : Nat)
\(q : @(NatLe, x, y))
let T = \(a : Nat, b : Nat)
[@(P, b) -> @(P, a)] in
let u = @(q,
T,
\(a : Nat, p : @(P, a))
p,
\(a : Nat, *b : Nat, h1 : @(T, a, *b), h2 : @(P, @(SS, *b)))
@(h1, h2)) in
@(u, p);

3.4.6 Reflexive and Transitive Property NatLe

Reflexivity of NatLe

n≤n

dec NatLeReflLem : !(n : Nat) @(NatLe, n, n);

def NatLeReflLem = NatLeN;

36
Successor Lemma of NatLe

n ≤ m → n ≤ S(m)

dec NatLeSuccLem :
!(n : Nat, m : Nat)
[@(NatLe, n, m) -> @(NatLe, n, @(SS, m))];

def NatLeSuccLem = NatLeS;

Transitivity of NatLe

n≤m∧m≤l →n≤l

dec NatLeTranLem :
!(n : Nat, m : Nat, l : Nat)
[@(NatLe, n, m) -> @(NatLe, m, l) -> @(NatLe, n, l)];

dec NatLeTranCondLem :
!(n : Nat, m : Nat, l : Nat)
!(d1 : Nat, d2 : Nat)
[@(Equal, Nat, m, @(ADD, n, d1)) ->
@(Equal, Nat, l, @(ADD, m, d2)) ->
let d = @(ADD, d1, d2) in
@(Equal, Nat, l, @(ADD, n, d))];

dec NatLeTrCondLem2 :
!(n : Nat, m : Nat, l : Nat)
!(d1 : Nat, d2 : Nat)
[@(Equal, Nat, m, @(ADD, n, d1)) ->
@(Equal, Nat, l, @(ADD, m, d2)) ->
let d = @(ADD, d1, d2) in
@(Equal, Nat, l, @(ADD, n, d))];

dec NatAddAssLem :
!(n : Nat, d1 : Nat, d2 : Nat)
@(Equal,
Nat,
@(ADD, @(ADD, n, d1), d2),
@(ADD, n, @(ADD, d1, d2)));

def NatLeTrCondLem2 =
\(n : Nat, m : Nat, l : Nat)
\(d1 : Nat, d2 : Nat)
\(h1 : @(Equal, Nat, m, @(ADD, n, d1)),
h2 : @(Equal, Nat, l, @(ADD, m, d2)))
let d = @(ADD, d1, d2) in
let Q = \(z : Nat) @(Equal, Nat, l, @(ADD, z, d2)) in
let q = @(h1, Q, h2) in
let R = \(z : Nat) @(Equal, Nat, l, z) in
let r = @(NatAddAssLem, n, d1, d2) in
@(r, R, q);

def NatLeTranCondLem =

37
 \(n : Nat, m : Nat, l : Nat)
\(d1 : Nat, d2 : Nat)
\(p2 : @(Equal, Nat, m, @(ADD, n, d1)),
q2 : @(Equal, Nat, l, @(ADD, m, d2)))
let d = @(ADD, d1, d2) in
@(NatLeTrCondLem2, n, m, l, d1, d2, p2, q2);

def NatLeTranLem =
\(n : Nat, m : Nat, l : Nat)
\(h1 : @(NatLe, n, m), h2 : @(NatLe, m, l))
let p1 = @(NatLeCondLem1, n, m, h1),
p2 = @(NatLeCondLem1, m, l, h2) in
let d1 = @(FST, p1), q1 = @(SND, p1),
d2 = @(FST, p2), q2 = @(SND, p2) in
let d = @(ADD, d1, d2),
q = @(NatLeTranCondLem, n, m, l, d1, d2, q1, q2) in
@(NatLeCondLem2, n, l, <d, q>);

3.4.7 Other Properties of NatLe

Predecessor Lemma of NatLe

S(n) ≤ S(m) → n ≤ m

dec NatLePredLem :
!(n : Nat, m : Nat)
[@(NatLe, @(SS, n), @(SS, m)) -> @(NatLe, n, m)];

dec EqNatSSAddLem :
!(n : Nat, m : Nat, d : Nat)
[@(Equal, Nat, @(SS, m), @(ADD, @(SS, n), d)) ->
@(Equal, Nat, @(SS, m), @(SS, @(ADD, n, d)))];

def NatLePredLem =
\(n : Nat, m : Nat)
\(H : @(NatLe, @(SS, n), @(SS, m)))
let p = @(NatLeCondLem1, @(SS, n), @(SS, m), H) in
let d = @(FST, p), q = @(SND, p) in
let u1 = @(EqNatSSAddLem, n, m, d, q),
u2 = @(EqNat2NatEqLem, @(SS, m), @(SS, @(ADD, n, d)), u1),
u3 = @(NatEqFunLem, PP, @(SS, m), @(SS, @(ADD, n, d)), u2),
u4 = @(NatEq2EqNatLem, m, @(ADD, n, d), u3) in
@(NatLeCondLem2, n, m, <d, u4>);

Double Successor Lemma of NatLe

n ≤ m → S(n) ≤ S(m)

dec NatLeSuccSuccLem :
!(n : Nat, m : Nat)
[@(NatLe, n, m) -> @(NatLe, @(SS, n), @(SS, m))];

dec EqNatAddSSLem :

38
 !(n : Nat, m : Nat, d : Nat)
[@(Equal, Nat, m, @(ADD, n, d)) -> @(Equal, Nat, @(SS, m), @(ADD, @(SS, n), d))];

def EqNatAddSSLem =
\(n : Nat, m : Nat, d : Nat)
\(h : @(Equal, Nat, m, @(ADD, n, d)))
let P = \(z : Nat)
@(Equal, Nat, @(SS, m), @(SS, z)) in
let p1 = @(h, P, @(Refl_Eq, Nat, @(SS, m))),
p2 = @(AddLLem1, d, n),
p3 = @(Symm_Eq, Nat, @(ADD, @(SS, n), d), @(SS, @(ADD, n, d)), p2) in
@(Tran_Eq, Nat, @(SS, m), @(SS, @(ADD, n, d)), @(ADD, @(SS, n), d), p1, p3);

def NatLeSuccSuccLem =
\(n : Nat, m : Nat)
\(H : @(NatLe, n, m))
let p = @(NatLeCondLem1, n, m, H) in
let d = @(FST, p), q = @(SND, p) in
let u = @(EqNatAddSSLem, n, m, d, q) in
@(NatLeCondLem2, @(SS, n), @(SS, m), <d, u>);

¬(S(n) ≤ 0)
There is no production rules for @(NatLe, @(SS, m), OO) for any natural number m. It has the type Null. We treat this
as an axiom instead.

dec NatLeSnOAxm :
!(m : Nat)
@(Equal, Prop, @(NatLe, @(SS, m), OO), Null);

dec NatLeSnOLem :
!(m : Nat)
[@(NatLe, @(SS, m), OO) -> Null];

def NatLeSnOLem =
\(m : Nat)
\(H : @(NatLe, @(SS, m), OO))
let P = \(Z : Prop) Z in
@(NatLeSnOAxm, m, P, H);

dec NatLeSnmLem :
!(m : Nat)
[@(NatLe, @(SS, m), m) -> Null];

dec NatLeSnmLem1 :
[@(NatLe, @(SS, OO), OO) -> Null];

def NatLeSnmLem1 = @(NatLeSnOLem, OO);

dec NatLeSnmLem2 :
let P = \(m : Nat)
[@(NatLe, @(SS, m), m) -> Null] in
!(n : Nat) [@(P, n) -> @(P, @(SS, n))];

def NatLeSnmLem2 =
let P = \(m : Nat)

39
 [@(NatLe, @(SS, m), m) -> Null] in
\(m : Nat, h : @(P, m))
\(p : @(NatLe, @(SS, @(SS, m)), @(SS, m)))
let q = @(NatLePredLem, @(SS, m), m, p) in
@(h, q);

def NatLeSnmLem =
let P = \(m : Nat)
[@(NatLe, @(SS, m), m) -> Null] in
@(NatInduct,
P,
NatLeSnmLem1,
NatLeSnmLem2);

0≤1

dec ZeroLEqOneLem : @(NatLe, OO, @(SS, OO));

def ZeroLEqOneLem =
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, OO, OO, @(x, OO));

0≤2

dec ZeroLEqTwoLem : @(NatLe, OO, @(SS, @(SS, OO)));

def ZeroLEqTwoLem =
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, OO, @(SS, OO), @(ZeroLEqOneLem, T, x, y));

0≤3

dec ZeroLEqThreeLem : @(NatLe, OO, @(SS, @(SS, @(SS, OO))));

def ZeroLEqThreeLem =
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, OO, @(SS, @(SS, OO)), @(ZeroLEqTwoLem, T, x, y));

n ≤ m → n ̸> m

dec NatLeNegGtLem :

40
 !(n : Nat, m : Nat)
[@(NatLe, n, m) -> @(Neg, @(NatGt, n, m))];

n<m→n≤m

dec NatLt2NatLeLem :
!(n : Nat, m : Nat)
[@(NatLt, n, m) -> @(NatLe, n, m)];

def NatLt2NatLeLem =
\(n : Nat, m : Nat)
\(h : @(NatLt, n, m))
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, n),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(h, T, \(n : Nat) @(y, n, n, @(x, n)), y);

a<b∧b=c→a<c

dec NatLtEqLtTranLem :
!(a : Nat, b : Nat, c : Nat)
[@(NatLt, a, b) -> @(NatEq, b, c) -> @(NatLt, a, c)];

def NatLtEqLtTranLem =
\(a : Nat, b : Nat, c : Nat)
\(h1 : @(NatLt, a, b), h2 : @(NatEq, b, c))
let p = @(NatEq2EqNatLem, b, c, h2) in
let P = \(z : Nat) @(NatLt, a, z) in
@(p, P, h1);

a=b∧b<c→a<c

dec NatEqLtLtTranLem :
!(a : Nat, b : Nat, c : Nat)
[@(NatEq, a, b) -> @(NatLt, b, c) -> @(NatLt, a, c)];

def NatEqLtLtTranLem =
\(a : Nat, b : Nat, c : Nat)
\(h1 : @(NatEq, a, b), h2 : @(NatLt, b, c))
let p = @(NatEq2EqNatLem, a, b, h1) in
let q = @(Symm_Eq, Nat, a, b, p) in
let P = \(z : Nat) @(NatLt, z, c) in
@(q, P, h2);

n = m → n < S(m)

dec NatEqLeSSLem :
!(n : Nat, m : Nat)
[@(NatEq, n, m) -> @(NatLt, n, @(SS, m))];

41
 def NatEqLeSSLem =
\(n : Nat, m : Nat)
\(h : @(NatEq, n, m))
let p = @(NatEq2EqNatLem, n, m, h) in
let P = \(z : Nat)
@(NatLt, n, @(SS, z)) in
@(p, P, @(NatLtN, n));

n≤m→n<m∨n=m

dec NatLe2NatLtEqLem :
!(n : Nat, m : Nat)
[@(NatLe, n, m) -> @(Or, @(NatLt, n, m), @(NatEq, n, m))];

def NatLe2NatLtEqLem =
\(n : Nat, m : Nat)
\(h : @(NatLe, n, m))
let T = \(a : Nat, b : Nat)
@(Or, @(NatLt, a, b), @(NatEq, a, b)) in
@(h,
T,
\(a : Nat)
@(INJ2, @(NatLt, a, a), @(NatEq, a, a), @(NatEqReflLem, a)),
\(a : Nat, b : Nat)
\(p : @(Or, @(NatLt, a, b), @(NatEq, a, b)))
@(WHEN,
@(NatLt, a, b),
@(NatEq, a, b),
@(Or, @(NatLt, a, @(SS, b)), @(NatEq, a, @(SS, b))),
p,
\(u : @(NatLt, a, b))
@(INJ1, @(NatLt, a, @(SS, b)), @(NatEq, a, @(SS, b)), @(NatLtS, a, b, u)),
\(u : @(NatEq, a, b))
@(INJ1, @(NatLt, a, @(SS, b)), @(NatEq, a, @(SS, b)), @(NatEqLeSSLem, a, b, u))));

n≤m∧m≤n→n=m

dec NatLe2NatEqLem :
!(n : Nat, m : Nat)
[@(NatLe, n, m) -> @(NatLe, m, n) -> @(NatEq, n, m)];

def NatLe2NatEqLem =
\(n : Nat, m : Nat)
\(h1 : @(NatLe, n, m), h2 : @(NatLe, m, n))
let p = @(NatLeNegGtLem, n, m, h1),
q = @(NatLe2NatLtEqLem, m, n, h2) in
@(WHEN,
@(NatLt, m, n),
@(NatEq, m, n),
@(NatEq, n, m),
q,
\(u : @(NatLt, m, n))
@(p, u, @(NatEq, n, m)),

42
 \(u : @(NatEq, m, n))
@(NatEqSymmLem, m, n, u));

def NatLeNegGtLem =
\(n : Nat, m : Nat)
\(h : @(NatLe, n, m))
\(p : @(NatGt, n, m))
let q1 = @(NatLt2NatLeLem, m, n, p),
q2 = @(NatLe2NatEqLem, n, m, h, q1),
q3 = @(NatEq2EqNatLem, n, m, q2),
q4 = @(Symm_Eq, Nat, n, m, q3) in
let P = \(z : Nat)
@(NatLt, z, n) in
@(NatLtNmLem, n, @(q4, P, p));

3.4.8 Definition of ≥

def NatGe =
\(n1 : Nat, n2 : Nat)
@(NatLe, n2, n1);

3.4.9 Linear Ordering of NatLe on Nat

The linear ordering of NatLe on Nat is described as follows:

n≤m∨n≥m∨n=m

dec TrichLem :
!(n : Nat, m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m)));

dec TrichLem1 :
!(m : Nat)
@(Or,
@(NatLe, OO, m),
@(Or,
@(NatGe, OO, m),
@(NatEq, OO, m)));

dec TrichLem11 :
@(Or,
@(NatLe, OO, OO),
@(Or,
@(NatGe, OO, OO),
@(NatEq, OO, OO)));

def TrichLem11 =
let Q1 = @(NatLe, OO, OO),
Q2 = @(NatGe, OO, OO),
Q3 = @(NatEq, OO, OO) in

43
 let q = @(NatLeReflLem, OO) in
@(INJ1, Q1, @(Or, Q2, Q3), q);

dec TrichLem12 :
let P = \(m : Nat)
@(Or,
@(NatLe, OO, m),
@(Or,
@(NatGe, OO, m),
@(NatEq, OO, m))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def TrichLem12 =
let P = \(m : Nat)
@(Or,
@(NatLe, OO, m),
@(Or,
@(NatGe, OO, m),
@(NatEq, OO, m))) in
\(m : Nat)
\(h : @(P, m))
let Q1 = @(NatLe, OO, m),
Q2 = @(NatGe, OO, m),
Q3 = @(NatEq, OO, m) in
let R1 = @(NatLe, OO, @(SS, m)),
R2 = @(NatGe, OO, @(SS, m)),
R3 = @(NatEq, OO, @(SS, m)) in
@(WHEN,
Q1,
@(Or, Q2, Q3),
@(P, @(SS, m)),
h,
\(u : Q1)
let q = @(NatLeS, OO, m, u) in
@(INJ1, R1, @(Or, R2, R3), q),
\(u : @(Or, Q2, Q3))
@(WHEN,
Q2,
Q3,
@(P, @(SS, m)),
u,
\(v : Q2)
let q = @(NatLe2NatLtEqLem, m, OO, v) in
@(WHEN,
@(NatLt, m, OO),
@(NatEq, m, OO),
@(P, @(SS, m)),
q,
\(w : @(NatLt, m, OO))
@(NatLtNOLem, m, w, @(P, @(SS, m))),
\(w : @(NatEq, m, OO))
let r = @(NatEq2EqNatLem, OO, m, @(NatEqSymmLem, m, OO, w)) in
let W = \(z : Nat)
@(P, @(SS, z)) in
let W1 = @(NatLe, OO, @(SS, OO)),
W2 = @(NatGe, OO, @(SS, OO)),

44
 W3 = @(NatEq, OO, @(SS, OO)) in
let w1 = ZeroLEqOneLem,
w2 = @(INJ1, W1, @(Or, W2, W3), w1) in
@(r, W, w2)),
\(v : Q3)
let W = \(z : Nat)
@(P, @(SS, z)) in
let W1 = @(NatLe, OO, @(SS, OO)),
W2 = @(NatGe, OO, @(SS, OO)),
W3 = @(NatEq, OO, @(SS, OO)) in
let w1 = ZeroLEqOneLem,
w2 = @(INJ1, W1, @(Or, W2, W3), w1) in
@(NatEq2EqNatLem, OO, m, v, W, w2)));

def TrichLem1 =
let P = \(m : Nat)
@(Or,
@(NatLe, OO, m),
@(Or,
@(NatGe, OO, m),
@(NatEq, OO, m))) in
@(NatInduct,
P,
TrichLem11,
TrichLem12);

dec TrichLem2 :
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

dec TrichLem21 :
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
!(n : Nat)
[@(P, n) ->
@(Or,
@(NatLe, @(SS, n), OO),
@(Or,
@(NatGe, @(SS, n), OO),
@(NatEq, @(SS, n), OO)))];

def TrichLem21 =
let P = \(n : Nat)
!(m : Nat)
@(Or,

45
 @(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
\(n : Nat)
\(h : @(P, n))
let P1 = @(NatLe, n, OO),
P2 = @(NatGe, n, OO),
P3 = @(NatEq, n, OO) in
let R1 = @(NatLe, @(SS, n), OO),
R2 = @(NatGe, @(SS, n), OO),
R3 = @(NatEq, @(SS, n), OO) in
@(WHEN,
P1,
@(Or, P2, P3),
@(Or, R1, @(Or, R2, R3)),
@(h, OO),
\(u : P1)
let q = @(NatLe2NatLtEqLem, n, OO, u) in
@(WHEN,
@(NatLt, n, OO),
@(NatEq, n, OO),
@(Or, R1, @(Or, R2, R3)),
q,
\(w : @(NatLt, n, OO))
@(NatLtNOLem,
n,
w,
@(Or, R1, @(Or, R2, R3))),
\(w : @(NatEq, n, OO))
let r = @(NatEq2EqNatLem, OO, n, @(NatEqSymmLem, n, OO, w)) in
let W = \(z : Nat)
@(NatGe, @(SS, z), OO) in
let w1 = ZeroLEqOneLem,
w2 = @(r, W, w1) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, w2))),
\(u : @(Or, P2, P3))
@(WHEN,
P2,
P3,
@(Or, R1, @(Or, R2, R3)),
u,
\(v : P2)
let r = @(NatLeS, OO, n, v) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, r)),
\(v : P3)
let W = \(z : Nat)
@(NatGe, @(SS, z), OO) in
let w1 = ZeroLEqOneLem,
w2 = @(NatEq2EqNatLem, OO, n, @(NatEqSymmLem, n, OO, v), W, w1) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, w2))));

dec TrichLem22 :
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLe, n, m),

46
 @(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
!(n : Nat)
[@(P, n) ->
let Q = \(m : Nat)
@(Or,
@(NatLe, @(SS, n), m),
@(Or,
@(NatGe, @(SS, n), m),
@(NatEq, @(SS, n), m))) in
!(m : Nat)
[@(Q, m) -> @(Q, @(SS, m))]];

def TrichLem22 =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
\(n : Nat)
\(p : @(P, n))
let Q = \(m : Nat)
@(Or,
@(NatLe, @(SS, n), m),
@(Or,
@(NatGe, @(SS, n), m),
@(NatEq, @(SS, n), m))) in
\(m : Nat)
\(q : @(Q, m))
let P1 = @(NatLe, n, m),
P2 = @(NatGe, n, m),
P3 = @(NatEq, n, m) in
let R1 = @(NatLe, @(SS, n), @(SS, m)),
R2 = @(NatGe, @(SS, n), @(SS, m)),
R3 = @(NatEq, @(SS, n), @(SS, m)) in
@(WHEN,
P1,
@(Or, P2, P3),
@(Q, @(SS, m)),
@(p, m),
\(u : P1)
let r = @(NatLeSuccSuccLem, n, m, u) in
@(INJ1, R1, @(Or, R2, R3), r),
\(u : @(Or, P2, P3))
@(WHEN,
P2,
P3,
@(Q, @(SS, m)),
u,
\(v : P2)
let r = @(NatLeSuccSuccLem, m, n, v) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, r)),
\(v : P3)
let r = @(NatEq2EqNatLem, n, m, v) in

47
 let W = \(z : Nat)
@(NatEq, @(SS, n), @(SS, z)) in
let w = @(r, W, @(NatEqReflLem, @(SS, n))) in
@(INJ2, R1, @(Or, R2, R3), @(INJ2, R2, R3, w))));

def TrichLem2 =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
\(n : Nat)
\(h : @(P, n))
let Q = \(m : Nat)
@(Or,
@(NatLe, @(SS, n), m),
@(Or,
@(NatGe, @(SS, n), m),
@(NatEq, @(SS, n), m))) in
@(NatInduct,
Q,
@(TrichLem21, n, h),
@(TrichLem22, n, h));

def TrichLem =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(NatEq, n, m))) in
@(NatInduct, P, TrichLem1, TrichLem2);

3.4.10 Nat with ADD, TIMES and NatLe as a Ordered Semi-Ring

dec TrichAuxLem :
!(n : Nat, m : Nat)
@(Or,
@(NatLe, n, m),
@(Or,
@(NatGe, n, m),
@(Equal, Nat, n, m)));

def TrichAuxLem =
\(n : Nat, m : Nat)
let p = @(TrichLem, n, m) in
let P1 = @(NatLe, n, m),
P2 = @(NatGe, n, m),
P3 = @(NatEq, n, m),
P4 = @(Equal, Nat, n, m) in
@(WHEN,
P1,

48
 @(Or, P2, P3),
@(Or, P1, @(Or, P2, P4)),
p,
\(u : P1)
@(INJ1, P1, @(Or, P2, P4), u),
\(u : @(Or, P2, P3))
@(WHEN,
P2,
P3,
@(Or, P1, @(Or, P2, P4)),
u,
\(v : P2)
@(INJ2, P1, @(Or, P2, P4), @(INJ1, P2, P4, v)),
\(v : P3)
let w = @(v, @(Equal, Nat), @(Refl_Eq, Nat)) in
@(INJ2, P1, @(Or, P2, P4), @(INJ2, P2, P4, w))));

def OrdSMRProof =
let P1 = @(Ax_CMO, Nat, OO, ADD),
P2 = @(Ax_MO2, Nat, II, TIMES),
P3 = @(Dis_ax, Nat, ADD, TIMES),
P4 = @(Zero_ax, Nat, OO, TIMES),
P5 = @(Ord_ax, Nat, NatLe) in
let p1 = CMOProof,
p2 = TMOProof,
p3 = \(a : Nat, b : Nat, c : Nat)
let P1 = @(Equal,
Nat,
@(TIMES, a, @(ADD, b, c)),
@(ADD, @(TIMES, a, b), @(TIMES, a, c))),
P2 = @(Equal,
Nat,
@(TIMES, @(ADD, a, b), c),
@(ADD, @(TIMES, a, c), @(TIMES, b, c))) in
let p1 = @(DistrLLem, a, b, c),
p2 = @(DistrRLem, c, a, b) in
@(ANDS, P1, P2, p1, p2),
p4 = \(n : Nat)
@(ANDS,
@(Equal, Nat, @(TIMES, OO, n), OO),
@(Equal, Nat, @(TIMES, n, OO), OO),
@(TimesLLem0, n),
@(TimesRLem0, n)),
p5 = @(ANDS,
@(Tran, Nat, NatLe),
@(Trich, Nat, NatLe),
NatLeTranLem,
TrichAuxLem) in
@(ANDS,
P1,
@(And, P2, @(And, P3, @(And, P4, P5))),
p1,
@(ANDS,
P2,
@(And, P3, @(And, P4, P5)),
p2,
@(ANDS,

49
 P3,
@(And, P4, P5),
p3,
@(ANDS, P4, P5, p4, p5))));

def NatOrdSemiRing = @(OrdSMRingGen, <Nat, OO, II, ADD, TIMES, NatLe>, OrdSMRProof);

3.5 Strict Inequalities <

3.5.1 Strict Inequality Defined as a Successor and Transitive Relation
3.5.2 Inductive Definition of NatLt

def NatLt =
\(n : Nat, m : Nat)
!(T : [Nat -> Nat -> Prop])
[!(n : Nat) @(T, n, @(SS, n)) ->
!(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))] ->
@(T, n, m)];

3.5.3 Production Rules of NatLt

dec NatLtN : !(n : Nat) @(NatLt, n, @(SS, n));

def NatLtN =
\(n : Nat)
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, @(SS, n)),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(x, n);

dec NatLtS :
!(n : Nat, m : Nat)
[@(NatLt, n, m) -> @(NatLt, n, @(SS, m))];

def NatLtS =
\(n : Nat, m : Nat, p : @(NatLt, n, m))
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, @(SS, n)),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, n, m, @(p, T, x, y));

There is no production rules for @(NatLt, m, OO) for any natural number m. It has the type Null. We treat this as an
axiom instead.

dec NatLtNOAxm :
!(m : Nat)
@(Equal, Prop, @(NatLt, m, OO), Null);

dec NatLtNOLem :
!(m : Nat)

50
 [@(NatLt, m, OO) -> Null];

def NatLtNOLem =
\(m : Nat)
\(H : @(NatLt, m, OO))
let P = \(Z : Prop) Z in
@(NatLtNOAxm, m, P, H);

There is no production rules for @(NatLt, m, m) for any natural number m. It has the type Null. We treat this as an
axiom instead.

dec NatLtNmAxm :
!(m : Nat)
@(Equal, Prop, @(NatLt, m, m), Null);

dec NatLtNmLem :
!(m : Nat)
[@(NatLt, m, m) -> Null];

def NatLtNmLem =
\(m : Nat)
\(H : @(NatLt, m, m))
let P = \(Z : Prop) Z in
@(NatLtNmAxm, m, P, H);

3.5.4 Conditions for NatLt

Similar to NatLeCond we have the following conditions for NatLt.

def NatLtCond1 =
\(n : Nat, m : Nat)
[@(NatLt, n, m) ->
?(d : Nat)
@(And,
@(Neg, @(Equal, Nat, d, OO)),
@(Equal, Nat, m, @(ADD, n, d)))];

def MkNatLtCond1 =
\(n : Nat, m : Nat)
\(H : @(NatLt, n, m))
\(d : Nat,
p : @(And,
@(Neg, @(Equal, Nat, d, OO)),
@(Equal, Nat, m, @(ADD, n, d))))
<d, p>;

def NatLtCond2 =
\(n : Nat, m : Nat)
[?(d : Nat)
@(And,
@(Neg, @(Equal, Nat, d, OO)),
@(Equal, Nat, m, @(ADD, n, d))) ->
@(NatLt, n, m)];

def NatLtCond =
\(n : Nat, m : Nat)

51
 @(And, @(NatLtCond1, n, m), @(NatLtCond2, n, m));

dec NatLtCondLem :
!(n : Nat, m : Nat)
@(NatLtCond, n, m);

dec NatLtCondLem1 :
!(n : Nat, m : Nat)
@(NatLtCond1, n, m);

dec NatLtCondLem11 :
!(m : Nat)
@(NatLtCond1, OO, m);

dec NatLtCondLem111 :
!(m : Nat)
[@(NatLt, OO, m) ->
let d = m in
@(Neg, @(Equal, Nat, d, OO))];

def NatLtCondLem111 =
\(m : Nat)
\(h : @(NatLt, OO, m))
let d = m in
\(p : @(Equal, Nat, d, OO))
let P = \(z : Nat)
@(NatLt, z, m) in
let q = @(Symm_Eq, Nat, d, OO, p, P, h) in
@(NatLtNmLem, m, q);

dec NatLtCondLem112 :
!(m : Nat)
[@(NatLt, OO, m) ->
let d = m in
@(Equal, Nat, m, @(ADD, OO, d))];

def NatLtCondLem112 =
\(m : Nat)
\(h : @(NatLt, OO, m))
let d = m in
@(Refl_Eq, Nat, @(ADD, OO, d));

def NatLtCondLem11 =
\(m : Nat)
\(H : @(NatLt, OO, m))
let d = m in
let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, OO, d)) in
let q1 = @(NatLtCondLem111, m, H),
q2 = @(NatLtCondLem112, m, H) in
let q = @(ANDS, Q1, Q2, q1, q2) in
@(MkNatLtCond1, OO, m, H, d, q);

dec NatLtCondLem12 :
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
!(n : Nat) [@(P, n) -> @(P, @(SS, n))];

52
dec NatLtSSLtLem :
!(n : Nat, m : Nat)
[@(NatLt, @(SS, n), m) -> @(NatLt, n, m)];

dec NatLtCondLem121 :
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
!(n : Nat)
!(h : @(P, n))
!(m : Nat)
!(p : @(NatLt, @(SS, n), m))
let q = @(h, m, @(NatLtSSLtLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, n, d)) in
let q1 = @(PJ1, Q1, Q2, r),
q2 = @(PJ2, Q1, Q2, r) in
let ds = @(PP, d) in
@(Neg, @(Equal, Nat, ds, OO));

dec NatLtSSAddLem :
!(n : Nat, d : Nat)
[@(NatLt, @(SS, n), @(ADD, n, d)) -> @(NatLt, II, d)];

dec Nat1LtDLem :
!(d : Nat)
[@(NatLt, II, d) -> @(Neg, @(Equal, Nat, @(PP, d), OO))];

def NatLtCondLem121 =
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
\(n : Nat)
\(h : @(P, n))
\(m : Nat)
\(p : @(NatLt, @(SS, n), m))
let q = @(h, m, @(NatLtSSLtLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, n, d)) in
let q1 = @(PJ1, Q1, Q2, r),
q2 = @(PJ2, Q1, Q2, r) in
let ds = @(PP, d) in
let Q = \(z : Nat) @(NatLt, @(SS, n), z) in
let u1 = @(q2, Q, p),
u2 = @(NatLtSSAddLem, n, d, u1) in
@(Nat1LtDLem, d, u2);

dec NatAddSSPPEqLem :
!(n : Nat, d : Nat)
[@(Neg, @(Equal, Nat, d, OO)) -> @(Equal, Nat, @(ADD, n, d), @(ADD, @(SS, n), @(PP, d)))];

dec NatLtCondLem122 :
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
!(n : Nat)
!(h : @(P, n))
!(m : Nat)
!(p : @(NatLt, @(SS, n), m))
let q = @(h, m, @(NatLtSSLtLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in

53
 let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, n, d)) in
let q1 = @(PJ1, Q1, Q2, r),
q2 = @(PJ2, Q1, Q2, r) in
let ds = @(PP, d) in
@(Equal, Nat, m, @(ADD, @(SS, n), ds));

def NatLtCondLem122 =
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
\(n : Nat)
\(h : @(P, n))
\(m : Nat)
\(p : @(NatLt, @(SS, n), m))
let q = @(h, m, @(NatLtSSLtLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, n, d)) in
let q1 = @(PJ1, Q1, Q2, r),
q2 = @(PJ2, Q1, Q2, r) in
let ds = @(PP, d) in
let Q = \(z : Nat) @(Equal, Nat, m, z) in
let u = @(NatAddSSPPEqLem, n, d, q1) in
@(u, Q, q2);

def NatLtCondLem12 =
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
\(n : Nat)
\(h : @(P, n))
\(m : Nat)
\(p : @(NatLt, @(SS, n), m))
let q = @(h, m, @(NatLtSSLtLem, n, m, p)) in
let d = @(FST, q), r = @(SND, q) in
let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, n, d)) in
let q1 = @(PJ1, Q1, Q2, r),
q2 = @(PJ2, Q1, Q2, r) in
let ds = @(PP, d) in
let U1 = @(Neg, @(Equal, Nat, ds, OO)),
U2 = @(Equal, Nat, m, @(ADD, @(SS, n), ds)) in
let u1 = @(NatLtCondLem121, n, h, m, p),
u2 = @(NatLtCondLem122, n, h, m, p) in
let u = @(ANDS, U1, U2, u1, u2) in
@(MkNatLtCond1, @(SS, n), m, p, ds, u);

def NatLtCondLem1 =
let P = \(n : Nat) !(m : Nat) @(NatLtCond1, n, m) in
@(NatInduct0,
P,
NatLtCondLem11,
NatLtCondLem12);

dec NatLtCondLem2 :
!(n : Nat, m : Nat)
@(NatLtCond2, n, m);

dec NatLtAddNo0Lem :
!(n : Nat, d : Nat)

54
 [@(Neg, @(Equal, Nat, d, OO)) -> @(NatLt, n, @(ADD, n, d))];

def NatLtCondLem2 =
\(n : Nat, m : Nat)
\(p : ?(d : Nat)
@(And,
@(Neg, @(Equal, Nat, d, OO)),
@(Equal, Nat, m, @(ADD, n, d))))
let d = @(FST, p), q = @(SND, p) in
let Q1 = @(Neg, @(Equal, Nat, d, OO)),
Q2 = @(Equal, Nat, m, @(ADD, n, d)) in
let q1 = @(PJ1, Q1, Q2, q),
q2 = @(PJ2, Q1, Q2, q) in
let P = \(z : Nat)
@(NatLt, n, z) in
let r = @(Symm_Eq, Nat, m, @(ADD, n, d), q2) in
@(r, P, @(NatLtAddNo0Lem, n, d, q1));

def NatLtCondLem =
\(n : Nat, m : Nat)
let P1 = @(NatLtCond1, n, m),
P2 = @(NatLtCond2, n, m) in
let p1 = @(NatLtCondLem1, n, m),
p2 = @(NatLtCondLem2, n, m) in
@(ANDS, P1, P2, p1, p2);

3.5.5 Transitive Property of NatLt

n<m∧m<l →n<l

dec NatLtTranLem :
!(n : Nat, m : Nat, l : Nat)
[@(NatLt, n, m) -> @(NatLt, m, l) -> @(NatLt, n, l)];

dec NatLtTranCondLem :
!(n : Nat, m : Nat, l : Nat)
!(d1 : Nat, d2 : Nat)
[@(Neg, @(Equal, Nat, d1, OO)) ->
@(Equal, Nat, m, @(ADD, n, d1)) ->
@(Neg, @(Equal, Nat, d2, OO)) ->
@(Equal, Nat, l, @(ADD, m, d2)) ->
let d = @(ADD, d1, d2) in
@(And,
@(Neg, @(Equal, Nat, d, OO)),
@(Equal, Nat, l, @(ADD, n, d)))];

dec NatLtTrCondLem1 :
!(d1 : Nat, d2 : Nat)
[@(Neg, @(Equal, Nat, d1, OO)) ->
@(Neg, @(Equal, Nat, d2, OO)) ->
let d = @(ADD, d1, d2) in
@(Neg, @(Equal, Nat, d, OO))];

dec NatLtTrCondLem2 :
!(n : Nat, m : Nat, l : Nat)

55
 !(d1 : Nat, d2 : Nat)
[@(Equal, Nat, m, @(ADD, n, d1)) ->
@(Equal, Nat, l, @(ADD, m, d2)) ->
let d = @(ADD, d1, d2) in
@(Equal, Nat, l, @(ADD, n, d))];

def NatLtTrCondLem2 =
\(n : Nat, m : Nat, l : Nat)
\(d1 : Nat, d2 : Nat)
\(h1 : @(Equal, Nat, m, @(ADD, n, d1)),
h2 : @(Equal, Nat, l, @(ADD, m, d2)))
let d = @(ADD, d1, d2) in
let Q = \(z : Nat) @(Equal, Nat, l, @(ADD, z, d2)) in
let q = @(h1, Q, h2) in
let R = \(z : Nat) @(Equal, Nat, l, z) in
let r = @(NatAddAssLem, n, d1, d2) in
@(r, R, q);

def NatLtTranCondLem =
\(n : Nat, m : Nat, l : Nat)
\(d1 : Nat, d2 : Nat)
\(p1 : @(Neg, @(Equal, Nat, d1, OO)),
p2 : @(Equal, Nat, m, @(ADD, n, d1)),
q1 : @(Neg, @(Equal, Nat, d2, OO)),
q2 : @(Equal, Nat, l, @(ADD, m, d2)))
let d = @(ADD, d1, d2) in
let U1 = @(Neg, @(Equal, Nat, d, OO)),
U2 = @(Equal, Nat, l, @(ADD, n, d)) in
let u1 = @(NatLtTrCondLem1, d1, d2, p1, q1),
u2 = @(NatLtTrCondLem2, n, m, l, d1, d2, p2, q2) in
@(ANDS, U1, U2, u1, u2);

def NatLtTranLem =
\(n : Nat, m : Nat, l : Nat)
\(h1 : @(NatLt, n, m), h2 : @(NatLt, m, l))
let p1 = @(NatLtCondLem1, n, m, h1),
p2 = @(NatLtCondLem1, m, l, h2) in
let d1 = @(FST, p1), q1 = @(SND, p1),
d2 = @(FST, p2), q2 = @(SND, p2) in
let Q11 = @(Neg, @(Equal, Nat, d1, OO)),
Q12 = @(Equal, Nat, m, @(ADD, n, d1)) in
let q11 = @(PJ1, Q11, Q12, q1),
q12 = @(PJ2, Q11, Q12, q1) in
let Q21 = @(Neg, @(Equal, Nat, d2, OO)),
Q22 = @(Equal, Nat, l, @(ADD, m, d2)) in
let q21 = @(PJ1, Q21, Q22, q2),
q22 = @(PJ2, Q21, Q22, q2) in
let d = @(ADD, d1, d2),
q = @(NatLtTranCondLem, n, m, l, d1, d2, q11, q12, q21, q22) in
@(NatLtCondLem2, n, l, <d, q>);

3.5.6 Successor Lemma of NatLt

n < m → n < S(m)

56
 dec NatLtSuccLem :
!(n : Nat, m : Nat)
[@(NatLt, n, m) -> @(NatLt, n, @(SS, m))];

def NatLtSuccLem = NatLtS;

3.5.7 Other Properties of NatLt

0<1

dec ZeroLtOneLem : @(NatLt, OO, @(SS, OO));

def ZeroLtOneLem =
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, @(SS, n)),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(x, OO);

0<2

dec ZeroLtTwoLem : @(NatLt, OO, @(SS, @(SS, OO)));

def ZeroLtTwoLem =
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, @(SS, n)),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, OO, @(SS, OO), @(ZeroLtOneLem, T, x, y));

0<3

dec ZeroLtThreeLem : @(NatLt, OO, @(SS, @(SS, @(SS, OO))));

def ZeroLtThreeLem =
\(T : [Nat -> Nat -> Prop])
\(x : !(n : Nat) @(T, n, @(SS, n)),
y : !(n : Nat, m : Nat)
[@(T, n, m) -> @(T, n, @(SS, m))])
@(y, OO, @(SS, @(SS, OO)), @(ZeroLtTwoLem, T, x, y));

3.5.8 Definition of NatGt

The inequality “>” is the reversion of “<”.

def NatGt =
\(n1 : Nat, n2 : Nat)
@(NatLt, n2, n1);

57
3.5.9 Linear Ordering of NatLe on Nat
The linear ordering of NatLt on Nat is described as follows:

n<m∨n>m∨n=m

dec TrichLem :
!(n : Nat, m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m)));

The proof of TrichLem is conducted using mathematical induction rule on n requiring two auxiliary lemmas TrichLem1
and TrichLem2 being proved.
0<m∨0>m∨0=m

dec TrichLem1 :
!(m : Nat)
@(Or,
@(NatLt, OO, m),
@(Or,
@(NatGt, OO, m),
@(Equal, Nat, OO, m)));

The proof of TrichLem1 is conducted using mathematical induction rule on m requiring two additional auxiliary lemmas
TrichLem11 and TrichLem12.
0<0∨0>0∨0=0

dec TrichLem11 :
@(Or,
@(NatLt, OO, OO),
@(Or,
@(NatGt, OO, OO),
@(Equal, Nat, OO, OO)));

def TrichLem11 =
let Q1 = @(NatLt, OO, OO),
Q2 = @(NatGt, OO, OO),
Q3 = @(Equal, Nat, OO, OO) in
let q = @(Refl_Eq, Nat, OO) in
@(INJ2, Q1, @(Or, Q2, Q3), @(INJ2, Q2, Q3, q));

dec TrichLem12 :
let P = \(m : Nat)
@(Or,
@(NatLt, OO, m),
@(Or,
@(NatGt, OO, m),
@(Equal, Nat, OO, m))) in
!(m : Nat)
[@(P, m) -> @(P, @(SS, m))];

def TrichLem12 =
let P = \(m : Nat)

58
 @(Or,
@(NatLt, OO, m),
@(Or,
@(NatGt, OO, m),
@(Equal, Nat, OO, m))) in
\(m : Nat)
\(h : @(P, m))
let Q1 = @(NatLt, OO, m),
Q2 = @(NatGt, OO, m),
Q3 = @(Equal, Nat, OO, m) in
let R1 = @(NatLt, OO, @(SS, m)),
R2 = @(NatGt, OO, @(SS, m)),
R3 = @(Equal, Nat, OO, @(SS, m)) in
@(WHEN,
Q1,
@(Or, Q2, Q3),
@(P, @(SS, m)),
h,
\(u : Q1)
let q = @(NatLtS, OO, m, u) in
@(INJ1, R1, @(Or, R2, R3), q),
\(u : @(Or, Q2, Q3))
@(WHEN,
Q2,
Q3,
@(P, @(SS, m)),
u,
\(v : Q2)
@(NatLtNOLem, m, v, @(P, @(SS, m))),
\(v : Q3)
let W = \(z : Nat)
@(P, @(SS, z)) in
let W1 = @(NatLt, OO, @(SS, OO)),
W2 = @(NatGt, OO, @(SS, OO)),
W3 = @(Equal, Nat, OO, @(SS, OO)) in
let w1 = ZeroLtOneLem,
w2 = @(INJ1, W1, @(Or, W2, W3), w1) in
@(v, W, w2)));

The proof of TrichLem1 is then given as follows:

def TrichLem1 =
let P = \(m : Nat)
@(Or,
@(NatLt, OO, m),
@(Or,
@(NatGt, OO, m),
@(Equal, Nat, OO, m))) in
@(NatInduct,
P,
TrichLem11,
TrichLem12);

We now start to prove TrichLem2:

dec TrichLem2 :
let P = \(n : Nat)

59
 !(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
!(n : Nat)
[@(P, n) -> @(P, @(SS, n))];

dec TrichLem21 :
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
!(n : Nat)
[@(P, n) ->
@(Or,
@(NatLt, @(SS, n), OO),
@(Or,
@(NatGt, @(SS, n), OO),
@(Equal, Nat, @(SS, n), OO)))];

def TrichLem21 =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
\(n : Nat)
\(h : @(P, n))
let P1 = @(NatLt, n, OO),
P2 = @(NatGt, n, OO),
P3 = @(Equal, Nat, n, OO) in
let R1 = @(NatLt, @(SS, n), OO),
R2 = @(NatGt, @(SS, n), OO),
R3 = @(Equal, Nat, @(SS, n), OO) in
@(WHEN,
P1,
@(Or, P2, P3),
@(Or, R1, @(Or, R2, R3)),
@(h, OO),
\(u : P1)
@(NatLtNOLem, n, u, @(Or, R1, @(Or, R2, R3))),
\(u : @(Or, P2, P3))
@(WHEN,
P2,
P3,
@(Or, R1, @(Or, R2, R3)),
u,
\(v : P2)
let r = @(NatLtS, OO, n, v) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, r)),

60
 \(v : P3)
let W = \(z : Nat)
@(NatGt, @(SS, z), OO) in
let w1 = ZeroLtOneLem,
w2 = @(Symm_Eq, Nat, n, OO, v, W, w1) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, w2))));

dec TrichLem22 :
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
!(n : Nat)
[@(P, n) ->
let Q = \(m : Nat)
@(Or,
@(NatLt, @(SS, n), m),
@(Or,
@(NatGt, @(SS, n), m),
@(Equal, Nat, @(SS, n), m))) in
!(m : Nat)
[@(Q, m) -> @(Q, @(SS, m))]];

def TrichLem22 =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
\(n : Nat)
\(p : @(P, n))
let Q = \(m : Nat)
@(Or,
@(NatLt, @(SS, n), m),
@(Or,
@(NatGt, @(SS, n), m),
@(Equal, Nat, @(SS, n), m))) in
\(m : Nat)
\(q : @(Q, m))
let P1 = @(NatLt, n, m),
P2 = @(NatGt, n, m),
P3 = @(Equal, Nat, n, m) in
let R1 = @(NatLt, @(SS, n), @(SS, m)),
R2 = @(NatGt, @(SS, n), @(SS, m)),
R3 = @(Equal, Nat, @(SS, n), @(SS, m)) in
@(WHEN,
P1,
@(Or, P2, P3),
@(Q, @(SS, m)),
@(p, m),
\(u : P1)
let r = @(NatLtSuccSuccLem, n, m, u) in

61
 @(INJ1, R1, @(Or, R2, R3), r),
\(u : @(Or, P2, P3))
@(WHEN,
P2,
P3,
@(Q, @(SS, m)),
u,
\(v : P2)
let r = @(NatLtSuccSuccLem, m, n, v) in
@(INJ2, R1, @(Or, R2, R3), @(INJ1, R2, R3, r)),
\(v : P3)
let W = \(z : Nat)
@(Equal, Nat, @(SS, n), @(SS, z)) in
let w = @(v, W, @(Refl_Eq, Nat, @(SS, n))) in
@(INJ2, R1, @(Or, R2, R3), @(INJ2, R2, R3, w))));

def TrichLem2 =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
\(n : Nat)
\(h : @(P, n))
let Q = \(m : Nat)
@(Or,
@(NatLt, @(SS, n), m),
@(Or,
@(NatGt, @(SS, n), m),
@(Equal, Nat, @(SS, n), m))) in
@(NatInduct,
Q,
@(TrichLem21, n, h),
@(TrichLem22, n, h));

The proof of TrichLem is finally given as follows:

def TrichLem =
let P = \(n : Nat)
!(m : Nat)
@(Or,
@(NatLt, n, m),
@(Or,
@(NatGt, n, m),
@(Equal, Nat, n, m))) in
@(NatInduct, P, TrichLem1, TrichLem2);

3.5.10 Nat with ADD, TIMES and NatLt as a Ordered Semi-Ring

def OrdSMRProof =
let P1 = @(Ax_CMO, Nat, OO, ADD),
P2 = @(Ax_MO2, Nat, II, TIMES),
P3 = @(Dis_ax, Nat, ADD, TIMES),

62
 P4 = @(Zero_ax, Nat, OO, TIMES),
P5 = @(Ord_ax, Nat, NatLt) in
let p1 = CMOProof,
p2 = TMOProof,
p3 = \(a : Nat, b : Nat, c : Nat)
let P1 = @(Equal,
Nat,
@(TIMES, a, @(ADD, b, c)),
@(ADD, @(TIMES, a, b), @(TIMES, a, c))),
P2 = @(Equal,
Nat,
@(TIMES, @(ADD, a, b), c),
@(ADD, @(TIMES, a, c), @(TIMES, b, c))) in
let p1 = @(DistrLLem, a, b, c),
p2 = @(DistrRLem, c, a, b) in
@(ANDS, P1, P2, p1, p2),
p4 = \(n : Nat)
@(ANDS,
@(Equal, Nat, @(TIMES, OO, n), OO),
@(Equal, Nat, @(TIMES, n, OO), OO),
@(TimesLLem0, n),
@(TimesRLem0, n)),
p5 = @(ANDS,
@(Tran, Nat, NatLt),
@(Trich, Nat, NatLt),
NatLtTranLem,
TrichLem) in
@(ANDS,
P1,
@(And, P2, @(And, P3, @(And, P4, P5))),
p1,
@(ANDS,
P2,
@(And, P3, @(And, P4, P5)),
p2,
@(ANDS,
P3,
@(And, P4, P5),
p3,
@(ANDS, P4, P5, p4, p5))));

def NatOrdSemiRing = @(OrdSMRingGen, <Nat, OO, II, ADD, TIMES, NatLt>, OrdSMRProof);

4 Models
A model of the Peano axioms is a triple (N , 0, S), where N an infinite set, 0 ∈ N and S : N → N satisfies the axioms
above. Dedekind proved in his 1888 book, What are numbers and what should they be (German: Was sind und was
sollen die Zahlen) that any two models of the Peano axioms (including the second-order induction axiom) are isomorphic.
In particular, given two models (NA , 0A , SA ) and (NB , 0B , SB ) of the Peano axioms, there is a unique homomorphism
f : NA → NB satisfying

f (0A ) = 0B
f (SA (n)) = SB (f (n))

and it is a bijection. The second-order Peano axioms are thus categorical; this is not the case with any first-order
reformulation of the Peano axioms, however.

63
4.1 First-Order Theory of Arithmetic
First-order theories are often better than second order theories for model or proof theoretic analysis. All of the Peano
axiom except the ninth axiom (the induction axiom) are statements in first-order logic. The arithmetical operations of
addition and multiplication and the order relation can also be defined using first-order axioms. The second-order axiom
of induction can be transformed into a weaker first-order induction schema.
First-order axiomatizations of Peano arithmetic have an important limitation, however. In second-order logic, it is
possible to define the addition and multiplication operations from the successor operation, but this cannot be done in the
more restrictive setting of first-order logic. Therefore, the addition and multiplication operations are directly included in
the signature of Peano arithmetic, and axioms are included that relate the three operations to each other.
The following list of axioms (along with the usual axioms of equality) is sufficient for this purpose:
• 0 ̸= S(x1 )
• S(x1 ) = S(x2 ) → x1 = x2
• x1 + 0 = x1
• x1 + S(x2 ) = S(x1 + x2 )
• x1 × 0 = 0
• x1 × S(x2 ) = x1 × x2 + x1
In addition to this list of numerical axioms, Peano arithmetic contains the induction schema, which consists of a countably
infinite set of axioms. For each formula ϕ(x, y1 , . . . , yk ) in the language of Peano arithmetic, the first-order induction axiom
for ϕ is the sentence
∀ȳ.(ϕ(0, ȳ) ∧ ∀x.ϕ(x, ȳ)) → ϕ(S(x), ȳ)) → ∀x.ϕ(x, ȳ))
where ȳ is an abbreviation for y1 , ..., yk . The first-order induction schema includes every instance of the first-order induction
axiom, that is, it includes the induction axiom for every formula ϕ.
This schema avoids quantification over sets of natural numbers, which is impossible in first-order logic. For instance,
it is not possible in first-order logic to say that any set of natural numbers containing 0 and closed under successor is
the entire set of natural numbers. What can be expressed is that any definable set of natural numbers has this property.
Because it is not possible to quantify over definable subsets explicitly with a single axiom, the induction schema includes
one instance of the induction axiom for every definition of a subset of the naturals.

4.2 Equivalent Axiomatizations

There are many different, but equivalent, axiomatizations of Peano arithmetic. While some axiomatizations, such as the
one just described, use a signature that only has symbols for 0 and the successor, addition, and multiplications operations,
other axiomatizations use the language of ordered semi-rings, including an additional order relation symbol. One such
axiomatization begins with the following axioms that describe a discrete ordered semi-ring.
• ∀x, y, z ∈ N .(x + y) + z = x + (y + z), i.e., addition is associative.
• ∀x, y ∈ N .x + y = y + x, i.e., addition is commutative.
• ∀x, y, z ∈ N .(x × y) × z = x × (y × z), i.e., multiplication is associative.
• ∀x, y ∈ N .x × y = y × x, i.e., multiplication is commutative.
• ∀x, y, z ∈ N .x × (y + z) = (x × y) + (x × z), i.e., the distributive law.
• ∀x ∈ N .x + 0 = x ∧ x × 0 = 0, i.e., zero is the identity element for addition.
• ∀x ∈ N .x × 1 = x, i.e., one is the identity element for multiplication.
• ∀x, y, z ∈ N .x < y ∧ y < z ⊃ x < z, i.e., the ‘<’ operator is transitive.
• ∀x ∈ N .¬(x < x), i.e., the ‘<’ operator is irreflexive.
• ∀x, y ∈ N .x < y ∨ x = y ∨ y < x.
• ∀x, y, z ∈ N .x < y ⊃ x + z < y + z.
• ∀x, y, z ∈ N .0 < z ∧ x < y ⊃ x × z < y × z.
• ∀x, y ∈ N .x < y ⊃ ∃z ∈ N.x + z = y.
• 0 < 1 ∧ ∀x ∈ N .x > 0 ⊃ x ≥ 1.
• ∀x ∈ N .x ≥ 0.
The theory defined by these axioms is known as PA− ; PA is obtained by adding the first-order induction schema.
An important property of PA− is that any structure M satisfying this theory has an initial segment (ordered by ≤)
isomorphic to N . Elements of M \ N are known as nonstandard elements.

64
4.3 Nonstandard Models
Although the usual natural numbers satisfy the axioms of PA, there are other non-standard models as well; the compactness
theorem implies that the existence of nonstandard elements cannot be excluded in first-order logic. The upward Löwenheim-
Skolem theorem shows that there are nonstandard models of PA of all infinite cardinalities. This is not the case for the
original (second-order) Peano axioms, which have only one model, up to isomorphism. This illustrates one way the
first-order system PA is weaker than the second-order Peano axioms.
When interpreted as a proof within a first-order set theory, such as ZFC, Dedekind’s categoricity proof for PA shows
that each model of set theory has a unique model of the Peano axioms, up to isomorphism, that embeds as an initial
segment of all other models of PA contained within that model of set theory. In the standard model of set theory, this
smallest model of PA is the standard model of PA; however, in a nonstandard model of set theory, it may be a nonstandard
model of PA. This situation cannot be avoided with any first-order formalization of set theory.
It is natural to ask whether a countable nonstandard model can be explicitly constructed. Tennenbaum’s theorem,
proved in 1959, shows that there is no countable nonstandard model of PA in which either the addition or multiplication
operation is computable. This result shows it is difficult to be completely explicit in describing the addition and multipli-
cation operations of a countable nonstandard model of PA. However, there is only one possible order type of a countable
nonstandard model. Letting ω be the order type of the natural numbers, ζ be the order type of the integers, and η be the
order type of the rationals, the order type of any countable nonstandard model of PA is ω + ζ · η, which can be visualized
as a copy of the natural numbers followed by a dense linear ordering of copies of the integers.

4.4 Set-Theoretic Models

The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as
the ZF. The standard construction of the naturals, due to John von Neumann, starts from a definition of 0 as the empty
set, ∅, and an operator s on sets defined as:
s(a) = a ∪ {a}.
The set of natural numbers N is defined as the intersection of all sets closed under s that contain the empty set. Each
natural number is equal (as a set) to the set of natural numbers less than it:

0 = ∅
1 = s(0) = s(∅) = ∅ ∪ {∅} = {0}
2 = s(1) = s({0}) = {0} ∪ {{0}} = {0, {0}} = {0, 1}
3 = {0, 1, 2}

and so on. The set N together with 0 and the successor function s : N → N satisfies the Peano axioms.
Peano arithmetic is equiconsistent with several weak systems of set theory. One such system is ZFC with the axiom of
infinity replaced by its negation. Another such system consists of general set theory (extensionality, existence of the empty
set, and the axiom of adjunction), augmented by an axiom schema stating that a property that holds for the empty set
and holds of an adjunction whenever it holds of the adjunct must hold for all sets.

5 Consistency
When the Peano axioms were first proposed, Bertrand Russell and others agreed that these axioms implicitly defined what
we mean by a “natural number”. Henri Poincar was more cautious, saying they only defined natural numbers if they were
consistent; if there is a proof that starts from just these axioms and derives a contradiction such as 0 = 1, then the axioms
are inconsistent, and don’t define anything. In 1900, David Hilbert posed the problem of proving their consistency using
only finitistic methods as the second of his twenty-three problems. In 1931, Kurt Gödel proved his second incompleteness
theorem, which shows that such a consistency proof cannot be formalized within Peano arithmetic itself.
Although it is widely claimed that Gödel’s theorem rules out the possibility of a finitistic consistency proof for Peano
arithmetic, this depends on exactly what one means by a finitistic proof. Gödel himself pointed out the possibility of giving
a finitistic consistency proof of Peano arithmetic or stronger systems by using finitistic methods that are not formalizable
in Peano arithmetic, and in 1958 Gödel published a method for proving the consistency of arithmetic using type theory.
In 1936, Gerhard Gentzen gave a proof of the consistency of Peano’s axioms, using transfinite induction up to an ordinal
called ϵ0 . Gentzen explained: “The aim of the present paper is to prove the consistency of elementary number theory
or, rather, to reduce the question of consistency to certain fundamental principles”. Gentzen’s proof is arguably finitistic,
since the transfinite ordinal ϵ0 can be encoded in terms of finite objects (for example, as a Turing machine describing
a suitable order on the integers, or more abstractly as consisting of the finite trees, suitably linearly ordered). Whether

65
 or not Gentzen’s proof meets the requirements Hilbert envisioned is unclear: there is no generally accepted definition of
exactly what is meant by a finitistic proof, and Hilbert himself never gave a precise definition.
The vast majority of contemporary mathematicians believe that Peano’s axioms are consistent, relying either on intuition
or the acceptance of a consistency proof such as Gentzen’s proof. The small number of mathematicians who advocate
ultrafinitism reject Peano’s axioms because the axioms require an infinite set of natural numbers.

6 Conclusions
We have presented a complete investigation of natural numbers formalized in terms of Peano’s axioms and arithmetics by
the mathematical theorem proof development system PowerEpsilon. This work shows that PowerEpsilon can serve
very well as a logical framework for which the mathematical reasoning can be formalized.

References
[1] Yves Bettot and Pierre Castéran. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.
[2] Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, 1979.
[3] R. L. Constable and et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc.,
Englewood Cliffs, New Jersey, 1986.
[4] T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2/3), 1988.
[5] J.-Y. Girard. Proofs and Types. Cambridge University Press, Cambridge, UK, 1989.
[6] M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. LNCS 78. Springer-Verlag, 1979.
[7] Michael J. C. Gordon and Thomas F. Melham. Introduction to HOL: a theorem proving environment for higher order
logic. Cambridge University Press, 1993.
[8] P. Martin-Löf. An intuitionistic theory of types: Predicative part. In Proceedings of Logic Colloquium 1973. North-
Holland, 1973.
[9] P. Martin-Löf. Constructive mathematics and computer programming. In Proceedings of Six International Congress
for Logic, Methodology, and Philosophy of Science, Amsterdam, 1982. North-Holland.
[10] P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory, Vol. 1. Bibliopolis, Naples, 1984.
[11] L. C. Paulson. The foundation of a generic theorem prover. Journals of Automated Reasonning, 5, 1989.
[12] M.-Y. Zhu. AUTOSTAR - a software development system. ACM SIGPLAN Notices, 23(3), 1989.

66

View publication stats