Sequent calculus proof theory of intuitionistic apartness and order relations

Contraction-free sequent calculi for intuitionistic theories of apartness a nd order are given and cut-elimination for the calculi proved. Among the co nsequences of the result is the disjunction property for these theories. Th rough methods of proof analysis and permutation of rules, we establish cons ervativity of the theory of apartness over the theory of equality defined a s the negation of apartness, for sequents in which all atomic formulas appe ar negated. The proof extends to conservativity results for the theories of constructive order over the usual theories of order.