6
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Yes! But I don't see a clear motivation for Amb other than on logical grounds, and more precisely the logic of types and their rule in preventing paradoxes through cutting the circularity that is thought to be the underpenning of all logical paradoxes. Clearly, the types are a tool to achieve this logical aim, but achieving this aim bears no relavance to the particular valuation of types over a formula, the most important is the relative positions those types bear towards each other, so clearly Amb is justified logically, I don't see other part of justification, so to me its purely logical. $\endgroup$ Aug 22, 2021 at 16:43
  • $\begingroup$ You mean it proves the stratified theorems of NF as typed theorems in all levels, yet this does change the meaning, for example NF asserts existence of a universal set, but TST+Amb would only assert that for each type there exists of a set of all objects of that type, this set is unlike the universal set of NF is not in itself. But, with infinity it appears the meaning is the same, like the assertion of existence of a Dedekind infinite set! $\endgroup$ Aug 22, 2021 at 20:05
  • $\begingroup$ I just wanted to comment, that along this answer, one can say that the majority of mathemtics can be founded in a by-product of logicism?! Which to me appears to be in some sense a kind of logicism, though un-intended. $\endgroup$ Jul 11, 2022 at 6:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.