Eliminability of definite descriptions

Judgemental First-Order Zermelo-Fraenkel Set Theory with Descriptions (JZF)[3], is a rigorous formalization of constructive set theory. JZF includes a natural deduction system for first-order logic extended with the axioms of an intuitionistic set theory (Intuitionistic Zermelo-Fraenkel set theory [1, 6]). The system is extended by the set elementhood binary relation as well as definite descriptions [8, 9]. Definite descriptions make it possible to concisely and directly reason about sets that are uniquely identified by a specific property. However, these descriptions are not a necessary part of the system. Thus, we must be able to eliminate definite descriptions from JZF by translating all propositions that use them into equivalent ones that do not. Furthermore, we must ensure that all propositions that are derivable in JZF remain derivable when translated. In this thesis, we prove the metatheorem that definite descriptions are eliminable. First, we provide a translation from propositions in JZF to a new system: one that uses the subset of JZF rules that do not contain definite descriptions. Then, we prove that the corresponding translations of propositions that are derivable in JZF are derivable in the system without definite descriptions.