このLeonardoさん、代数のイロハを勉強した方が良いですよ。代数的数の中で実数で表わせるのは特殊ケースだし、exactなeや2\pi iは計算機で自然に実現できるし（2\pi iの方は卑怯だけど。そしてそのばあいは0,1,-1以外の有理数は一つもfaithfulには表現できなくなるけど）、無限小はスキーム的に冪零元で表現するのが自然だし、と色々突っ込みたくなる。

> 代数的数の中で実数で表わせるのは特殊ケースだし、

まあ、代数的数を実数と言ってしまっているのはどうかとは思いましたが、文中でも Algebraic numbers と大文字で書き始めるので統一されているので、ここでは単にZ3での実数のデータ表現のことを指しているのでしょう。

> exactなeや2\pi iは計算機で自然に実現できるし（2\pi iの方は卑怯だけど。そしてそのばあいは0,1,-1以外の有理数は一つもfaithfulには表現できなくなるけど）、無限小はスキーム的に冪零元で表現するのが自然だし、と色々突っ込みたくなる。

あまり理解できていないのですが、実閉体の理論をこのように拡張をした理論(の quantifier free な fragment)に対する決定手続きを実装する上で、その方が都合が良いのでしょうか？

メタな言い方をすると、代数のカテゴリーでは順序に拘るのは得策ではない、と思います（だから実閉体も人工的な概念だと）。それよりも付値の方がユニバーサルなのは歴史的にも明らかなはず（p進とかアデールとか）。アルキメデスな局所体を計算機で扱うのだったら
z = e^{r + 2 \pi i s}
で、rとsは有理数（あるいは2のベキ分の整数）の様に表現するのが、少なくとも数学的には自然だと思います。こうすれば、BigNumがアプリオリに有界ではない任意の整数を扱える程度には、任意の複素数を扱えるし。

なるほど……
まだちゃんと理解は出来ていませんが、ありがとうございます。