Recently, I submitted a paper on foundationless types. This suggested that it might be useful for others and fun for me to present the basic idea of foundationless types.

The foundational idea of (simple) type theories, that is, the standard well-founded sort, is the following (recursive) specification of type symbols.

- 0 is a type symbol (
*i*is also sometimes used). - If t
_{1}, …, t_{n}are type symbols, then (t_{1}, …, t_{n}) is a type symbol. - Nothing else is a type symbol.

Simple types also have a *matching requirement*, according to which type symbols of a predicate must ‘match’ those of terms it relates: in general, if we have a formula

R^{s}(x^{t}^{1}, …, x^{t}^{n}),

then the simple type s of the predicate R^{s} must be (t_{1}, …, t_{n}).

The effect of this specification of type symbols plus the matching requirement is that some terms, like x^{0}, can only occur in subject-position and never in predicate position. For example, y^{(0)}(x^{0}) is well-formed, but x^{0}(y^{(0)}) is an ungrammatical string: it violates the matching requirement. Just like there is a least natural number, there is a lowest type, 0, such that terms of that type cannot be predicates.

However, we can give a different (recursive) specification of type symbols such that there is no least type, just as there is no least integer. One upshot of this is that certain claims about cardinality of various types can be proven. For instance, in type systems that have a lowest type, we can usually only prove that the lowest type is non-empty. In a type system without a lowest type, we can prove that every type has at least 2 elements (we can actually prove more, as I argue in forthcoming work: this is just an illustration).

For some more detail, you might check out:

- Hao Wang’s 1952 “Negative types“
- Peter Azcel’s 1988
*Non-Well-Founded Sets* - Ernst Specker’s 1958 “Typical Ambiguity“

One caveat: the above authors, like many others, study type theories in which, in a type symbol like (t_{1}, …, t_{n}), it is always the case that t_{1}=…=t_{n}, so that a type symbol is always *homogeneous*. That requirement is not imposed in type theories that allow for *heterogeneous* types of terms, that is, type symbols (t_{1}, …, t_{n}) such that t_{i}≠t_{j} for some distinct *i* and *j*.

Finally, note that the foundationless types can also be recursively specified. First, note that **Z** can be recursively specified. Then we have the following (recursive) specification:

- For any integer z in
**Z**, z is a type symbol. - If z
_{1}, …, z_{n}are type symbols (n≥2), then (z_{1}, …, z_{n}) is a type symbol. - Nothing else is a type symbol.

A recursive specification of the type symbols z in **Z** can be had as follows:

- 0, 0′, and ′0 are type symbols.
- If z′ is a (“positive”) type symbol, then so is z′′.
- If ′z is a (“negative”) type symbol, then so is ′′z.
- If z
_{1}, …, z_{n}are type symbols (n≥2), then (z_{1}, …, z_{n}) is a type symbol. - Nothing else is a type symbol.

One can informally represent 0′ by 1, 0′′ by 2, and so on, and ′0 by -1, ′′0 by -2, and so on. The presentation is thus cleaner if we take integers z in **Z** to stand for type symbols without losing the recursive specification.

There you have it: a brief, er, *foundation*, for foundationless types!

“One can informally represent z′′ by 1, z′′ by 2, and so on, and ′z by -1, ′′z by -2, and so on. The presentation is thus cleaner if we take integers z in Z to stand for type symbols without losing the recursive specification.”

I assume you mean 0′ for 1, 0” for 2, ‘0 for -1, ”0 for -2 etc.

Note that although you’ve recursively specified the integers this won’t support recursive definitions of functions on the integers. This is because there is not a unique path to get any integer from 0. (E.g. 1 = 0’ = (‘0)” = ”(0”’) etc.)

LikeLiked by 1 person

Howdy Michael,

Yes, you’re right about what I meant. Thanks! – I fixed the typo.

One can get a unique path to any integer by imposing a two-part definition that splits type symbols by left or right marks on “0.” I figured this slightly duplicative definition would be easier (?) to read, but it’s probably worth putting in a non-duplicative version. EDIT: a non-duplicative version was added. Thanks for pointing it out.

LikeLike