Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Category Theory Illustrated – Types

abuseofnotation.github.io

Post reply on HN
Print view View original

21–26 of 26 posts

Re: Category Theory Illustrated – Types

#21

Post by seanhunter »

igravious wrote: post #14
Koshkin wrote: post #8

> a set can contain itself Can it? > a term can have only one type... Due to this law, types cannot contain themselves Doesn't look like one follows from the other...

> > a set can contain itself > Can it? Yes -- in set theory sets can contain themselves > > a term can have only one type... Due to this law, types cannot contain themselves > Doesn't look like one follows from the other... types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them

> Yes -- in set theory sets can contain themselves

Hrbacek and Jech would like a word. It is very much not the case that in standard axiomatic set theory sets can contain themselves, precisely because this leads to things like Russell’s paradox. Sets containing themselves is generally prevented by the axiom of regularity. (Every non-empty set S contains an element wihch is disjoint from S) https://en.wikipedia.org/wiki/Axiom_of_regularity

> types are not sets and sets are not types

This is also not true. All types can be expressed as sets but not all sets are types in the standard definitions.

Re: Category Theory Illustrated – Types

#22

Post by seanhunter »

igravious wrote: post #15
igravious wrote: post #14

Earlier quoted context omitted.

> > a set can contain itself > Can it? Yes -- in set theory sets can contain themselves > > a term can have only one type... Due to this law, types cannot contain themselves > Doesn't look like one follows from the other... types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them

to justify my claim with an excerpt from the article: ““ What is type theory “Every propositional function φ(x)—so it is contended—has, in addition to its range of truth, a range of significance, i.e. a range within which x must lie if φ(x) is to be a proposition at all, whether true or false. This is the first point in the theory of types; the second point is that ranges of significance form types, i.e. if x belongs…

The modern formulation of functions as sets doesn’t require type theory but is entirely congruent with Russell’s definition, just much less cumbersome. In this view, φ is a relation on the set (D X C) where D and C are the domain and codomain of the function (which he calls the “range of significance of x” and the “range of significance of φ(x)” respectively). So since he’s talking about propositional functions, here C is the set {true, false} and D is all the things that are like whatever x is ie the set {x’: x’ is of the same type as x}.

Now a relation is just a particular type of predicate (ie it too is a set) so here we have x ~ y if φ(x) = y for all (x,y) in (D X C).

Notice here both the propositional function and the type are sets.

Re: Category Theory Illustrated – Types

#23

Post by jesuslop »

layer8 wrote: post #13
xanderlewis wrote: post #6

Earlier quoted context omitted.

Why is it ill-defined? As you said, there's no contradiction. Also, in the usual ZF set theory, it's empty.

It’s ill-defined in the sense that it doesn’t uniquely define the set. There are at least two different sets that D could be (one containing it and one not containing it), hence the expression doesn’t denote a well-defined set. (*) The axioms of ZF do not allow to form that expression, so the set doesn’t exist in ZF. (*) This is from a universist view. In a pluralist view, one wouldn’t say that the fact of the matter…

I think "Foundation" axiom F forbids your recursive set, and there are models of both core set theory satisfying either F or ¬F, so F is independent of core set theory (core -> not including F or ¬F). F is normally assumed in set theory, but Aczel has worked with "ill" founded (¬F) set theory models. Just as with the axiom of choice. No religion wars, just people pushed to be explicit with assumptions.

Re: Category Theory Illustrated – Types

#24

Post by Koshkin »

impact-basin wrote: post #12
Koshkin wrote: post #8

> a set can contain itself Can it? > a term can have only one type... Due to this law, types cannot contain themselves Doesn't look like one follows from the other...

I think you're taking this point a little too forcefully; this is meant to informally motivate Russell's paradox, in my reading - which is exactly the title of the section you're referencing. The point here is a little more subtle; category theory doesn't necessarily rely on sets; the definitions of categories that you often see (involving sets of objects and sets of morphisms) is more axiomatically forceful than the…

> category theory can use set theory, but does not depend on it

But aren't, say, the morphisms between two objects necessarily a set (termed "hom-set")?

Re: Category Theory Illustrated – Types

#25

Post by Koshkin »

mrkeen wrote: post #17
Koshkin wrote: post #8

> a set can contain itself Can it? > a term can have only one type... Due to this law, types cannot contain themselves Doesn't look like one follows from the other...

The system works according to its defined rules. In one system, a set can contain itself, in another system it can't. So it doesn't really make sense to ask 'can it?' If you allow sets to contain themselves, you also have to talk about sets which do not contain themselves, which yields Russell's paradox. If you disallow sets (or types) from containing themselves then you can't construct Russell's paradox, which is wh…

> In one system, a set can contain itself

But doesn't this lead to a contradiction (or to making the system of little use)?

Re: Category Theory Illustrated – Types

#26

Post by Koshkin »

igravious wrote: post #14
Koshkin wrote: post #8

> a set can contain itself Can it? > a term can have only one type... Due to this law, types cannot contain themselves Doesn't look like one follows from the other...

> > a set can contain itself > Can it? Yes -- in set theory sets can contain themselves > > a term can have only one type... Due to this law, types cannot contain themselves > Doesn't look like one follows from the other... types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them

> in the way you are linking them

This is what the text says, not me.

Post reply on HN