What happened to Type Theory?

Probably the particular formulation of Russell and Whitehead became less used in comparison with the arguably more straightforward approach of axiomatic set theory.

Nevertheless, interest in type theories has continued. In the literature through the decades there are many kinds of type theories and variations of type theories representing different schools of mathematical and foundational thinking.

Possibly because simple ideas like "and" and "or" are defined as type, whereas set theory is not so bizarre. Maybe not.

Is there a way to resolve Russell's Paradox without resort to Type Theory? Can it be resolved by argument from the axioms of set theory?

For any relation R, it is a theorem of first order logic that:

There does not exist an x such that, for all y, Ryx if and only if ~Ryy.

In symbols:

~ExAy(Ryx <-> ~Ryy)

In set theory (with 'e' for 'member of' and taking R to be the membership relation):

~ExAy(yex <-> ~yey)

That is, there does not exist a set x such that, for all y, y is a member of x if and only if y is not a member of itself.

That is a theorem of set theory, as it is a theorem of first order logic for any R.

But how does set theory ensure that that theorem is not contradicted by having its negation also a theorem of set theory?

That is accomplished by not having axioms that would allow it.

In particular, set theory does not have the axiom schema of unrestricted comprehension (aka 'the axiom schema of comprehension' or 'the axiom schema of naive comprehension'), which is:

If P is a formula in which x does not occur free, then ExAy(yex <-> P).

If we have that schema, then we could take P to be ~yey, and derive Russell's paradox from:

ExAy(yex <-> ~yey).

Instead, Z set theory has the axiom schema of separation (aka 'the axiom schema of specification'). (NBG class theory, has a different but similar approach), which is:

If P is a formula in which x does not occur free, then AzExAy(yex <-> (yez & P)).

That says: If you have a set z, then you can form the subset x of z such that the members of x are all and only those members of z that have property P.

In other words, to use a property to define a set, you can only do it by using that property to make a subset of an already given set.

With P being ~yey, with the axiom schema of separation, we have:

AzExAy(yex <-> (yez & ~yey)).

And that doesn't yield a contradiction.

So set theory does not block Russell's paradox by adopting an axiom to block it. (In general, since the logic is monotonic, one cannot add axioms to block inconsistency.) Instead, set theory avoids Russell's paradox by refraining from having axioms that would allow it.

Note: Pedantically, instead of saying 'set theory ensures', we would say 'as far as we know, set theory ensures', since, as far as we know, set theory is consistent.

Thanks for your detailed and considerate reply, TonesInDeepFreeze. I need some time to digest it, as I'm a newcomer to this area of philosophy!

You are very welcome. I fixed some typos (including fatal ones) and added details and more explanation after you replied.

If you would like to have background to understand the details, then I can recommend a couple of books.

Reply to TonesInDeepFreeze Nice :up:

I'd appreciate it, I'd like to read up more on this topic area.

(1) Start by learning basic symbolic logic, which is the first order predicate calculus. The best textbook I have found is:

'Logic: Techniques Of Formal Reasoning' - Kalish, Montague and Mar

Supplement that with the best chapter I have found on the subject of mathematical definitions:

chapter 8 in 'Introduction To Logic; - Suppes

(2) Then basic axiomatic set theory. The book I like best is:

'Elements Of Set Theory' - Enderton

Supplement, if you like with:

'Axiomatic Set Theory' - Suppes

(3) Then basic mathematical logic. The book I like best is:

'A Mathematical Introduction To Logic' - Enderton

(4) The above book takes you through a proof of Godel's incompleteness theorem. After that, a more relaxing but wonderfully insightful read is a brilliant and beautifully written book for the layman on incompleteness:

'Godel's Theorem: An Incomplete Guide To It Use And Abuse' - Franzen

(4) At any point during this study, you can read what I have found to be the best general overview of the background for logic. That is:

the Introduction chapter in 'Introduction To Mathematical Logic' - Church

(5) If you like, you can put your toes in the water of other kinds of logic. An excellent overview is:

'An Introduction To Non-Classical Logic' - Priest

/

All of those books are widely used and considered to be authoritative. They will give you vocabulary and concepts that are common in discourse on logic and set theory.

This course of reading would arm you with a solid understanding that provides a foundation for more studies, if you like, at a graduate level that includes a panoply of rich and fascinating investigations.

In an earlier post, when I was editing, somehow I cut a part that is helpful about the axiom schema of separation. I added it back:

Quoting TonesInDeepFreeze

That says: If you have a set z, then you can form the subset x of z such that the members of x are all and only those members of z that have property P.

In other words, In other words, instead of using a property to define a set in an unrestricted manner, you do it by using that property to make a subset of an already given set.

With P being ~yey, with the axiom schema of separation, we have:

AzExAy(yex <-> (yez & ~yey)).

And that doesn't yield a contradiction.

Thanks for your help! My reading so far has been fairly haphazard. This should allow me to put some system into it.

Quoting Shawn

I'm interested in finding out what happened to Bertrand Russell's Type Theory?

Coming back as various forms of neo-intuitionism via the influence of computers and automated proof systems. See for example homotopy type theory.