次の命題を考える（証明はしない）。
$`\quad \forall x\in {\bf R}.\exists n\in {\bf Z}. n \le x \lt n + 1`$
もしこれが成立するなら、実数を整数部と小数部に分けることができる。
$`\quad x = n + r \text{ where } n\in{\bf Z} \land 0\le r \lt 1`$
ちゃんと書くなら：
$`\quad \forall x\in {\bf R}.\exists n\in {\bf Z}, r \in {\bf R}.(x = n + r \land 0\le r \lt 1)`$
これを示す前提としてアルキメデス性は使っていいとする。実数のアルキメデス性〈the Archimedean property〉は次のように書けた。
$`\quad
\forall a, b\in {\bf R}.( a \gt 0 \implies \exists n\in {\bf N}. na \gt b )
`$
負の実数に関しては、符号を反転する写像 $`x \mapsto -x`$ を使ってなんとかするとして、非負実数だけに絞って考える。すると、目的の命題は：
$`\quad \forall x\in {\bf R}_{\ge 0}.\exists n\in {\bf N}. n \le x \lt n + 1`$
ここで、
$`\quad {\bf R}_{\ge 0} := \{x\in {\bf R} \mid x \ge 0\}`$
アルキメデス性は：
$`\quad
\forall a, b\in {\bf R}_{\ge 0}. \exists n\in {\bf N}. na \gt b
`$
特に、$`a = 1`$ と置くと：
$`\quad
\forall b\in {\bf R}_{\ge 0}. \exists n\in {\bf N}. n \gt b
`$
自然言語で言えば：
- どんな非負実数に対しても、それより（真に）大きい自然数が存在する。
言い方を変えれば、
- どんな非負実数に対しても、それより（真に）大きい自然数の集合は空ではない。
空でない部分集合に最小元（あるいは最大下界）の存在が言えれば、「より大きいなかでは最小」な自然数がとれる。
この性質（最大下界の存在）は、自然数の性質と考えるか非負実数の性質と考えるかで違う定式化になる。自然数だけで考えれば：
$`\newcommand{\mrm}[1]{\mathrm{#1}}
\forall A \in \mrm{Pow}({\bf N}).(\\
\quad A \ne \emptyset \implies \\
\quad \exists m \in {\bf N}.( \\
\qquad \forall k\in A.( m \le k) \land\\
\qquad \forall l \in{\bf N}.(
\forall k\in A.( l \le k) \implies l \le m
)\\
\quad )\\
)
%`$
上記の命題は、実数には一切言及してないので、自然数単独で言える性質である。
非負実数に関して同様な性質があれば、$`{\bf N}\subset {\bf R}`$ だから、最大下界の存在は言える。
$`\forall A \in \mrm{Pow}({\bf R}_{\ge 0} ).(\\
\quad A \ne \emptyset \implies \\
\quad \exists x \in {\bf R}_{\ge 0}.( \\
\qquad \forall s\in A.( x \le s) \land\\
\qquad \forall y \in {\bf R}_{\ge 0}.(
\forall s\in A.( y \le s) \implies y \le x
)\\
\quad )\\
)
%`$
この場合、最大下界は実数として与えられるので、次が保証されているわけではない。
$`\quad A\subseteq {\bf N} \implies \mrm{inf}(A) \in {\bf N}`$
こので、$`\mrm{inf}`$ は、非空集合の最大下界を与える関数。この関数の存在は別途証明を必要とする。最大下界の存在が保証されていても、一意性は別だから、関数値の一意性のために最大下界の一意性証明が要求される。
ともかくも、非負実数 $`x \in {\bf R}_{\ge 0}`$ に対して、次の集合を考える。
$`\quad U(x) := \{t \in {\bf R}_{\ge 0} \mid x \lt t \land t \in {\bf N} \}`$
なんらかの方法で、$`\mrm{inf}(U(x))`$ が自然数として存在することが示せれば、冒頭の命題の証明に近づくことになる。
