When Cantor’s set theory – what we now call naive set theory – was shown to have problems in the form of Russell’s paradox, there were many different attempts to salvage the theory. In addition to the axiomatic approaches that we’ve looked at (ZFC and NBG), there were attempts by changing the basis of set theory – discarding sets in favor of something similar, but with restrictions that avoid the problems of naive set theory. Today, I’m going to talk about an example of the latter approach, called type theory. Type theory is a very different approach from what we’ve seen before, and one which is particularly useful and interesting to people in my neck of the woods.
What type theory does is create a new kind of collection object, called a type. The idea behind types is to create a stratification, similar to the idea behind ordered logics. In first order logic, you can only reason about primitive atoms, not about predicates. In second order logic, you can reason about atoms and first-order predicates, but not second-order predicates. And so on.
In type theory, you do roughly the same kind of thing, but you do it even more strictly. A first-order type can only contain atoms – primitive values that are not types. (Some versions of type theory call these ur-elements.) A second order type can only contain first-order types as elements. And so on. So type are strictly stratified: each level or stratum of types has members of the next lower stratum of types.
Using the basic idea above, of stratified types, we can define the simplest version of type theory, called ST, with a collection of axiom schema. For the axiom schema, there’s a convention in how they’re written. Each axiom makes statements about types of two levels: a base level, and its successor. Variables that range over types of the base level are written as lower-case letters; variables that range over the next level are written as lower-case letters followed by “‘”. So if “a” is a variable ranging over level n types, “b'” is a variable ranging over level n+1 types.
ST has 4 axiom schemas:
- Axiom of Identity: x=y ⇔ ∀z'[x ∈ z’ ⇔ y∈z’]: two values x and y are the same if and only if every type that contains x also contains y. It’s interesting to compare this one to set theory; it’s exactly inverse. In set theory, two values are the same if they have the same members; in type theory, two values are the same if they’re members of the same types.
- Axiom of Extensionality: ∀x[x∈y’ ⇔ x∈z’] ⇒ y’ = z’. This is very much the same idea as equality in set theory. Two types are equal as long as they have the same members. So in type theory, we get both the upwards and downwards properties of equality.
- Axiom of Comprehension: If φ is a first-order predicate, then: ∃z’: ∀x[x∈z’ ⇔ φ(x)]. Basically the same as the comprehension axiom of set theory, modified to include the stratification of types. It says that we can define a level n+1 type using a predicate over level n types.
- Axiom of Infinity: There exists a relation, “<“, which ranges over pairs of atoms, which is total, irreflexive, transitive, and strongly connected, such that ∀x,y[x≠y ⇒ [x<y ∨ y<x]]. The version of the axiom of infinity in type theory is a bear. Instead of being a direct construction like it is in ZF, it’s an indirect statement. What it says is that “<” is a total relation, which imposes a closed total order on the atoms. More, it requires that the domain and the codomain of < are the same: so if a value can appear on the right side of “<” (saying that there’s something smaller than it), it must also appear on the left side of “<” (saying that there’s something larger than it.) For this relation over the atoms to be possible, there must be at least one level 0 infinite type. So this does really assert the existence of an infinite type; but it does it indirectly, via requiring a relation which can only be satisfied by an infinite type. (Note: originally, I left “total” out of this definition; without totality, it doesn’t necessarily imply the existence of an infinite set! Thanks to commenters for pointing this out.)
If you look at this structure: atoms, stratified types, and the axioms, it should be clear that most of the things that we can do using axiomatic set theory can also be done in ST. You can’t mix things like x and {x} like you could in set theory, which does place some limits on you – but the fact that you’re allowed to have non-type primitive atoms goes a long way towards fixing that. The downside there is clear: while you can generally say the same things in set theory and type theory, the statements are often a lot more complex in terms of type theory.
Type theory is clearly more complicated than good old set theory. So what does that complexity buy you? Most importantly, it gets rid of Russell’s paradox. Since no type can contain members of its own type level, you can’t construct anything like “The types of all types that don’t contain themselves as members.”; there’s just no way of saying that. Axiomatic theory does the same thing – but it does it by, essentially, creating only two levels: proper classes and sets, and sharply limiting the ability to do reasoning about proper classes. Type theory restricts the structures you can build at any level, but by doing so, it allows to create a hierarchy of types, each of which is first class, capable of membership, and fully amenable to formal reasoning.
In addition, logic using type theory can be quite elegant. A lot of work in logic is done in terms of stratified logics, and type theory fits quite naturally with stratified logic. Plus, type theory and logic together are the basis of an awful lot of theoretical computer science. ST, and its more powerful children, form the basis of types in λ-calculus, which in turn is the source of the whole idea of types in programming languages. In fact, the parametric type system which was added to Java not too long ago has its semantics formally specified using a relative of ST.
Interesting article. I had been curious about this.
I think you missed something on the Axiom of Infinity, though. It looks like you’re only requiring
My comment got clipped for some reason; reproducing below.
I think you missed something on the Axiom of Infinity, though. It looks like you’re only requiring < to be a strict total ordering on all the atoms; but there are plenty of finite total orderings. Your explanation of how this actually does force an infinite class of atoms doesn’t wash; just because an object can appear on one side of a relation symbol, doesn’t mean that relation must ever be true. Thus there can in fact be a minimum atom, for example. There can even be an empty class of atoms; it occurs to me that the disjoint union of the finite levels of the Zermelo hierarchy would be a legitimate model of this theory.
Looks to me that there might be a connection between type theory, type hierarchies and partial order sets, lattices and such? I know you talked about these in the past. Am I right? Thanks for the post.
Chad:
The combination of the facts that the relation is total, anti-reflexive, and the domain equals the codomain that creates the requirement for infinity.
A value x is in the domain of “<” if and only if ∃ y : x<y. A value x is in the co-domain of “<” if/f ∃ y : y<x.
The above property of the domain and codomain can only be true if either the relation’s domain is infinite, or if the relation is cyclic. But the relation can’t be cyclic: the combination of anti-reflexive and transitive forbids cycles. So it’s got to be infinite.
So given these axioms for stratified types, could we define the Axiom of Reducibility as an extension to your version of the scheme? And if so, what would it look like? Reducibility is the one I never really understood…
Note that even in set theory two objects (necessarily sets, because that’s all there are) are equal iff they’re elements of the same sets. In the forward direction this is simply because set membership respects equality: if a in A and a=b then b in A. In the reverse direction simply consider the singleton set {a}, so a in {a} iff b in {a}, hence b=a. So there is nothing going on here that distinguishes set theory from type theory.
Which brings me to my main point, namely that there is no serious distinction between set theory and Church’s classical type theory, which is essentially what is being described here. It’s just a matter of style whether we present things using the notation and terminology of types, or the notation and terminology of sets.
However, there is an important distinction between set theory and the INTUITIONISTIC (aka CONSTRUCTIVE) theory of types developed by Per Martin-Loef. It is ITT, and not so much Church’s type theory, that has had such a profound influence on Computer Science, principally because the semantics of ITT is intrinsically computational, or constructive, in nature. That is, one starts with the concept of a program and develops mathematics on that foundation, rather than starting with a vague notion of set and working from there.
So is it fair to say that:
sets are to types
as
traditional email program’s folders are to gmail’s labels
? Thanks.
Hi Mark,
Granted that you are probably correct about ‘cyclic’ v ‘infinite’ in comment #4, let me present what I think may be an exception?
MOD(n) is probably an infinite helical function, bit most often is truncated in an illusion of repetitive loops appearing as a single cycle?
The combination of the facts that the relation is total, anti-reflexive, and the domain equals the codomain that creates the requirement for infinity.
These facts, along with the existence of at least 2 elements (which is missing from the axioms), would imply it. However, the only thing in Axiom 4 that would make the domain equal to the codomain is the statement that < is strongly connected, but there’s no such thing as a strongly connected, transitive, irreflexive relation. So there’s definitely a problem with your Axiom 4.
MOD(n) is probably an infinite helical function, bit most often is truncated in an illusion of repetitive loops appearing as a single cycle?
Since we’re discussing relations, not functions, I assume you’re referring to equivalence (mod n) here. This relation is neither anti-symmetric nor irreflexive, so it has nothing to do with the relation’s being discussed.
MOD(n) is probably an infinite helical function, bit most often is truncated in an illusion of repetitive loops appearing as a single cycle?
I have no idea what you’re saying.
Antendren,
A function is a relation!
I do not care if you do not understand.
Mark, #4: Ah, I see the problem now. I hadn’t seen the phrase “strongly connected” to describe total orders before, so I took it to mean “complete”. You’re right; as defined, the atoms at least have to contain a copy of the integers.
Anonymous, #9: I don’t think Mark means “strongly connected” as it’s applied to directed graphs.
The thing is, strongly connected as applied to relations doesn’t usually mean “domain = codomain”. It means exactly what Mark said in symbols, that is: ∀x,y[x≠y ⇒ [x<y ∨ y<x]]. How does that lead to domain and codomain being equal?
Why can I not have a set of atoms of size 2, called “a” and “b”, with a<b, and nothing else? That satisfies the irreflexive criterion, it trivially satisfies transitivity, and as written it also satisfies the strongly connected criterion. So what’s missing in the axiom? Is the domain = codomain bit supposed to be part of the axiom itself, and not something derived from the axiom?
I’ll note that the wikipedia page makes this same strange assertion – that is, that somehow being irreflexive, transitive, and strongly connected together requires domain = codomain. But how does my simple two-element system fail to be strongly connected? What are the replacements for x and y in the strongly connected definition that cause x≠y and yet neither x<y or y<x ?
Something’s missing here
I’ll note that the four axioms Mark quotes above are identical to the ones in Wikipedia, and Wikipedia claims to be giving the system found in Introduction to Mathematical Logic, 4th ed. by Mendellson.
In actuality, Google book search tells me that Mendellson calls the first axiom above a definition, and gives as the axiom of infinity (translated from three rows of symbols dense with quantifiers and variables):
There exists a binary relation on level 0 types that:
1) is non-empty,
2) is irreflexive,
3) is transitive, and
4) has every element of the range in the domain
Now, this clearly leads to requiring an infinite atom set. Note, however, that this does not require that the relation be strongly connected.
I can verify that the axiom of extensionality is identical to Mendellson’s book, but my google book search preview is missing the page that would give me the axiom of comprehension.
At this point, it looks as though wikipedia has screwed with the axioms for some reason, and Mark’s picked up the wikipedia-mangled version. I’ll note that this version of the wikipedia article (http://en.wikipedia.org/w/index.php?title=Type_theory&oldid=68142936), although short on the readability, appears to have faithfully reproduced the axioms. The way the axioms evolved on the page subsequently is like one giant slow game of telephone. (Except with only two players, repeatedly rewriting the text and slowly changing the meaning – 7 August 2006 was an interesting day for that article)
Daniel:
What’s missing is that “<” is total.
If < is total, that means that ∀x, &exists;y: x<y. If you have total, strongly connected, and domain=codomain, then it works.
Of course, in the process of editing, I managed to omit that. 🙂 An earlier draft had it, but I rewrote the paragraph on the axiom of infinity many times trying to make it clear, and managed to rearrange it right out of the definition. If you add the totality requirement back in where it belongs, then that form of the axiom works.
Incidentally, while I did look at the wikipedia article, it wasn’t my source for the axioms. A lot of wikipedia articles on math are excellent, but I’m not wild about their article on simple type theory.
I’m not entirely sure of what the exact source was – I’m using some old lecture notes, the Quine text, “Labyrinth of Thought”, plus several sources around the web, and by the time I’m done writing, I’m not even sure what came from where. I put together the axioms from several variants of the basic type theory axiom schema, trying to get them together in a form that was consistent and comprehensible.
1. Can you have w-level types in this system? (w standing for omega)
2. That’s not what I think of as type theory. To intuitionist or a functional programmer (and I am both nowadays), a type is a set together with a way to describe all of its elements. See “Naive type theory” (except it’s a pretty bad paper), Girard, etc.
Anonymous:
First: Yes, you can have ω level types. The type levels correspond to Ordinals. As far as I know, ω level types don’t particularly do much – they just contain values of type level ω-1 – but they can certainly be defined.
Second: you’re thinking of intuitionistic type theory, a la Martin Lof and Hindley-Milner. We’ll get to that – but we first need to be able to handle functions and such in basic set theory, which I’m starting on in another post.
(Anonymous above was me)
Actually, now that I think of it, all formulas in the version of type theory that you use have a “base type level”, which you denote by n. So it’s n+ω I should have asked about–and they can’t appear in formulas of finite length, of course.