Timeline for Set theories without "junk" theorems?
Current License: CC BY-SA 4.0
40 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 20 at 19:45 | comment | added | Christopher King | You can get closer to this theory if you explicitly "close" it under interpretation. See mathoverflow.net/a/464547/65915 | |
| Feb 20 at 17:02 | history | edited | Christopher King | CC BY-SA 4.0 |
added 67 characters in body
|
| Sep 15, 2023 at 6:14 | comment | added | plm | [2/2] if "philosophical" means relative to the utility (in Mill's utilitarian sense) of a way of thinking (here thinking in terms of sets with common axioms), and "nature of these entities" means the psychological dynamics characteristic of their manipulation -for instance "sets" may relate to visual stimuli, seeing "real sets of objects", and our brain's dynamics mirroring those real objects' belong to their nature; then i think that studying only the philosophy/nature of sets eschews part (probably most) of that of defined objects, which may have their own (eg proof-theoretic) utility. | |
| Sep 15, 2023 at 6:11 | comment | added | plm | [1/2} Dear Andreas, This is very much how i conceive mathematics, with perhaps a personal tendency to remember "my" objects are sets in a definitional extension of ZF. I wonder though exactly what you mean by the first philosophical use: not having to consider the "nature" of defined objects. It seems to me that on the contrary there is a slight problem with considering sets as so fundamental: it obscures the reasons to choose sets as most practical foundation, best suited to human (mathematical) reasoning, in our social context. I'm not sure what you mean by "philosophical" and "nature": | |
| Mar 25, 2018 at 14:11 | comment | added | James Smith | About point four. If A constitutes B, then B is constitutive of A. I hope you appreciated my formal definition! Alternatively, a good definition Google returned is 'having the power to establish or give organised existence to something'. My point being, if you want to prove anything about T then, well, best start with T! And on the last point, I think we will have to agree to differ, but that is half the fun. | |
| Mar 25, 2018 at 14:05 | comment | added | James Smith | Your third comment is really enlightening, thank you. I'm glad to know there's more to modern set theory than foundations! Of course so many mathematical things are sets with additional structure, I don't need to tell you this, but it still wasn't obvious to me whether set theory would influence, say, topology. Again, it's good to learn that it does. | |
| Mar 25, 2018 at 14:02 | comment | added | James Smith | ...very basic set of axioms that to be common seemed common sense, and since moreover it appeared that everything could be encoded as a set (please forgive the usage), it become the de facto standard, as it were. Anyway, so I was told. Tom Körner once wrote that a glance at any maths textbook will convince that mathematicians make lousy historians. I would go so far as to say that you don't even have to glance at a text book! | |
| Mar 25, 2018 at 13:58 | comment | added | James Smith | @AndreasBlass Thanks so much for replying, it's more than my disjointed comments deserved. And I'm glad they were taken in the right spirit. You have a point about connectedness. Another mathematician in fact clarified the historical situation for me a few weeks ago. He said, in brief, that until set theory came along mathematics was indeed disjointed. Geometry had its own axioms, for example, going back to Euclid, and I think he gave two other areas that were in a sense solid but apart. I think the point was that when set theory came along, since it brought with it a... | |
| Mar 24, 2018 at 22:01 | comment | added | Andreas Blass | (4) I agree. You're a confirming instance of my claim that "mathematicians generally reason in" T. (5) I see no reason why the properties of a theory should be best done in the language of that theory. My nearest dictionary gives no meaning for "constitutive" that would support the claim that all properties of T must be constitutive of T, but I admit that "constitutive" may have a technical meaning in philosophy that I don't know and that would support your claim. Finally, concerning $1\cap2$: ZFC proves some statements that are not the interpretations of statements in T's language; so what? | |
| Mar 24, 2018 at 21:54 | comment | added | Andreas Blass | (3) For many set theorists, including me, the most interesting parts of set theory are not its foundational aspect but rather (a) its role as a mathematical subject in its own right, sometimes called "infinitary combinatorics and (b) its applications to other fields of mathematics. Applications to real analysis were part of Cantor's motivation for developing set theory in the first place, and applications have long been ubiquitous in general topology. More recently, other fields, like abelian group theory and C*-algebras have used a lot of set theory. | |
| Mar 24, 2018 at 21:50 | comment | added | Andreas Blass | (2) Inertia may have something to do with ZFC being the standard (nowadays) foundation for mathematics; it takes a lot of work to show that a proposed foundation works, and once the work is done for one foundation, there's less motivation to repeat it for others. I'm not sure mathematics is really more connected now than 100 years ago. New connections have indeed been found, but also new areas have developed, and I"m not sure about the trade-off between these two phenomena as far as the overall connectedness of the subject is concerned. | |
| Mar 24, 2018 at 21:46 | comment | added | Andreas Blass | @JamesSmith I"ll try to briefly answer your five comments, in order. (1) "Interpretation" has a standard meaning in mathematical logic, and that's what I intended. Essentially, it means that all the primitive notions of one theory (like T) are expressed in terms of the primitive notions of another theory (like ZFC) and all the axioms of the former theory thereby become theorems of the latter. You can call it "encoding" for conversational purposes, but "interpretation" conveys the precise technical meaning for logicians. | |
| Mar 24, 2018 at 17:08 | comment | added | James Smith | Finally, I wonder about the assertion that you can prove anything about T by encoding it in ZFC. Surely all of the properties that T possesses must surely be constitutive of T, and proving things about them, or any other formal endeavour do to with T, is best done in the language of T or formalisms that are based on it. At best you will get the same results from ZFC, at worst you will get, well, as the OP suggested, the 'j' word. Unfortunately, $1\cap 2$ does not equal $1$. | |
| Mar 24, 2018 at 17:03 | comment | added | James Smith | Generally I think the "everything is a set" belief is just that and that T, whatever exactly we take T to be, can be treated on its own without the need to encode it as anything else. I would say that "everything is what it is". There is no need for example, to encode zero as the empty set, we can simply have a term called zero and leave it at that. Similarly, there is no need to encode mathematical objects as tuples. We can just define group as a type with two properties. | |
| Mar 24, 2018 at 17:00 | comment | added | James Smith | ...My point is here not to disagree with that justification, at least not now, but to ask the question, what is the value of set theory if ZFC is not taken as a foundation for T. I mean, are set theorists primarily only interested in such meta results, or does modern set theory have a place and a purpose outside of this remit? I have thought of asking such a question on MO at times and wonder whether anyone can enlighten me. | |
| Mar 24, 2018 at 16:54 | comment | added | James Smith | Also, justifications for encoding T in ZFC are always a little shaky. Many, including me, would say that the main justification is just a kind of historical inertia. Set theory provided a unifying foundation for mathematics well over a century ago now at am time I am led to believe when mathematics was not the connected whole it is generally perceived to be now. To go back to your other justification, namely that encoding T in ZFC affords meta-mathematical or meta-logical properties of T to be proven is something I have often wondered about... | |
| Mar 24, 2018 at 16:53 | comment | added | James Smith | A couple of things. I think to say that your theory T is encoded in ZFC is better than to say that is interpreted, indeed I am not quite sure what interpreted means in this context (although this is probably just ignorance on my part). Nonetheless, to say that we encode zero as the empty set is better, because this is precisely what is being done. | |
| Mar 7, 2018 at 4:35 | comment | added | dfeuer |
@TobyBartels, perhaps it would be better to discuss that in a typed context. In a dependently typed language, the equality test can reveal (at the type level) that two things are not equal. As long as you only write 1/x in a context within which that information is available (typically under a pattern match), there is no difficulty whatsoever.
|
|
| Mar 15, 2017 at 6:08 | comment | added | Toby Bartels |
@user99916 : This business about A(x) and B(x) not only can be formalized but has been in some programming languages such as C. You can even write if ((0 == 1) && (1/0)) … and the division by zero will never be executed. Obviously, that's a silly example, but if the B(x) is a routine that might never terminate (or just might be terribly inefficient), as long as A(x) is only true in those cases where B(x) is fine to use, then you can write it that way.
|
|
| Nov 30, 2016 at 2:17 | comment | added | Danielle Ulrich | @AndreasBlass This is a minor quibble, relative to your main argument in the post, I realize. | |
| Nov 30, 2016 at 2:13 | comment | added | Danielle Ulrich | @AndreasBlass My point was just that this does seem to impose a limitation on how people do math, or at least think about it. | |
| Nov 30, 2016 at 2:03 | comment | added | Andreas Blass | @DouglasUlrich If you wanted to introduce $V^*$ as a new sort, then you'd specify it with suitable axioms (a non-degenerate bilinear pairing with $V$), rather than constructing it as a space of functions. The space-of-functions description would then serve not as a "reduction" of $V^*$ to other sorts like sets or functions but rather as a proof that the new sort and axioms are conservative over the previously available theory. That would be a perfectly reasonable view of dual spaces, but it seems not to be what mathematicians usually do. | |
| Nov 30, 2016 at 1:58 | comment | added | Danielle Ulrich | @AndreasBlass Perhaps I am misunderstanding, but I thought part of what you were saying was that every vector space had to consist of urelements. The phrase I am looking at is "There are no axioms that attempt to reduce one sort to another" am I misreading this? | |
| Nov 30, 2016 at 1:55 | comment | added | Andreas Blass | @DouglasUlrich I see no difficulty in constructing dual spaces in $T$. Just take the construction as written in any standard textbook, and as summarized in your own comment. Note that T includes sorts for sets, functions, and the like --- all the stuff you need to build dual spaces. | |
| Nov 30, 2016 at 1:28 | comment | added | Danielle Ulrich | @AndreasBlass I object that most mathematicians work in this theory $T$. For instance, in linear algebra, suppose we have a vector space $V$ over $\mathbb{R}$, and we wish to define its dual space $V^*$, Naturally we take this to be a vector space with underlying set all linear functions from $V$ to $\mathbb{R}$, and we endow it with vector space structure in the usual way. There are many other examples. It's not clear how this would work in your theory. Perhaps instead most mathematicians work in $ZFC$ with expansions by definitions, and just ignore the resulting "junk theorems?" | |
| Nov 28, 2016 at 18:57 | comment | added | Terry Tao | The use of a set theory encoding is always an option in T for the purposes of showing that a concept one is trying to introduce is in fact well defined. But one can also do so in other ways (basically by demonstrating existence, uniqueness, and independence from temporarily introduced parameters such as coordinate charts). T doesn't reject set theory, but rather it gives working mathematicians the freedom to use it or not use it depending on the application and on the mathematician's aesthetic tastes. | |
| Nov 20, 2016 at 16:42 | comment | added | user99916 | @TerryTao: You say "if one wishes to be rigorous in T, one has to go through the exercise of verifying that the definition of a pseudosmooth widget in Definition 5.7 is indeed "well defined" (which one can do either via a set theory encoding, or by …)" Why should one use a set theory encoding when working in the theory T? Isn't T intended to not involve such unnatural encodings? | |
| Nov 19, 2016 at 18:23 | comment | added | user99916 | @TerryTao: For example on the type of ordered pairs one can define a predicate "isGroup" that says that the first component is a set, and the second an operation on that set, such that the group axioms hold. Thus there should be a type of all groups, so that we can say "For all groups ..." and don't have to say "For all ordered pairs, if this ordered pair happens to be a group, then ...", because this would be unnatural, right? Also, the integers are a type and "even" is a predicate on the integers, thus "even integer" should be a type. | |
| Nov 19, 2016 at 18:22 | comment | added | user99916 | @AndreasBlass: Another feature of natural language I don't know how to formalize is that for each type/sort $S$, and every predicate $P$ on that type, one expects that there is a type of all the objects $x$ of $S$ that have the property $P(x)$. | |
| Nov 19, 2016 at 11:55 | comment | added | user99916 | @AndreasBlass, Terence Tao: A problem I see that could occur when formalizing $T$ is that in natural language we humans say something like "A(x) and B(x)" where B(x) only makes sense if A(x) is true. Thus we "A(x) and B(x)" consider to be false if A(x) is false, even if B(x) is meaningless in this case. It's hard for me to imagine how one can formalize these features of natural language in a formal system. | |
| Nov 19, 2016 at 11:26 | comment | added | user99916 | @AndreasBlass: A second question: Do you really think that mathematicians generally work in $T$, or is $T$ just supposed to be the natural choice of a formalization of the real informal theory in which mathematicians generally reason? | |
| Nov 19, 2016 at 11:18 | comment | added | user99916 | @AndreasBlass: Are you sure that $T$ is gonna be a many-sorted theory rather than an order-sorted logic? Wikipedia: "While many-sorted logic requires two distinct sorts to have disjoint universe sets, order-sorted logic allows one sort $s_{1}$ to be declared a subsort of another sort $s_{2}$". I think that for example, the type "integer" should be a subtype of "real number". And every type should be a subtype of the type "object", so that we can have a relation $x\in M$, where $x$ can be any object, and $M$ has type "set". | |
| Oct 27, 2016 at 1:34 | comment | added | Terry Tao | Another source of dynamism is the use of iterative algorithms (e.g. greedy algorithms) in which a number of variables are dynamically updated a finite, infinite, or transfinite number of times until some halting condition is reached. One can formalise this statically of course, by introducing a time parameter and making everything in the algorithm a recursively defined function of that time parameter, but it can often be quicker and more conceptual to instead give dynamic pseudocode for such an argument. | |
| Oct 27, 2016 at 1:32 | comment | added | Terry Tao | Some of the dynamism of T can (and should) be thought of this way, but not all. For instance, it is convenient in T to "abuse notation" by identifying an object with another object of a different type, e.g. identifying a group $(G, 1, \times, ()^{-1})$ with the set $G$, identifying a scalar constant $c$ with the constant function $f: x \mapsto c$, and so forth. | |
| Oct 26, 2016 at 20:35 | comment | added | LSpice |
@TerryTao, surely one is better off thinking of this dynamism as being of the form let x :: Real in …; let x :: ManPoint in …, with the understanding that we are only ever temporarily binding $x$ locally to some (often ill specified) block, rather than constantly rebinding an already permanently bound $x$?
|
|
| Mar 9, 2014 at 16:11 | comment | added | Terry Tao | ... although of course, if one wishes to be rigorous in T, one has to go through the exercise of verifying that the definition of a pseudosmooth widget in Definition 5.7 is indeed "well defined" (which one can do either via a set theory encoding, or by checking "consistency", "uniqueness", "coordinate independence", etc.). And so on. All this is already hard to formalise in standard first-order logic (with static variables, etc.), let alone in standard FOL+ZFC. But it would be extremely crippling in practice to give up these features of T when trying to prove a new mathematical result. | |
| Mar 9, 2014 at 16:07 | comment | added | Terry Tao | I'd like to add one additional remark to this excellent answer: the theory T is not only many-sorted, but extremely dynamic. A variable $x$ may have the type of a real number in Section 3 of a paper, but the type of a point on a manifold in Section 6, the type of an indeterminate algebraic variable in Section 10, and undefined in all other sections. The notion of (say) a "pseudosmooth widget" may be an undefined type until Definition 5.7, at which point it suddenly becomes a first-class mathematical object (and all the previous axioms of T are now assumed to apply to it). ... | |
| Mar 12, 2012 at 2:36 | comment | added | Jacques Carette | Indeed, that is a wonderful answer. Thank you for posting it, it really does add something new. I wish that, as OP, I could upvote more than once! | |
| Mar 11, 2012 at 23:08 | comment | added | Asaf Karagila♦ | No need to apologize for this second, and wonderful answer. +1! | |
| Mar 11, 2012 at 22:37 | history | answered | Andreas Blass | CC BY-SA 3.0 |