We generalize Specker's theorem on typical ambiguity, that NF and TST + Ambiguity have the same stratified consequences, to the subschemes Amb(Γ) of ambiguity restricted to classes of sentences Γ with certain natural closure conditions.

We give a necessary and sufficient condition in order that a type-shifting automorphism be constructed on a model of the Theory of Simple Types (TST) by forcing. Namely it is proved that, if for every n ≥ 1 there is a model of TST in the ground model M of ZFC that contains an n-extendible coherent pair, then there is a generic extension M[G] of M that contains a model of TST with a type-shifting automorphism, and hence M[G] contains a (...) model of NF. The converse holds trivially. It is also proved that there exist models of TST containing l-extendible coherent pairs. (shrink)