Model Theories of Set Theories and Type Theory

This paper is divided into three parts. In the first part, we review the historical background of a system of logic devised by Henry S. Leonard to allow for reasoning using existence as a predicate. In the second part, we consider various directions in which his logic could be further developed, syntactically, semantically, and as an adjunct to quantifier elimination and set theory. In the third and final part, we develop proofs of some underlying results of his logic, using modern notation but retaining his axioms and rules of inference.