# Re: Is a function a relation?

Date: Tue, 23 Jun 2009 20:27:42 -0700 (PDT)

Message-ID: <0b967ffa-75ff-4155-af91-bc85b00c7c3e_at_a5g2000pre.googlegroups.com>

On Jun 23, 3:33 am, David BL <davi..._at_iinet.net.au> wrote:

*>
*

> It's not clear that type systems particularly help in this purist

*> mathematical endeavour.
*

My sense is that it doesn't.

> I note that the usual axioms of set theory

*> completely ignore any concept of type. I'd be interested to know
**> whether modern mathematicians that have researched type theory believe
**> it's important to mathematical foundations. My understanding is that
**> Russell only investigated type theory with the aim to avoid paradoxes
**> by preventing loops, but his work was made redundant by axiomatic
**> systems like ZFC which is believed to be free of paradoxes.
*

Certainly Russel's paradox is easily avoided by using a restricted form of comprehension. However every time I see it suggested that that was a particular motivation for Russel's work, it gets laughed at by those more in the know about math history.

An interesting paper on the question, which I bet you will like:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.7134

Anything by Leslie Lamport is worth reading. Even if he often flies way over my head.

Marshall Received on Wed Jun 24 2009 - 05:27:42 CEST