「実数εを任意に選べる文脈で、項と極限値の差をε未満に抑えるNを選ぶことができる」ことを示すのがイプシロンデルタ論法

それを記号論理で扱える処理系を実装すればいいだけ

εは「正の実数である」という情報しか持っていない
浮動小数点数や多倍長整数の誤差なんか全く無関係