\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Numbers in Mizar

Table of Contents

1. Overview

Numbers are constructed in Mizar as working mathematicians use them, e.g., \(\mathbb{N}\subset\mathbb{Z}\subset\mathbb{Q}\subset\mathbb{R}\).

But they are scattered across various articles (NUMBERS, XREAL, XXREAL, ORDINAL, NEWTON, and so on).

  • Natural numbers are registered as real numbers in XREAL_0
    • This implies that positive is registered for natural numbers, since positive is registered for real numbers in XREAL_0, too.
  • The general pattern seems to be that the set of a number system is defined using all capital letters (e.g., INT, RAT, REAL, COMPLEX, etc.), the attribute of belonging to the set is defined using all lowercase letters (e.g., integer, rational, real, complex, etc.), and the type is defined using PascalCase (e.g., Nat, Integer, Rational, Real, Complex, etc.).
    • The only "exception" to this is that natural is defined as belonging to the \(\omega\) ordinal…but NAT is defined as a synonym for \(\omega\), so I guess it all checks out.
  • This extends to Quaternions: the set QUATERNION, attribute quaternion, and type Quaternion
  • The Octonions are implicitly constructed in CAYLDICK, but there is no set OCTONION, attribute octonion, or type Octonion (though it should be straightforward to implement these guys).

Last Updated 2023-01-31 Tue 09:50.