On axiomatizing fragments
C. Smoryński · Journal of Symbolic Logic · 1977
The main purpose of this note is to present new semi-model-theoretic proofs of some axiomatization results. Principally, we prove the result of [van Dalen and Statman] on the axiomatization of the equality fragment of the intuitionistic theory of apartness by ω-fold stability axioms. Further examples are also discussed. The intuitionistic theories of equality and apartness are given by the following nonlogical axioms: EQ . AP . In AP, one can define a notion of equality by means of the abbreviation: . The corresponding interpretation of E Q in AP is not faithful — since equality is a negation, we have stability of equality: . The equality fragment of AP is axiomatized by a suitable generalization of the stability of equality. To state it, one first defines a sequence of partial apartness relations: . A simple induction shows, for all n, whence .