4 ms·
As I understand this (which arguably I don't), what sets bring to the table (so to say) is a notion of unique identification That said, I wonder if it's at all
by bsedlm 5y ago
As I understand this (which arguably I don't), what sets bring to the table (so to say) is a notion of unique identification
That said, I wonder if it's at all possible to replace sets (to do all which is founded on sets) with a simple untyped lambda calculus (which I think is "functions at their most abstract") and then re-build mathematics on top of that?
I suppose the idea would be to define sets in terms of lambdas and then show all the set axioms etc...
This occured to me when I noticed that 'standard' set theory defines functions in terms of sets. If sets can be constructed (defined) in terms of lambdas (and types?), then yes to my own question.
- arjvik 5y agoI have no authority to write on this topic, but I think it's most definitely possible. After all, untyped Lambda Calculus is Turing Complete, so it clearly can represent sets somehow.
- carnitine 5y agoPull this thread far enough and it turns out the Y-combinator is a lambda encoding of Russell’s paradox.
- carnitine 5y agoThe untyped lambda calculus is inconsistent as a logic, hence you need some notion of types. Type theory is indeed building mathematics from lambdas, though.
- bsedlm 5y agobecause of the y-combinator|russell paradox? correct?? better question: any references to a type-based construction of set theory?
- anchpop 5y agoYou should read the homotopy type theory book if you’re interesting in things like this :p But to answer your question, there’s one here: https://arxiv.org/abs/1305.3835 https://arxiv.org/abs/1305.3835