 Other propositional connectives and the existential quantifier are easily defined. By using \(\iota_{(\imath({o}\imath))}\), one can define description operators \(\iota_{\alpha({o}\alpha)}\) for all types α.