Inequality in constructive mathematics.
Wim Ruitenburg · Notre Dame Journal of Formal Logic · 1991
We present difference relations as a natural generalization of inequality in constructive mathematics.Differences on a set S are defined as binary relations on all powers S n simultaneously, satisfying axiom schemas generalizing the ones for inequality.The denial inequality and the apartness relation are special cases of a difference relation.Several theorems in constructive algebra are given that unify and generalize well-known results in constructive algebra previously employing special cases of difference relations.Finally, we discuss extended differences for a set S as collections of relations defined on all powers S x simultaneously.