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](https://arxiv.org/pdf/1503.01406.pdf)]. The latter is known to prove *Infinity* [[Specker](https://arxiv.org/pdf/1503.01406.pdf)].



> 
> 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?
> 
> 
> 



Does simple theory of types + ambiguity prove axiom of infinity?
The development of TST + Amb is arguably motivated by the logicist program, ultimately.


But Amb is not a purely logical principle, it is a conjecture past the logically provable facts, with unexpected consequences.


I dont think that TST + Amb can be taken to motivate logicism. It is a by-product of this program.


TST + Ambiguity proves every stratified theorem of NF, so it proves Infinity, disproves Choice, and so forth.


