Abstract: Sequent calculus proof theory of intuitionistic apartness and order relations
Sara Negri
Sequent calculus formulations of intuitionistic
theories of apartness and order are given and
cut-elimination for the calculi proved.
Among the consequences of the result is
the disjunction property for these theories.
Through methods of proof analysis
and permutation of rules, we establish conservativity
of theories of apartness and constructive order
over the theory of equality and the usual theories of order.
Back to Sara's homepage.