Does simple theory of types + ambiguity prove axiom of infinity?
The simple theory of types known as $\sf TST$ is a multi-sorted first order theory, syntactical restrictions include $\in$ being a dyadic symbol where the symbol on the right of it is one sort (type) higher than the one on the left, while the two symbols linked by $=$ must be of the same type.
Axioms (on top of multi-sorted axioms of identity):
Extensionality: $\forall x^{i+1} \, \forall y^{i+1}:\\ \forall z^i (z^i \in x^{i+1} \leftrightarrow z^i \in y^{i+1}) \to x^{i+1}=y^{i+1}$
Comprehension: if $\phi$ is a formula in which $x^{i+1}$ doesn't occur, then: $$\exists x^{i+1} \, \forall y^i (y^i \in x^{i+1} \leftrightarrow \phi)$$
Now the schema of ambiguity is:
Ambiguity: If $\phi^+$ is the formula obtained from formula $\phi$ by raising all type indices in $\phi$ by one, then: $$\phi \iff \phi^+$$ It's well known that $\sf TST +Ambg$ is equi-interpretable with Quine's $\sf NF$ [Specker]. The latter is known to prove Infinity [Specker].
Would that entail that the fomer must also prove Infinity?
That was the first question.
The second question is if the answer is to the positive, then clearly the above theory is purely motivated by a logic of types, and types are only needed in a relative manner, and clearly this doesn't need the particular values of types to matter other than their relative positions. There is a remote resemblance between ambiguity and axiom of reducibility of Russell's, although of course they are not the same principle. If Infinity is provable from the above purely logically motivated axioms for set theory, then in some sense this could be seen as a motivation for logicism, since infinity, a clearly mathematical axiom, is not axiomatized here! So my second question is:
Had $\sf TST + Ambg$ been considered as motivating the program of logicism?