実数の形式体系

ウィキペディアの「0.999...」の項が話題になったことがあるが、これって形式体系としてはどうなるんだろう？

実数の形式体系というのを、「X_i」という変項と「a_i」という定項だけを使って定義するなら問題はない。でも、その形式体系は、「0.999...」に相当する表現を含まない。

自然数の形式的体系は、例えば「0'''''」といった記号列を導入することによって、これなら「5」に相当する表現をもっている。

そういったものを持つ形式体系を実数に関して構築するならば、そしてそれが「0.999...」に相当する表現と、「1」に相当する表現を別々に持つならば、やはりそれらは別の記号であって、純粋に形式的な見方から言えば別の項(のタイプ)という外ない。

解決策は、同一性記号「=」とその記号に関する公理図式(二階の述語論理なら公理)を別に導入するということだろう。しかし、そうすると「¬(a=b)(ただし、aとbは異なる定項)」という公理図式を使うことはできないだろう。

また、自然数の形式的体系は、例えば「0''' + 0''」といった式の記号列を、「0'''''」という式の記号列に変換する、明示的なアルゴリズムを持つことができる。

実数の形式的体系は、そのようなアルゴリズムを持つことができるのだろうか？　その形式体系は「1/9 * 9」という式に相当する表現を、そのアルゴリズムにしたがって「1」に相当する表現に変換することができるのか？