Equality in the Presence of Apartness: An Application of Structural Proof Analysis to Intuitionistic Axiomatics

Abstract

The theories of apartness, equality, and n-stable equality are presented through contraction- and cut-free sequent calculi. By methods of proof analysis, a purely proof-theoretic characterization of the equality fragment of apartness is obtained.