Set Theory and Algebra in CS: Introduction to Mathematical Modeling (2013) [pdf]
pdfs.semanticscholar.org
pdfs.semanticscholar.org
In the context of a RDBMS, SQL is a domain language for expressing the underlying Relational Algebra:
https://cs.ulb.ac.be/public/_media/teaching/infoh417/sql2alg...
[1] https://en.wikipedia.org/wiki/Relational_model
So the “application” for set theory you want is point-set topology, and the “application” for point-set topology is analysis, or further down the road all sorts of modeling used in physics and engineering and so on.
Here’s a bit of a history lesson by Rudin, https://youtu.be/hBcWRZMP6xs
If you want to get a sense of the historical fights involved based on an analogy, see Lakatos’s Proofs and Refutations https://math.berkeley.edu/~kpmann/Lakatos.pdf
edit: but that is a nice paper you linked to. thank you.
What about where set theory interplays with model theory? Would it surprise you to hear that the dizzying towers of infinities that can be spoken of in ZF can be modeled by a merely countable universe? What about a computer program (albeit an impractical one) that decides whether sentences about the natural numbers with successor are true or false, whose existence is discovered by proving that large uncountable models are isomorphic?
To be clear, it's okay to be bored by this stuff. I tend to get bored pretty quickly when people start talking about systems of DEs or eigenvectors, or really much of anything that looks too much like calculus, and I'm not about to apologize for my apathy for those things. But most of the above stuff tends catch the attention of even the humanities types, who are easily deterred by most mathematical topics.
Out of curiosity, I might ask whether you're similarly bored by computability theory or complexity theory, which leverage many of the same tools as those used in set theory (mappings as preorders, diagonal arguments, etc), but add computable enumerability/uniformity/syntacticity requirements to the mix.
But if mathematicians’ convention is that they will refer to ZFC when writing their proofs about something else I am interested in, I am willing to humor them, and keep my caveats to myself.
I’m reasonably well convinced that most models mathematicians can make in the context of ZFC which have any real-world implications (e.g. accurately simulate some physical phenomenon) could be alternately proved under some more restrictive set of axioms, just sometimes with a lot more hassle.
Why?
But it doesn’t really matter what I think. This is not a fight I care about. It’s like arguing with Buddhists about the nature of suffering or something.
YMMV.
[1] https://math.stackexchange.com/questions/315399/how-does-zfc...
What do you find hand-wavy or circular about it?
Can you specify which absurd implications you're referring to?
Not trying to argue, just genuinely curious.
If mechanical reasoning is not something that interests you, you have little use for these pedantic systems. Mechanical reasoning has two current uses: 1. mechanical verification of mathematical proofs and assistance in such proofs -- this application is very rarely used in practice, and is commonly the domain of a few enthusiasts who hold high hopes for improvements that would make it more mainstream. 2. Mechanical verification of software, including static analysis, model checkers, type systems and other software-relevant proof systems.
"There's the other possibility: set theory is completely irrelevant to physics... That's almost more interesting because if this conjecture is true, we've argued there's truth here for set theory, and it's a truth that's not about the physical universe. To me that's almost more remarkable, that there could be some conception of truth that transcends truth that we see around us."
The presentation is called The Continuum Hypothesis and the search for Mathematical Infinity [2].
Obviously, professional set theorists go way beyond what is described in this document, but to be honest, none of that more advanced stuff seems very useful to me in practical applications in technology.
I wondered the same thing. The first half of the linked paper is usually contained (if abridged) in the intro chapter of more or less any algebra/topology/analysis textbook. I don't remember Rudin's first book being an exception. Most of that material can be found in the first chapter of Rudin's "Principles" (3rd edition).
I'd say the basic topology in R^n is much more abstract (the 2nd chapter of Rudin "Principles" [3rd ed]) and it's not treated in the linked doc.
So: all kinds of typed programming languages with non trivial features being effects (monads&modalities, linear logic), structuring/interfaces (parametrized modules, type classes, translucent types, ..) or interactive theorem proving.
I think one of the problems of set-theory and applictions is that it doesn't lend itself very well to computers. An immediate thought was software verification & theorem proving, but while it's used in modelling (for example Peano Numbers), the underlying theories should (all?) be type-theories.
But that's something i am definitly not an expert in. Maybe someone with real knowledge can help answer this!
Of course everybody interested in math & it's applications should know really basics set-stuff. But I think, while foundational, set theory is just not that important to be super proficient in! You could write all the required stuff on a single sheet of paper.
I might be misunderstanding what you mean here, but I'm confused by this statement. Set theory is used very often in computer science. Relational databases are essentially applied set theory.
My (not entirely informed) sense is that constructive mathematics would have more success if more of an effort was made to pose it as a readily instantiable, tagged embedding within the larger classical mathematical corpus. Less Brouwer-style dogma about LEM being "wrong", more emphasis on streamlining a pathway for results to travel from the mathematical journal literature into software design specs.
LEM is not wrong, it's just not always true. You must be familiar with the fact that AC is not provable in ZF, as such isn't LEM kinda philosophically wrong for AC? Not forcing LEM to be true is useful to have a better (more generic) understanding of complicated things. In general restricting logics (eg linear logic, constructive logic, etc) is only making them more powerful: we are able to express more propositions and we can internally (or externally as in linear logic with `!`) define the fragment for which the old axioms were valid. Pure languages enable explicit talk about computation, linear languages enable explicit talk about memory. Restriction are about increasing expressivity and most of we time we build them in the way that they retain the same proof-theoretic power.
How many of these results require applying the LEM to undecidable propositions? The LEM works fine in constructive logic for provably-decidable propositions.
For what it's worth, Haskell has very little to do with actual category theory. Even though terminology like "monad" is used, Haskell doesn't have much more overlap with higher mathematics than any other programming language. Mathematicians working on category theory and software engineers working on Haskell don't have much overlap at all.
This is kind of frustrating because it's a meme that Haskell is very mathematical. It borrows concepts from category theory, yes. But it's not anymore mathematical than calling a GET request "idempotent" is mathematical.
I didn't say haskell is mathematical (and i do agree to your point), i said category theorists probably know haskell of all languages because of the deeper understanding/intuition they will naturally have for it. There is no denying that haskell is laid on category theory foundation and that understanding these will help you. But of course well designed things do not require you to understand their foundations to build intuition/understanding.
The idea that Haskell has much to do with mathematical category theory is a meme that arises from the cargo cult of functional abstraction. It's an example of terminology overloading. There is this pattern of taking terminology from abstract algebra and category theory and using it to describe design patterns in functional programming or certain paradigms of engineering. "Monad" is one you see in Haskell which ostensibly makes it related to category theory. Another example is the idea of an "isomorphism" in web development, which doesn't mean the same thing as it does in algebra.
There's no problem with using terminology borrowed from mathematics for design patterns in engineering (and vice versa), but it should be transparent about the fact that it doesn't confer any special relation to the underlying mathematics. A category theorist and a Haskell programmer have different conceptions of what a "monad" is, and any functional design pattern modeled after an idea in category theory is going to be covered in the introduction or first chapter to a textbook. The language has more to do with lambda calculus than it does anything in actual category theory.
can you elaborate here? what is a mathematical hipster, and what are “new frameworks”? and what do you mean by algebra “dropping all models”? i am confused by what these mean.
algebras are about studying various means of combination. given some set, how can we combine two things from that set to get another thing in the set? what are the structures that arise as we explore that question? i highly recommend reading the expository chapter one of pinter’s abstract algebra book.
For that matter you actually don't need a lot of this machinery to derive analysis; for that all you need is a minimal subset (hah!) of set theory. Analysis focuses on the properties of continuous things, like real and complex sequences. You can derive the real and complex numbers axiomatically (like with Dedekind cuts of rationals) or synthetically (field axioms) as long as you have the definitions of sets, subsets, bounds, unions and intersections. I'm not even sure you need to care about the distinction between a subset and a proper subset.
That's not to say the material presented here isn't useful - it is. I'm just making the point that most analysis doesn't require abstract algebra aside from fields and (later on) vector spaces, and you don't need a whole lot to get there.
My favorite critic of ZFC is Norman Wildberger, who has a great YouTube channel. I found his formulations of complex multiplication, the pythagorean theorem and quadratic forms were particularly worthwhile, even though he comes off as barely computer literate in other videos.
But no, seriously, it depends on what kind of set theory you're talking about. The stuff Hilbert was arguing about up to the stuff still being argued about today in the ivory tower? No, you pragmatically do not need to know that unless you're pursuing a research career in pure math. The stuff in an undergrad probability course? Yeah, sets come up basically everywhere if you're looking and are willing to think like that.
Modern pure mathematicians benefit from being able to conduct most of their reasoning on the lower footsteps of the von Neumann hierarchy (V_{omega + k} for small k), where they get access to higher-order tools like function spaces and topologies, countability as a fruitful property to impose and work with, and a playground where most of the disparate branches of mathematical research can be brought together without worrying about bindings between underlying frameworks. None of these things require a deep knowledge of the metamath of ZF to work with, but they'd all make many 19th-century mathematicians nervous.
Note also that the most frequently used tools of naive set theory today (e.g. unions/intersections, separations/replacements, powersets, cartesian products/relations/functions, a few notable infinite sets) roughy mirror ZF. That shouldn't seem like an accident. Having working mathematicians trained to think and organize their work in these constructs keeps them around those lower footsteps.