In this chapter, the authors adopt a similar strategy as regards quantificational logic (QL), i.e. they introduce a set of rules of inference so as to develop a formal system of quantificational logic. As a formal language, QL inherits all of the formal vocabulary of PL. Moreover, as a formal system, QL inherits the entire deductive apparatus of PL. In the proof-theory of PL, each connective has both an introduction-rule which allows us to enter that connective onto a line of proof and an elimination-rule which allows us to eliminate a connective from a line of proof. The authors use the proper names from QL to denote each of the inhabitants of Fabworld respectively. Having outlined and discussed both the introduction-rule and the elimination-rule for the universal quantifier in the proof-theory of QL, the authors turn their attention to the rules of inference which govern the existential quantifier.