Not sure this works constructively. x < y or x = y or x > y is valid for the constructive rationals, but taboo for the constructive reals. Wouldn’t this make it taboo for the real order to be an elementary extension of the rational order? Not familiar with constructive model theory so not entirely sure.
Not sure this works constructively. x < y or x = y or x > y is valid for the constructive rationals, but taboo for the constructive reals. Wouldn’t this make it taboo for the real order to be an elementary extension of the rational order? Not familiar with constructive model theory so not entirely sure.