論理体系は指定されてないんだから任意だとしてよいんだよな。
だとしたら定数記号として実数が全て含まれていて
任意のs,tに対してs=tかs≠tのどちらかが公理に含まれているような場合は
>>810は成り立たないな