Timeline for Categorical foundations without set theory
Current License: CC BY-SA 2.5
10 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Jun 6, 2016 at 5:40 | comment | added | The_Sympathizer | (If completed infinities weren't used prior to 1870, then I don't think the basic calculus would change extraordinarily since it predates that quite a bit, but what about the more extensive field of analysis with all its set-heavy theorems?) | |
Jun 6, 2016 at 5:37 | comment | added | The_Sympathizer | Does rejection of completed infinity at all change how you do more elementary mathematics outside the esoteric world of foundations? Like does calculus change at all if you have no completed infinities? How do you do set-heavy things like analysis that looks to be a natural way to a complete beginner to them with no sets, that doesn't look either too complicated, contrived, or "handwavy" like you're trying to "get around something"? Furthermore, what is the precise reason to reject completed infinities, on purely abstract or logical grounds? | |
Mar 3, 2014 at 11:50 | comment | added | goblin GONE | @TomLeinster, consider an infinite page that begins with a finite set of strings written on it. There are rules that allow you to write more strings on the page, given that certain other strings are already written down. Then we can think of the set of all strings writable on the page as a (perhaps infinite) set. But in reality, at any one moment in time, there are only finitely many strings written down. Hence the aforementioned system (consisting of the paper and its rules) could be described as a potentially infinite set. | |
Dec 21, 2009 at 18:44 | comment | added | Tom Leinster | Paul, can you explain what you mean by a completed infinity? What's the difference between an infinity and a completed infinity, or between a completed infinity and an uncompleted infinity? I've never understood the meaning of this word. | |
Dec 21, 2009 at 16:22 | comment | added | Neel Krishnaswami | I just looked at the typing rules on your axioms link, and I now see that implication isn't a proposition-former. That's really cool! But you're right this is going off the track of the question, so I'll fall silent now. | |
Dec 21, 2009 at 15:33 | history | edited | Paul Taylor | CC BY-SA 2.5 |
corrected urls and one typo
|
Dec 21, 2009 at 15:29 | comment | added | Paul Taylor | Given that I have said that fibrations and first order logic are unnecessary complications, this is not the place to discuss ASD, let alone compare it with Formal Topology. It is an example of what I said above in that it is presented as a "type theory" (paultaylor.eu/ASD/dedras/asdaxioms). However, ASD seeks to capture the intuitions of computable general topology, whereas I believe the questioner wanted to know about alternative theories such as a topos that also capture the notion of a discrete collection. | |
Dec 21, 2009 at 10:02 | comment | added | Neel Krishnaswami | "...see toposes as being just as bad." Could I characterize ASD as a cousin of Sambin's formal topology or Simpson's reverse mathematics, in which you take some interesting mathematics (ie, real analysis), and then try to understand exactly which logical principles are necessary to make it work (where sets/toposes/HOL give over-abundant logical power)? | |
Dec 21, 2009 at 2:59 | vote | accept | CommunityBot | ||
Dec 20, 2009 at 16:01 | history | answered | Paul Taylor | CC BY-SA 2.5 |