From Set Theory to Type Theory

The expression A ∈ X does not denote a set, it is not of type set, it is a proposition and denotes a boolean. So actually not everything is a set because set theory is built upon the predicate calculus in which you have to have booleans. What is true is that the relation ∈ is taken to be one among sets, to keep things simple. Typing can complicate things. But keep in mind that really a relation is an operator (in this case from sets) to the booleans. So see there is already a bit of typing involved when you are going to do mathematics.

What he means when he writes

(Also, most material-set theories are extensional in that a material-set X is uniquely determined by knowing for which A we have A∈X. This is a natural assumption if ∈ is the only available notion.)

is that we usually have the following postulate (called extesionality)

(s = r) = (Ax: (x ∈ s) = (x ∈ r)) .

After that he gets really confusing trying to explain the use of the ∈ symbol in type theory. The important thing is that it is not a relation, or an operator, and A ∈ X is not a well-formed expression. Actually it is something that can occur in quantifiers, so you can write

(Ax ∈ s: x2 >= 0) .

And in that x ∈ s is not a subexpression anymore than x2 >= is a subrexpession. Sure they are substrings but they are not well-formed expressions. This differs from the use of the symbol ∈ as an operator when we write

(Ax: (x ∈ s) => (x2 >= 0)) .

the problem is mathematicians can be lazy and they might incorrectly render the previous formula as

(Ax ∈ s: x2 >= 0)
thinking there is no more room for confusion. Which there isn't among the experienced but completely leaves the logical but inexperienced students out in the cold.

Anyway I don't want to go on explaining his post but I want to make a comment. When I was really young I thought I hated mathematics because it promised to be logical but there were a myriad of things that did not make any logical sense. Only when I got what was meant was I able to appreciate it but consequently I really hate lazy formulae.

/r/compsci Thread Parent Link - golem.ph.utexas.edu