Neo-logicism, set theory, and first-order Peano arithmetic
Addendum:
minor errata, I meant to say Russell type of argument instead of Cantor type. Did not list my "program" or the mathematical caveats needed to make it work either, cuz secret sauce B.
I get the feeling @naturalplastic you were trying to catch me for acting arrogant, or something like that. Did I read your mind, or am I off base? What sounds like arragonce to others is in actuality intellectually frustrated loneliness in me. You probably wouldn't understand unless you are a math wiz from an early age like myself who just does not get to talk with geniuses too much, cuz who does?
People write their ideas and it is just always feels like crazy levels of amateur hour level of thinking on practically every topic. I am booored out of my freaking skull with people. Forgive my petulance, I will do my best to keep it at bay.
Take care y'all!
_________________
Go Vegan!
I would agree that it does. And that Cantor's Omega (Absolute Infinite) is a beautiful number.
The imposition of types on sets does not solve the problem with sets though, it produces a new set theory with additional properties that enable more reasoning to be carried out but in turn reduces the domain of the theory. It becomes a proper subset of the more general untyped set theory, restricted to those bits of it that obey the strictures given by the type system.
I would agree that Cantor's uppercase Omega (Absolute Infinite) is a beautiful number, the Ein Sof of mathematics (was Cantor influenced by Kabbalah? Does a bear leave scat in the woods?), but aside from noting it for cultural reasons, that number is definitely not useful mathematically. The Burali-Forti paradox is the issue, forcing one to abandon the notion that a highest infinity exists.
Types do not solve all the problems associated with Sets, agreed, but strongly disagree that Types are just Sets in drag. We should consider each mathematical concept on its own merits. I think of sets as collections, types as formal specifications defined relative to "terms". Types are more about syntax versus Sets being about collections. I know that triangle man beats particle man (They Might Be Giants "Particle Man"), but Syntax Man beats Collector Man, so there!
Modern mathematical theory does not agree with your assessments la_fenkis. Homotopy Type Theory has uncountably infinite numbers of formally inequivalent Set Categories... For proof, consider the abstract of the following paper "Sets in homotopy type theory" by Egbert Rijke, Bas Spitters:
and thereby it includes (much of) the traditional set theoretical foundations as a special case.
Formally then, classical sets are subsidiary concepts to types. This is a much better conversation. The topic now has something worthy to debate about. Rehashing topics from a hundred years ago that people have moved on from seems like a waste of time in comparison...
_________________
Go Vegan!
Without reading the article I somewhat rankle at the presence of the words "much of," however without reading it I do not know exactly what of set theory is not encapsulated in homotypy type theory. It would at my initial glance however seem to say that classical sets are not properly subsidiary to types.
As far as your comment about Cantor and Kabbalah I've found that many scientists and mathematicians, even into the modern times have been heavily influenced by spirituality and religion. Perhaps it creeps into their notions from what was inculcated throughout childhood.
la_fenkis, the problem I had with what you wrote is that
it produces a new set theory with additional properties that enable more reasoning to be carried out but in turn reduces the domain of the theory.
Get rankled as much as you want, Types are a new way of looking at things. I am not sure if
Type < Set,
Type != Set, or
Type > Set,
I just find it odd, why would mathematicians be excited with HoTT if nothing fundamentally new was going on there as you imply? It makes little sense to me. An interesting document to consider is here.
Favorite part is
(homotopy type) theory = homotopy (type theory)
very Zen...
_________________
Go Vegan!
http://www.israelmgelfand.com/talks/gelfand_talk.pdf
Not directly related to your question, but given your interests, I thought you might benefit from this.