3
$\begingroup$

I just want to know if Tangled Type Theory $\mathsf{TTT}$ of Randall Holmes ([see: Holmes - NF is consistent, p:11, Holmes - The equivalence of NF-style set theories with “tangled” type theories; the construction of $\omega$-models of predicative NF (and more), p:4-5]) can be written completelly without any reference to sequences, i.e. written only in terms of types.

In particular does the following theory have exactly the same axioms of $\mathsf{TTT}$?

Language multi-sorted FOL, with sorts (types) indexed by the naturals, equality symbol restricted to same type, while membership symbol restricted from lower to higher types, i.e. $x_i^n = x_j^m$ is well formed formula only when $ n=m$, and $x_i^n \in x_j^m$ is well formed only when $n < m$.

Extensionality: $i=1,2,3,\dotsc; j=0,1,2,\dotsc, j<i \\ \forall x^i \forall y^i: \forall z^j (z^j \in x^i \iff z^j \in y^i) \to x^i=y^i$

Comprehension: $i=1,2,3,\dotsc; j=0,1,2,\dotsc, j< i \\ \exists x^i \forall y^j ( y^j \in x^i \iff \phi ) $

where $\phi $ is a well formed formula in which $ x^i $ is not free.

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ You surely don't mean to ask whether your theory has the same axioms as another theory, when you have written it with different axioms. Theorems, maybe? $\endgroup$
    – LSpice
    Commented Jul 26, 2022 at 22:37
  • $\begingroup$ @LSpice, the stipulation of the original theory per sequences is that the asserted sentence is an AXIOM, so the individual axioms are actually typed axioms (wihout sequences), which I think are those of this theory, but I might be mistaken of course. $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 27, 2022 at 7:51

2 Answers 2

Reset to default
10
$\begingroup$

No it is not the same. The type sequences are absolutely needed, in some form.

--Randall Holmes (author of the theory in question)

The theory you describe is provably inconsistent.

The formula has to be the result of replacing the variables in an axiom of ordinary TST (indexed by type in the usual order) with variables of types determined using a strictly increasing sequence of TTT types. This is unavoidable. Finite sequences could be used in place of the infinite ones I use, but this is a complication, not a simplification.

Improve this answer
$\endgroup$
2
  • $\begingroup$ But $\sf TTT$ prove all axioms of this theory! For any naturals $i, j$ where $j<i$ we can always have a sequence $s$ such that $s(n+1)= i$ and $s(n)=j$, we substitute those in comprehension of $\sf TTT$, and we get the relevant instance of comprehension of this theory. So, if this theory is provably inconsistent, then so is $\sf TTT$ $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 27, 2022 at 7:46
  • 2
    $\begingroup$ @ZuhairAl-Johar: I don’t think that TTT proves all axioms of your theory — certainly, not all instances of your scheme are instances of the comprehension scheme of TTT as you claim. See my answer for a specific example. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Jul 27, 2022 at 10:44
7
$\begingroup$

As Randall Holmes’ answer already says, your comprehension scheme is more general than the comprehension scheme of TTT.

To illustrate this with a concrete example: Your scheme gives comprehesion for formulas like $$(x^1 \in y^2) \land (y^2 \in z^3) \land (x^1 \in z^3)$$ which is not allowable in Holmes’ scheme in TTT, since it isn’t “stratified” in the appropriate sense.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .