Real numbers

Uses Rational numbers.

Many programming languages use the label "real numbers" for Floating-point numbers. In Leibniz, real numbers are the real numbers defined in mathematics. Real numbers cannot be represented in a computer, because the information content of a real number is, in general, infinite. Only well-defined subsets, such as the Rational numbers, can be represented as a finite sequence of bits. However, Leibniz is not a programming language, but a specification language. Even if you cannot compute with real numbers, you can still talk about real numbers and define axioms and rules in terms of real numbers.

The sort ℝ describes the real numbers. The rational numbers are a subsort: ℚ ⊆ ℝ.

There is a subsort ℝ.nz ⊆ ℝ for the non-zero real numbers, with ℚ.nz ⊆ ℝ.nz.

Another subsort, ℝ.nn ⊆ ℝ, describes the non-negative real numbers. The non-negative rational number are a subsort: ℚ.nn ⊆ ℝ.nn.

The positive real numbers, ℝ.p, are both non-zero (ℝ.p ⊆ ℝ.nz) and non-negative (ℝ.p ⊆ ℝ.nn). The positive rational number are a subsort: ℚ.p ⊆ ℝ.p.

Arithmetic

Addition

The sum of two real numbers is a real number:
 ℝ + ℝ : ℝ

Important special cases are:
 ℝ.p + ℝ.p : ℝ.p
 ℝ.nn + ℝ.nn : ℝ.nn

Addition is commutative:
 x:ℝ, y:ℝ, x + y = y + x
and associative:
 x:ℝ, y:ℝ, z:ℝ, (x + y) + z = x + (y + z)

Rules:

Eliminate zeros:
 (x:ℝ) + (zero:zero) ⇒ x
 (zero:zero) + (x:ℝ) ⇒ x

Subtraction

The difference of two real numbers is a real number:
 ℝ - ℝ : ℝ

The negative of a real number is a real number:
 -(ℝ) : ℝ

Rules

Eliminate zeros:
 (x:ℝ) - (zero:zero) ⇒ x
 (zero:zero) - (x:ℝ) ⇒ -(x)

Multiplication

The product of two real numbers is a real number:
 ℝ × ℝ : ℝ

Important special cases are:
 ℝ.p × ℝ.p : ℝ.p
 ℝ.nn × ℝ.nn : ℝ.nn
 ℝ.nz × ℝ.nz : ℝ.nz

Multiplication is commutative:
 x:ℝ, y:ℝ, x × y = y × x
and associative:
 x:ℝ, y:ℝ, z:ℝ, (x × y) × z = x × (y × z)

Addition is distributive over multiplication:
 x:ℝ, y:ℝ, z:ℝ, x × (y + z) = (x × y) + (x × z)

Rules:

Eliminate zeros:
 (x:ℝ) × (zero:zero) ⇒ 0
 (zero:zero) × (x:ℝ) ⇒ 0

Eliminate ones:
 (one:one) × (x:ℝ) ⇒ x
 (x:ℝ) × (one:one) ⇒ x

Division

The quotient of a real number and a non-zero real number is a real number:
 ℝ ÷ ℝ.nz : ℝ

Important special cases are:
 ℝ.nz ÷ ℝ.nz : ℝ.nz
 ℝ.p ÷ ℝ.p : ℝ.p
 ℝ.nn ÷ ℝ.p : ℝ.nn

Rules:

Elimination of zeros and ones:
 (z:zero) ÷ (x:ℝ.nz) ⇒ 0
 (x:ℝ) ÷ (one:one) ⇒ x

Exponentiation

Exponentiation is defined for non-zero real number to any integer power:
 ℝ.nz^ℤ.nz : ℝ.nz
 ℝ.nz^zero : ℕ.nz

The case of zero has already been defined in Integers.

Positive real numbers can be taken to any non-zero real power:
 ℝ.p^ℝ.nz : ℝ.p

Non-negative real numbers can be taken to any positive real power:
 ℝ.nn^ℝ.p : ℝ.nn

Rules:

Eliminate zeros:
 (x:ℝ.nz)^z:zero ⇒ 1

Eliminate ones:
 (x:ℝ.nz)^one:one ⇒ x

Comparison

ℝ < ℝ : 𝔹
ℝ > ℝ : 𝔹
ℝ ≤ ℝ : 𝔹
ℝ ≥ ℝ : 𝔹