Ambiguity in Typed Set Theory and the Universal-Existential Conjecture

Typed set theory deals with the traditional paradoxes of set theory by implementing the notion of a type at the level of syntax. This gives rise to the Simple Theory of Types (TST) and the Theory of Positive and Negative types (TZT). New Foundations NF is a theory that explicitly gets rid of the typing discipline used in TST and TZT but still essentially codes it into the formation of sets. The scheme of typical ambiguity asserts that all the types look the same. It turns out that TZT together with the scheme of typical ambiguity is consistent if and only if NF is consistent. Consequently, certain subsystems of NF are consistent if and only if TZT together with a corresponding subclass of the scheme of ambiguity is consistent. The consistency of NF has been an open problem since its conception and so ambiguity for certain classes of formulae have generated great interest. One such class is the class of universal-existential sentences. The main result of this thesis makes progress on what is known as the universal-existential conjecture. This is done by showing that TZT decides a larger subclass of the universal-existences than previously known. This has the consequence of showing that NF decides all universal-existential sentences that have a stratification belonging to this subclass. There is also a new result showing that ambiguity holds in the arithmetic of TZTI and the first verification of the canonicity of the term model for TZTO, a relativisation of a known result for NFO.