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 t1, …, tn are type symbols, then (t1, …, tn) 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
Rs(xt1, …, xtn),
then the simple type s of the predicate Rs must be (t1, …, tn).
The effect of this specification of type symbols plus the matching requirement is that some terms, like x0, can only occur in subject-position and never in predicate position. For example, y(0)(x0) is well-formed, but x0(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 (t1, …, tn), it is always the case that t1=…=tn, 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 (t1, …, tn) such that ti≠tj 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 z1, …, zn are type symbols (n≥2), then (z1, …, zn) 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 z1, …, zn are type symbols (n≥2), then (z1, …, zn) 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!