I don't see anything there that's incompatible with a high level of skill at mathematics. Honestly, I don't know of any opinion outside the realm of mathematics that could be deluded or disorganized enough to make me think that the person holding it couldn't be competent at math. That said, before I trusted this web site as a source I'd look for evidence that it has been reviewed and improved by other people, because even a competent person is bound to make mistakes, and if he's working entirely alone his mistakes are likely to go uncorrected.
the whole thing you linked reads like he is going through some existential crisis triggered by spending too much time in his own head, or he is struggling to find himself. he calls others stupid but that might just be due to feeling misunderstood and a symptom of his alienation.
one thing I learned is that knowing more doesn't make us happy. knowledge can be the key that opens a door to insanity.
whether he is a lunatic or genius is hard to say without evaluating the quality of his work.
> But there are still many well-placed people who will never listen, cannot grasp this and that keep denying the right for young geniuses to decide for their own life.
This obsession with I am a genius is bordering on pathological narcissism, excluding oneself from the society because one's too smart to be understood by the world is a very dangerous slippery slope. On the other hand, while in a healthy way, I applaud when one sticks to their own ways. I just wish humility was mode widely practiced. We are not gods, we're just some creatures that have varying degrees of intelligence, but nothing special.
Good luck to you young thinker but remember we are to enjoy this life and the people around us. Don't be lonely and miserable trying to prove everybody wrong, it's pointless.
The major red flag is in the "misunderstood genius" part -- 99% of the people I've ever seen with a claim like that haven't interacted with things enough to have been able to truly test their claims. "Genius" is only "misunderstood" when the person laying claim to it does not do enough to substantiate their argument.
Here, I read some of what they had to say about "infoliberalism" -- the immediate issue that I have with their position is that they make some kind of claim that a few participants in it would naturally lead to a revolution. They then go on to claim that the system is completely decentralized, but also complain that not one other person is willing to join. If their system were truly decentralized, and also something that would provide significant benefits to participants over the existing social/economic/political order, why is the number of practitioners exactly one? All of this screams quackery.
I think "mentally ill" is pretty unfair. Passionate, depressed, maybe even self-righteous? Sure, all of these.
But his capacity for logic doesn't seem to be affected. English isn't his first language, but he still writes in full, grammatically correct sentences that are very clear. Wordy and emotional - yes. But not mentally ill.
I think we should be careful not to dismiss/overlook people because we don't share their emotional perspective on the world. In other words, just because he's a unique character doesn't mean his take on set theory should be ignored.
From a very brief click through (and from my own fairly superficial memory of the topic), it doesn't seem to be extremely unconventional. At the very least, it's not standing shoulder to shoulder with Timecube.
The author is evidently far from neurotypical. Generally I find these kinds of diverse viewpoints interesting, if not appealing.
Unfortunately his prose borders on unreadable. There may very well be excellent ideas here, but until he follows the commandment "omit needless words" nobody is going to wade through it.
He's definitely angry, but from skimming it, it sounds like he had some ideas, put them out there, and no one bit.
And he's uspet that it didn't pan out, and he's quite clear on a fairly reasonable, if hyperbolic, explanation of why the ideas didn't work.
I read it as him coming to grips with the common blind spot of "my ideology would work just fine except for all the people who don't hold my ideology". You hear it from proponents of all major ideologies; liberalism "they're on the wrong side of history", conservatism "what happened to common sense?!" and libertarianism "but in a libertarian society..."
His stuff is ranty and tone-deaf, and he probably shouldn't include it on a page on set theory, but he's not delusional.
For all of the political ideologies you listed, we have concrete examples of societies which trend in those directions. Sure, most real societies do not trend toward radical versions of those ideologies, but at least we can each get an okay sense of the first derivative, so to speak, of "goodness" with respect to variation in political leanings.
Correct me if I'm wrong, but it doesn't seem like anything like "Infoliberalism" has ever been tested (and the author even _says_ as much). Before jumping on the boat of a radical political ideology, I'm sure that any reasonable person would at least like to have an _idea_ of what it leads to.
Yeah, I broadly agree. But I think a person can only be radical if they disregard normal social inhibitory / moderating influences. I'm reluctant to write him off as delusional because I'd have to write off most activists. And he's pretty clear that he's aware that he's behaving out of the bounds of polite society, and he's taking his ideas to their logical conclusion.
And I think for any new idea that is non-trivial, whether it's a new ideology, business plan, or whatever, a reasonable person also has to admit the only practical way to figure out if a thing works is to do it.
Yes, I absolutely agree with your second statement. However, the issue I take with the author is that they say that they are not a programmer, and they're frustrated that they cannot get a programmer to help build a prototype. Being _frustrated_ that people won't work for you _for free_ is delusional. The author could have also decided that their idea was worth enough to them to _learn_ how to program, so they could build a workable prototype, and possibly attract other developers as part of an open source project. However, the author seems more content to just sit there and complain about being "misunderstood." Implementations typically are worth a lot more than ideas, and this is exactly what the author doesn't seem to get.
Eh. Donald Knuth is Lutherian. I'm atheist and I believe it is unscientific and deluded to believe in things from an ancient book of fairy tales.
This doesn't discount Knuths' major contributions to the field. No one is perfect. Even the most logical, intelligent person could have aspects of himself that are illogical.
If the OP's set theory stuff is good, I wouldn't let his emotional rants affect my judgement of this.
I had a seminar on set theory and the foundations of mathmatics. It was very fun! But, coming from a computer science background, i found the foundations via set-theory unintuitive and a bit ackward to work with.
I know there are some type-system based approaches, how do they turn out in practice? How nice are they to work with "on a low level"?
Type theories, especially dependent type theories a la Martin-Löf, are quite natural to work with. They are easier to implement on a computer, and there are active communities around several such implementations (Agda, Coq, Lean,⋯).
Most computer verified proofs are implemented in systems based on type theory, not set theory. Most of the time you do not need sets of sets of sets… You want types whose elements are the mathematical objects you care about.
In fact, if you want to do set theory, you can do that inside type theory as well. You can define the type of iterative sets and define a membership relation on this. The resulting stucture will satisfy set theoretical axioms. This was first done by Aczel in the 70s.
>> i found the foundations via set-theory unintuitive and a bit ackward to work with.
> Type theories, especially dependent type theories a la Martin-Löf, are quite natural to work with (and) are easier to implement on a computer...
Whether or not type theories are "natural" is probably a matter of taste.
But it's hard to argue that they are necessarily "easier to implement on a computer". Metamath is a general-purpose verifier, and its primary database (the Metamath Proof Explorer at http://us.metamath.org/mpeuni/mmset.html ) is based on classical logic and ZFC set theory. A Metamath verifier in Mathematica is only 74 lines, while another in Python is only 350 lines. The Metamath verifier written in Rust is longer (it's written for speed), but it manages to verify about 32,000 proofs in about 0.9 seconds. It's so easy to write one that there's a long list of verifiers (see http://us.metamath.org/other.html#verifiers ). Metamath can handle HOL, too. I don't know of any shorter verifier that can handle the full range of mathematics. So by both code size and speed it's hard to argue that type theory is necessarily "easier" than traditional set theory on a computer. They both simply process symbols given a small set of rules.
There are many possible foundations of mathematics beyond ZFC and type theory, e.g., Quine's "New Foundations" (NF) (see http://us.metamath.org/nfeuni/mmnf.html for a Metamath encoding of that), HOL, etc. And that's not even counting logic systems: Classical logic is the most common in mathematics (by far), but intuitionistic logic is in use (and tools like Coq are built on it), and there are many other logic systems as well (paraconsistent, minimal, etc.).
That said, I believe ZFC (combined with classical logic) is by far the most commonly foundation referenced in mathematics today. Wikipedia claims: "Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics." https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
That doesn't mean that other systems are "not as good" or "not mathematical" - but when people ask about mathematical foundations, ZFC is typically what people refer to first. It's probably good to at least know a little about ZFC when discussing foundations, even if you decide to do something different.
EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very strict compiler.
Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program.
Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).
> Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
That's true. There's a Metamath database that encodes Higher-Order Logic (HOL) aka simple type theory: http://us.metamath.org/holuni/mmhol.html It's very bare-bones, but it shows it's possible.
> Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones...
I suspect we have to ask "popular for whom?" I'd agree that type theory is at least as popular as set theory among computer tools that formalize math. But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Type theory probably seems "natural" to people who are used to programming languages and compilers, and thus already have a daily familiarity with types (in the computer science sense).
"It's complicated" seems like an accurate summary of affairs :-).
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
Most mathematicians spend very little time thinking about the foundations of mathematics though, so I'd take that with a grain of salt. ;)
Seriously though, I think the statement that "all of modern mathematics can be formalized in ZFC" is probably wrong. There have been attempts to do just that (e.g., Bourbaki), but they invariably failed and ended up with extensions of ZFC (e.g., for category theory) or just silently started using higher-order logic.
Type theory seems to be a lot more practical. Both because it is explicitly designed to be an open system (a closed system must fail eventually due to Gödel arguments) and because similar formalization efforts go a lot more smoothly. For example, compare the treatment of category theory in the HoTT book with any introductory text using set theory.
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
That's true, but it's just as true that those same mathematicians only care about foundations as a proof of concept, not a practical device that you might someday want to do actual math in. ZFC is plenty good enough for the former, but you need type theories - or at least structural-set theories - to enable the latter (with the sorts of sanity checks that we've come to expect in any practical formal endeavor)!
"Set theory" itself is a bit of an overloaded term; most practical uses of naïve set theory in math do not make use of properties like extensionality or the global membership relation, that characterize axiomatic set theory over TT. Thus, one could also describe the sort of "more natural" systems you reference in your comment as 'structural set theory' https://ncatlab.org/nlab/show/structural+set+theory
It's true however that one can do material-set theory inside structural-set theory or type theory, by defining a type of material sets (not necessarily "iterative" however, that's a matter of whether you want to model the axiom of foundation!) and a membership relation on them.
Structural set theory, which as you say throws out the iterative structure, is more like type theory than set theory (this is pointed out in the nlab page you linked).
Naïve set theory as practised in say a course in discrete mathematics certainly uses the iterative structure to construct say a pair. You will typically find the definition 〈x,y〉 ≔ {{a},{a,b}} instead of defining it through a universal property.
All the axioms of material set theory take this iterative approach, not just foundation. In fact foundation is not very critical (The Axiom of Anti-foundation is just as workable), as you can always just use the class of well-founded sets and work with those.
I agree that "set theory" itself is a bit of an overloaded term, as there are in fact many set theories.
However, as you're probably well aware, naïve set theory can quickly lead to disaster because it leads to well-known paradoxes (like Russell's paradox). So if you're going to have foundations for mathematics (and it needs foundations!), it needs to avoid the paradoxes. ZFC does so, and in a way that many people have found satisfying enough.
Type theories like the one of coq support inductive definitions.
Inductive nat: Set
:= | O: nat
| S: nat -> nat
However, this feels a bit like having a whole programming language for the foundations of mathematics. An alternative would be to basically do the same as is usual in set theory. That is, have an axiom that states that an infinte set exists. This is enough to construct the natural numbers. This axiom can state that there is a Set S and a function f: S -> S that is injective but not surjective.
Seeing these comments let me remark that the problem that I have with inductive definitions is that one could have the expectation that the foundations of mathematics would be a rather small and simple set of rules from which the rest can be derived. When one introduces inductive definitions as is done in coq this principle is out of the window. The branches of an inductive must satisfy a 'positivity condition' that is quite complicated. Then there is the thing that one can also do mutually recursive inductive definions. Then there are more rules for what kind of match statements are allowed. And let us not even get started on CoInductive definitions. IIRC Freek Wiedijk described the foundations as they are in coq as 'beyond baroque' and that is quite to the point.
Actually, that `Inductive nat` is precisely a natural number object in terms of categorial semantics - it's worth mentioning that NNO's in categorial semantics are unique up to isomorphism. That "Inductive" syntax in Coq is actually a key part of the system, it's involved in defining things as basic as equality and product- or sum-types. This is quite different from how things would be done in a "standard" set theory.
> An alternative would be to basically do the same as is usual in set theory. That is, have an axiom that states that an infinte set exists. (...)
I was not aware of this construction, thanks! The only thing I knew is the construction of natural numbers from the empty set, by iteratively building singletons.
4. There exists a set X such that ∅ is in X and T ∪ {T} is in X whenever T is in X
These all follow from the axioms of ZFC and (4) is actually itself one of the axioms — the Axiom of Infinity. It says that an infinite set like X exists.
But you can see that the essence of it is just: "There exists a set X which includes the natural numbers." Note that this set X might contain many things beyond the set-theoretic copy of the natural numbers — the axiom just guarantees that a set containing the natural numbers exists ("some infinite set").
You can then use some of the other axioms to remove the unwanted elements, creating the unique, smallest set that satisfies this property.
In other words, the axioms of ZFC were designed to be Peano-friendly. It wasn't as if we arrived at ZFC and then said, "Oh, look at that, we can represent the natural numbers as sets. What a surprise!":D
Set theory as a toolkit is mostly geared towards questions of consistency/existence, size or "order" of objects, and raw mathematical explanatory power of theories or claims. It traditionally arose to explore ideas of infinity precisely, then grew to meet the needs of a mathematical community grappling with antinomies (e.g. Russell's paradox) and heated foundational divides (classicism vs intuitionism, etc). It still meets those needs well -- topics like large cardinals which chart the territory dangerously beyond the boundaries of (assumed) mathematical consistency are plied with set theory, and questions of consistency that arise in other fields tend to end up ported into set-theoretic terms.
I'm not a type theorist, but I imagine the split between set theory and type theory is analogous to the way in which different models of computation appeal to researchers on different sides of the "Theory A/Theory B" split in computer science. Researchers in the "A" group who study the outer limits of what problems are/aren't tractable, how different kinds of computational resource compare in power, etc, tend to use Turing machines and RAM models and circuits, which allow computational resources to be easily measured, bounded, simulated, reduced into things, etc. Researchers in the "B" group who explore programming languages, type systems, program analysis, etc, tend to prefer models like lambda calculus which allow programs to be easily composed and annotated with types and whatnot. I don't think this is just about cultural differences -- if you try to prove time-space trade-offs with the lambda calculus or invent a new type parameterization system with Turing machines then you're going to have a bad time.
Ironically, large-cardinals and related devices give set theory a rather type-theoretic "flavor". One can definitely explore the very same questions of 'consistency/existence, size or "order" of objects, and raw mathematical explanatory power of theories' with type-theoretic tools, and arguably do it quite more elegantly, because the related formal devices (e.g. "universes") arise more naturally in a type-theoretic context.
"The set theory formalism presented here differs from the traditional ZF system"
Do not, I repeat, DO NOT study nonstandard theories before familiarizing yourself with the standard theory. The standard set theory (ZFC) survived for over a century for very, very good reasons. Without an exposure to the accepted standards, you will not be able to tell what is reasonable and what is not in this set of notes.
It should also be noted that the author's field of concentration (geometric analysis) has nothing to do with set theory. A typical mathematician knows very little about axiomatic set theory and is prone to making imprecise statements about it.
While I agree that one could take caution when studying proposed alternative foundations of mathematics (there are a lot of dysfunctional theories out there, and the link may be one of them for all I know), I think it is unfair to presume incompetence based on the fact that the author has another field as his specialisation. ZFC is also not the one true way, there are many sensible ways to formulate set theory, and even valid criticisms of ZFC.
To me this looks like an interesting attempt to holistically give some overview of mathematics to lay people and could be improved if eg. those with correction proposals here would have some way to contribute back.
I might immensely enjoy such a wikipedia of mathematics.
Honestly, I would suggest looking at Wikipedia proper. It's coverage of mathematical topics seems to be currently quite good. You can generally easily google the proofs and the details for topics presented without these. The web altogether is goldmine of mathematical knowledge today imo.
Most things aren't explained "down to the elementary level" but anyone who spends significant time on this stuff will reach a higher level and appreciate not having the same elementary explanations repeated over and over.
Set theory and logic are too interdependent to venture far in one whilst steering clear of the other. For instance, you'll only really skim the surface of model theory without a basic understanding of infinite cardinals.
They can indeed be used together and are interdépendant in practice at "high level mathematics"
But set theory is made of a lower level primitive (first order logic) itself being an extension of zeroth order logic.
I was saying that in the context of learning the foundation of mathematics where set theory is not the first place to begin.
I'd say most intuition matches the reals, even if people's explanation of it would not match the definition.
You just need to walk someone through 'sqrt(2) is irrational ' and 'pi is transcendental' and you essentially end up with 'I want all converging sequences in Q to have a limit'. Which gives you the reals.
In some sense, the reals are the most naive number system. Just start with the natural numbers, and allow every sensible opperation.
> In some sense, the reals are the most naive number system. Just start with the natural numbers, and allow every sensible opperation.
It is simple only in retrospect. It took a few millennia for mankind to reach the definition of the reals. Meanwhile, Archimedes, Euclid, Pythagoras, al-Kwarizmi, Newton, Fermat, Gauss, Euler, Jacobi, Newton, Galois, Bernoulli, Laplace, Lagrange, Fourier did quite a lot of things (which are very relevant for all fields of math today) without even knowing the definition of limit!
It's a stretch to say that people after Newton did not know what a limit was. It's just that they did not have the formal definition of one.
Newton invented limits. Only he did not have a fundamental basis for it. Hence, he saw it is a dirty trick that happened to yield correct and useful results.
The formalization of limits came later when the intuitive use of a limit started failing. If I recall, this was with the Weierstrass function.
I think we agree though. You can do most maths just by assuming you can do things with the rational numbers. It takes some really weird stuff before you need to properly define the 'real-numbers'.
Yes indeed, one does not need to first learn zeroth order logic for doing maths.
I was talking for one that want to learn from the root of mathematics, some people believe that set theory is the foundation while it is a composition of lower level primitives
Interpreting A⇔B⇔C as (A⇔B)⇔C is utterly non-standard, but admittedly interesting.
A⇔B⇔C is usually not a valid expression in any mathematical formalism. But if used informally, A⇔B⇔C is usually meant to mean (A⇔B)∧(B⇔C), just as when you say A=B=C when you actually mean (A=B)∧(B=C).
The discussion is the meaninglessness of the parentheses. ⇔ is indeed commutative and associative which means that we can define removing the parentheses as equivalent. However it is equally valid to not do this and define an n-ary '⇔' operator that evaluates ⇔(a1..an) as all ai have the same value. The result is different semantics for A⇔B⇔C.
I've taught and always assume ((A⇔B)⇔C). I've apparently used (A⇔B)&(B⇔C) once.
Why not? The sky if green if and only if pigs can fly if and only if water is wet.
The sky if green if and only if pigs can fly is true.
True if and only if water is wet is true.
Ok, you've got a point, I've just never seen it used that way (though too be fair, I haven't often seen it used, probably for the reasons we're discussing).
I wish someone could give this a beauty treatment to make it look like Immersive Math, for instance (http://immersivemath.com/ila/index.html). This typography and formatting makes it very hard to read these notes, although the content seems to be very interesting.
There are links to pdf files near the headers of the chapters, although the pdfs are called "obsolete", so I guess they are not the latest version or miss content.
Seems like it's hit by the HN hug of death. Am wondering is there any way for me to help out random people who I think have good content by mirroring their content and increase scale on their behalf?
True, given any reasonable well-behaved notion of "set", there is a category Set of all sets. (Its properties will depend on the specific notion of "set" chosen.)
But this observation isn't really relevant to issues of formalization. Mathematics can be formalized in lots of systems, set theory being one, type theory being another, and category theory (more specifically ETCS) providing yet another alternative.
All of these foundations are interesting, enjoy unique features, and are interrelated. In particular, ETCS and set theory are very similar from the point of view of foundations: Basically, ordinary set theory and ETCS are two different flavors of set theory: ordinary set theory rests upon a global membership predicate ∈, while ETCS rests upon the notion of a morphism.
Closest to mathematical practice is probably type theory. (But keep in mind that the points above still stand, and that most mathematicians work informally, not knowing any details about set theory, type theory or ETCS.)
What is the first diagram on this page supposed to depict? Seems like a bunch of unrelated topics with random arrows drawn between them.
Also, the author seems more than a bit arrogant and deluded: http://settheory.net/life -- I would _not_ touch any of this stuff with a 40 foot pole.
I don't see anything there that's incompatible with a high level of skill at mathematics. Honestly, I don't know of any opinion outside the realm of mathematics that could be deluded or disorganized enough to make me think that the person holding it couldn't be competent at math. That said, before I trusted this web site as a source I'd look for evidence that it has been reviewed and improved by other people, because even a competent person is bound to make mistakes, and if he's working entirely alone his mistakes are likely to go uncorrected.
the whole thing you linked reads like he is going through some existential crisis triggered by spending too much time in his own head, or he is struggling to find himself. he calls others stupid but that might just be due to feeling misunderstood and a symptom of his alienation.
one thing I learned is that knowing more doesn't make us happy. knowledge can be the key that opens a door to insanity.
whether he is a lunatic or genius is hard to say without evaluating the quality of his work.
> But there are still many well-placed people who will never listen, cannot grasp this and that keep denying the right for young geniuses to decide for their own life.
This obsession with I am a genius is bordering on pathological narcissism, excluding oneself from the society because one's too smart to be understood by the world is a very dangerous slippery slope. On the other hand, while in a healthy way, I applaud when one sticks to their own ways. I just wish humility was mode widely practiced. We are not gods, we're just some creatures that have varying degrees of intelligence, but nothing special.
Good luck to you young thinker but remember we are to enjoy this life and the people around us. Don't be lonely and miserable trying to prove everybody wrong, it's pointless.
yeah it goes on and on. the Dunning-Kruger seems strong. I got the impression he is extremely isolated. sad really.
The major red flag is in the "misunderstood genius" part -- 99% of the people I've ever seen with a claim like that haven't interacted with things enough to have been able to truly test their claims. "Genius" is only "misunderstood" when the person laying claim to it does not do enough to substantiate their argument.
Here, I read some of what they had to say about "infoliberalism" -- the immediate issue that I have with their position is that they make some kind of claim that a few participants in it would naturally lead to a revolution. They then go on to claim that the system is completely decentralized, but also complain that not one other person is willing to join. If their system were truly decentralized, and also something that would provide significant benefits to participants over the existing social/economic/political order, why is the number of practitioners exactly one? All of this screams quackery.
That link looks like the writing of someone mentally ill.
I think "mentally ill" is pretty unfair. Passionate, depressed, maybe even self-righteous? Sure, all of these.
But his capacity for logic doesn't seem to be affected. English isn't his first language, but he still writes in full, grammatically correct sentences that are very clear. Wordy and emotional - yes. But not mentally ill.
I think we should be careful not to dismiss/overlook people because we don't share their emotional perspective on the world. In other words, just because he's a unique character doesn't mean his take on set theory should be ignored.
From a very brief click through (and from my own fairly superficial memory of the topic), it doesn't seem to be extremely unconventional. At the very least, it's not standing shoulder to shoulder with Timecube.
A lot of geniuses have issues. I wouldn't use this to judge the rest of his work.
The author is evidently far from neurotypical. Generally I find these kinds of diverse viewpoints interesting, if not appealing.
Unfortunately his prose borders on unreadable. There may very well be excellent ideas here, but until he follows the commandment "omit needless words" nobody is going to wade through it.
He's definitely angry, but from skimming it, it sounds like he had some ideas, put them out there, and no one bit.
And he's uspet that it didn't pan out, and he's quite clear on a fairly reasonable, if hyperbolic, explanation of why the ideas didn't work.
I read it as him coming to grips with the common blind spot of "my ideology would work just fine except for all the people who don't hold my ideology". You hear it from proponents of all major ideologies; liberalism "they're on the wrong side of history", conservatism "what happened to common sense?!" and libertarianism "but in a libertarian society..."
His stuff is ranty and tone-deaf, and he probably shouldn't include it on a page on set theory, but he's not delusional.
For all of the political ideologies you listed, we have concrete examples of societies which trend in those directions. Sure, most real societies do not trend toward radical versions of those ideologies, but at least we can each get an okay sense of the first derivative, so to speak, of "goodness" with respect to variation in political leanings.
Correct me if I'm wrong, but it doesn't seem like anything like "Infoliberalism" has ever been tested (and the author even _says_ as much). Before jumping on the boat of a radical political ideology, I'm sure that any reasonable person would at least like to have an _idea_ of what it leads to.
Yeah, I broadly agree. But I think a person can only be radical if they disregard normal social inhibitory / moderating influences. I'm reluctant to write him off as delusional because I'd have to write off most activists. And he's pretty clear that he's aware that he's behaving out of the bounds of polite society, and he's taking his ideas to their logical conclusion.
And I think for any new idea that is non-trivial, whether it's a new ideology, business plan, or whatever, a reasonable person also has to admit the only practical way to figure out if a thing works is to do it.
Yes, I absolutely agree with your second statement. However, the issue I take with the author is that they say that they are not a programmer, and they're frustrated that they cannot get a programmer to help build a prototype. Being _frustrated_ that people won't work for you _for free_ is delusional. The author could have also decided that their idea was worth enough to them to _learn_ how to program, so they could build a workable prototype, and possibly attract other developers as part of an open source project. However, the author seems more content to just sit there and complain about being "misunderstood." Implementations typically are worth a lot more than ideas, and this is exactly what the author doesn't seem to get.
Eh. Donald Knuth is Lutherian. I'm atheist and I believe it is unscientific and deluded to believe in things from an ancient book of fairy tales.
This doesn't discount Knuths' major contributions to the field. No one is perfect. Even the most logical, intelligent person could have aspects of himself that are illogical.
If the OP's set theory stuff is good, I wouldn't let his emotional rants affect my judgement of this.
I had a seminar on set theory and the foundations of mathmatics. It was very fun! But, coming from a computer science background, i found the foundations via set-theory unintuitive and a bit ackward to work with.
I know there are some type-system based approaches, how do they turn out in practice? How nice are they to work with "on a low level"?
Type theories, especially dependent type theories a la Martin-Löf, are quite natural to work with. They are easier to implement on a computer, and there are active communities around several such implementations (Agda, Coq, Lean,⋯).
Most computer verified proofs are implemented in systems based on type theory, not set theory. Most of the time you do not need sets of sets of sets… You want types whose elements are the mathematical objects you care about.
In fact, if you want to do set theory, you can do that inside type theory as well. You can define the type of iterative sets and define a membership relation on this. The resulting stucture will satisfy set theoretical axioms. This was first done by Aczel in the 70s.
>> i found the foundations via set-theory unintuitive and a bit ackward to work with.
> Type theories, especially dependent type theories a la Martin-Löf, are quite natural to work with (and) are easier to implement on a computer...
Whether or not type theories are "natural" is probably a matter of taste.
But it's hard to argue that they are necessarily "easier to implement on a computer". Metamath is a general-purpose verifier, and its primary database (the Metamath Proof Explorer at http://us.metamath.org/mpeuni/mmset.html ) is based on classical logic and ZFC set theory. A Metamath verifier in Mathematica is only 74 lines, while another in Python is only 350 lines. The Metamath verifier written in Rust is longer (it's written for speed), but it manages to verify about 32,000 proofs in about 0.9 seconds. It's so easy to write one that there's a long list of verifiers (see http://us.metamath.org/other.html#verifiers ). Metamath can handle HOL, too. I don't know of any shorter verifier that can handle the full range of mathematics. So by both code size and speed it's hard to argue that type theory is necessarily "easier" than traditional set theory on a computer. They both simply process symbols given a small set of rules.
There are many possible foundations of mathematics beyond ZFC and type theory, e.g., Quine's "New Foundations" (NF) (see http://us.metamath.org/nfeuni/mmnf.html for a Metamath encoding of that), HOL, etc. And that's not even counting logic systems: Classical logic is the most common in mathematics (by far), but intuitionistic logic is in use (and tools like Coq are built on it), and there are many other logic systems as well (paraconsistent, minimal, etc.).
That said, I believe ZFC (combined with classical logic) is by far the most commonly foundation referenced in mathematics today. Wikipedia claims: "Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics." https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
That doesn't mean that other systems are "not as good" or "not mathematical" - but when people ask about mathematical foundations, ZFC is typically what people refer to first. It's probably good to at least know a little about ZFC when discussing foundations, even if you decide to do something different.
EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very strict compiler.
Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program.
Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).
> Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
That's true. There's a Metamath database that encodes Higher-Order Logic (HOL) aka simple type theory: http://us.metamath.org/holuni/mmhol.html It's very bare-bones, but it shows it's possible.
> Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones...
I suspect we have to ask "popular for whom?" I'd agree that type theory is at least as popular as set theory among computer tools that formalize math. But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Type theory probably seems "natural" to people who are used to programming languages and compilers, and thus already have a daily familiarity with types (in the computer science sense).
"It's complicated" seems like an accurate summary of affairs :-).
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
Most mathematicians spend very little time thinking about the foundations of mathematics though, so I'd take that with a grain of salt. ;)
Seriously though, I think the statement that "all of modern mathematics can be formalized in ZFC" is probably wrong. There have been attempts to do just that (e.g., Bourbaki), but they invariably failed and ended up with extensions of ZFC (e.g., for category theory) or just silently started using higher-order logic.
Type theory seems to be a lot more practical. Both because it is explicitly designed to be an open system (a closed system must fail eventually due to Gödel arguments) and because similar formalization efforts go a lot more smoothly. For example, compare the treatment of category theory in the HoTT book with any introductory text using set theory.
Set Theory is not a "closed system." The Axiom of Choice is one example.
The axiom of choice is part of ZFC. The existence of, e.g., a Mahlo cardinal is not.
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
That's true, but it's just as true that those same mathematicians only care about foundations as a proof of concept, not a practical device that you might someday want to do actual math in. ZFC is plenty good enough for the former, but you need type theories - or at least structural-set theories - to enable the latter (with the sorts of sanity checks that we've come to expect in any practical formal endeavor)!
"Set theory" itself is a bit of an overloaded term; most practical uses of naïve set theory in math do not make use of properties like extensionality or the global membership relation, that characterize axiomatic set theory over TT. Thus, one could also describe the sort of "more natural" systems you reference in your comment as 'structural set theory' https://ncatlab.org/nlab/show/structural+set+theory
It's true however that one can do material-set theory inside structural-set theory or type theory, by defining a type of material sets (not necessarily "iterative" however, that's a matter of whether you want to model the axiom of foundation!) and a membership relation on them.
Structural set theory, which as you say throws out the iterative structure, is more like type theory than set theory (this is pointed out in the nlab page you linked).
Naïve set theory as practised in say a course in discrete mathematics certainly uses the iterative structure to construct say a pair. You will typically find the definition 〈x,y〉 ≔ {{a},{a,b}} instead of defining it through a universal property.
All the axioms of material set theory take this iterative approach, not just foundation. In fact foundation is not very critical (The Axiom of Anti-foundation is just as workable), as you can always just use the class of well-founded sets and work with those.
I agree that "set theory" itself is a bit of an overloaded term, as there are in fact many set theories.
However, as you're probably well aware, naïve set theory can quickly lead to disaster because it leads to well-known paradoxes (like Russell's paradox). So if you're going to have foundations for mathematics (and it needs foundations!), it needs to avoid the paradoxes. ZFC does so, and in a way that many people have found satisfying enough.
> Most of the time you do not need sets of sets of sets…
How do you construct the natural numbers, then ?
Type theories like the one of coq support inductive definitions.
However, this feels a bit like having a whole programming language for the foundations of mathematics. An alternative would be to basically do the same as is usual in set theory. That is, have an axiom that states that an infinte set exists. This is enough to construct the natural numbers. This axiom can state that there is a Set S and a function f: S -> S that is injective but not surjective.Seeing these comments let me remark that the problem that I have with inductive definitions is that one could have the expectation that the foundations of mathematics would be a rather small and simple set of rules from which the rest can be derived. When one introduces inductive definitions as is done in coq this principle is out of the window. The branches of an inductive must satisfy a 'positivity condition' that is quite complicated. Then there is the thing that one can also do mutually recursive inductive definions. Then there are more rules for what kind of match statements are allowed. And let us not even get started on CoInductive definitions. IIRC Freek Wiedijk described the foundations as they are in coq as 'beyond baroque' and that is quite to the point.
ZFC includes an infinite axiom schema, so it's not really elegant and simple in that way either.
> That is, have an axiom that states that an infinte set exists.
Type theories do have that axiom. It takes the form of the axiom that postulates the existence of inductive types of the kind you've shown.
Actually, that `Inductive nat` is precisely a natural number object in terms of categorial semantics - it's worth mentioning that NNO's in categorial semantics are unique up to isomorphism. That "Inductive" syntax in Coq is actually a key part of the system, it's involved in defining things as basic as equality and product- or sum-types. This is quite different from how things would be done in a "standard" set theory.
But is equality a basic thing to define? :)
> An alternative would be to basically do the same as is usual in set theory. That is, have an axiom that states that an infinte set exists. (...)
I was not aware of this construction, thanks! The only thing I knew is the construction of natural numbers from the empty set, by iteratively building singletons.
The axiom of infinity ("there exists an infinite set") is what gives you permission to carry out the construction you describe.
The usual construction of the naturals via set theory has us define...
1. 0 as the empty set ∅
2. succ(n) as n ∪ {n}
So you get...
But how do we know the following?1. The empty set ∅ is a set
2. If T is a set then {T} is also a set
3. If T is a set then T ∪ {T} is a set
4. There exists a set X such that ∅ is in X and T ∪ {T} is in X whenever T is in X
These all follow from the axioms of ZFC and (4) is actually itself one of the axioms — the Axiom of Infinity. It says that an infinite set like X exists.
But you can see that the essence of it is just: "There exists a set X which includes the natural numbers." Note that this set X might contain many things beyond the set-theoretic copy of the natural numbers — the axiom just guarantees that a set containing the natural numbers exists ("some infinite set").
You can then use some of the other axioms to remove the unwanted elements, creating the unique, smallest set that satisfies this property.
In other words, the axioms of ZFC were designed to be Peano-friendly. It wasn't as if we arrived at ZFC and then said, "Oh, look at that, we can represent the natural numbers as sets. What a surprise!":D
Set theory as a toolkit is mostly geared towards questions of consistency/existence, size or "order" of objects, and raw mathematical explanatory power of theories or claims. It traditionally arose to explore ideas of infinity precisely, then grew to meet the needs of a mathematical community grappling with antinomies (e.g. Russell's paradox) and heated foundational divides (classicism vs intuitionism, etc). It still meets those needs well -- topics like large cardinals which chart the territory dangerously beyond the boundaries of (assumed) mathematical consistency are plied with set theory, and questions of consistency that arise in other fields tend to end up ported into set-theoretic terms.
I'm not a type theorist, but I imagine the split between set theory and type theory is analogous to the way in which different models of computation appeal to researchers on different sides of the "Theory A/Theory B" split in computer science. Researchers in the "A" group who study the outer limits of what problems are/aren't tractable, how different kinds of computational resource compare in power, etc, tend to use Turing machines and RAM models and circuits, which allow computational resources to be easily measured, bounded, simulated, reduced into things, etc. Researchers in the "B" group who explore programming languages, type systems, program analysis, etc, tend to prefer models like lambda calculus which allow programs to be easily composed and annotated with types and whatnot. I don't think this is just about cultural differences -- if you try to prove time-space trade-offs with the lambda calculus or invent a new type parameterization system with Turing machines then you're going to have a bad time.
Ironically, large-cardinals and related devices give set theory a rather type-theoretic "flavor". One can definitely explore the very same questions of 'consistency/existence, size or "order" of objects, and raw mathematical explanatory power of theories' with type-theoretic tools, and arguably do it quite more elegantly, because the related formal devices (e.g. "universes") arise more naturally in a type-theoretic context.
"The set theory formalism presented here differs from the traditional ZF system"
Do not, I repeat, DO NOT study nonstandard theories before familiarizing yourself with the standard theory. The standard set theory (ZFC) survived for over a century for very, very good reasons. Without an exposure to the accepted standards, you will not be able to tell what is reasonable and what is not in this set of notes.
It should also be noted that the author's field of concentration (geometric analysis) has nothing to do with set theory. A typical mathematician knows very little about axiomatic set theory and is prone to making imprecise statements about it.
While I agree that one could take caution when studying proposed alternative foundations of mathematics (there are a lot of dysfunctional theories out there, and the link may be one of them for all I know), I think it is unfair to presume incompetence based on the fact that the author has another field as his specialisation. ZFC is also not the one true way, there are many sensible ways to formulate set theory, and even valid criticisms of ZFC.
Set theory historically exists to serve analysis.
https://www.youtube.com/watch?v=hBcWRZMP6xs
Related: Category Theory for Programmers
https://github.com/hmemcpy/milewski-ctfp-pdf
To me this looks like an interesting attempt to holistically give some overview of mathematics to lay people and could be improved if eg. those with correction proposals here would have some way to contribute back.
I might immensely enjoy such a wikipedia of mathematics.
Honestly, I would suggest looking at Wikipedia proper. It's coverage of mathematical topics seems to be currently quite good. You can generally easily google the proofs and the details for topics presented without these. The web altogether is goldmine of mathematical knowledge today imo.
Most things aren't explained "down to the elementary level" but anyone who spends significant time on this stuff will reach a higher level and appreciate not having the same elementary explanations repeated over and over.
One should read about standard logic, propositional logic, term logic and nth order logics before, because set theory is founded by them.
Set theory and logic are too interdependent to venture far in one whilst steering clear of the other. For instance, you'll only really skim the surface of model theory without a basic understanding of infinite cardinals.
They can indeed be used together and are interdépendant in practice at "high level mathematics" But set theory is made of a lower level primitive (first order logic) itself being an extension of zeroth order logic. I was saying that in the context of learning the foundation of mathematics where set theory is not the first place to begin.
Not really. There are many reasonable places to start learning in the edifice of mathematics, without needing to be aware of the whole structure.
For example, you can do a lot of math without knowing the definition of real number.
I'd say most intuition matches the reals, even if people's explanation of it would not match the definition.
You just need to walk someone through 'sqrt(2) is irrational ' and 'pi is transcendental' and you essentially end up with 'I want all converging sequences in Q to have a limit'. Which gives you the reals.
In some sense, the reals are the most naive number system. Just start with the natural numbers, and allow every sensible opperation.
> In some sense, the reals are the most naive number system. Just start with the natural numbers, and allow every sensible opperation.
It is simple only in retrospect. It took a few millennia for mankind to reach the definition of the reals. Meanwhile, Archimedes, Euclid, Pythagoras, al-Kwarizmi, Newton, Fermat, Gauss, Euler, Jacobi, Newton, Galois, Bernoulli, Laplace, Lagrange, Fourier did quite a lot of things (which are very relevant for all fields of math today) without even knowing the definition of limit!
It's a stretch to say that people after Newton did not know what a limit was. It's just that they did not have the formal definition of one.
Newton invented limits. Only he did not have a fundamental basis for it. Hence, he saw it is a dirty trick that happened to yield correct and useful results. The formalization of limits came later when the intuitive use of a limit started failing. If I recall, this was with the Weierstrass function.
I think we agree though. You can do most maths just by assuming you can do things with the rational numbers. It takes some really weird stuff before you need to properly define the 'real-numbers'.
Yes indeed, one does not need to first learn zeroth order logic for doing maths. I was talking for one that want to learn from the root of mathematics, some people believe that set theory is the foundation while it is a composition of lower level primitives
This contains some falsehoods, e.g.
is not the same as and the former doesn't imply either, but the latter does.Interpreting A⇔B⇔C as (A⇔B)⇔C is utterly non-standard, but admittedly interesting.
A⇔B⇔C is usually not a valid expression in any mathematical formalism. But if used informally, A⇔B⇔C is usually meant to mean (A⇔B)∧(B⇔C), just as when you say A=B=C when you actually mean (A=B)∧(B=C).
https://en.wikipedia.org/wiki/Logical_biconditional
(A⇔B)⇔C has more in common with the other logical operators: due to it's associativity an interpretation that is, in my opinion, closer than A=B=C.
Edit, removed: Note that (A⇔B)∧(B⇔C)) is not one of the two ambiguous options: either (A⇔B)⇔C or (A∧B∧C)∨(¬A∧¬B∧¬C) this is wrong.
What? `(A⇔B)∧(B⇔C)` is exactly equivalent to `(A∧B∧C)∨(¬A∧¬B∧¬C)` which is equivalent to `A = B = C`
So it is.
What?
What do you mean by (A⇔B⇔C) then?
Because I’m pretty sure I’ve basically only seen it as shorthand for the conjunction of (A⇔B) and (B⇔C), when it is understood that ⇔ is transitive.
So what's the interpretation that will make one false and the other true?
My standard interpretation is ((A⇔B)⇔C). A=F,B=F,C=T differ in evaluation.
* edited T to F
Those parentheses are meaningless, since IFF (aka NOT-XOR) is associative and commutative.
IFF is a parity counter like XOR.
XOR counts how many bits are true. IFF is NOT of how many bits are false. (This shows why XOR is used much more than IFF, because it is cleaner.)
(a XOR false is a, and a XOR true is NOT a, aka a+1 mod 2; a IFF true is a, and a IFF false is a+1 mod 2)
The discussion is the meaninglessness of the parentheses. ⇔ is indeed commutative and associative which means that we can define removing the parentheses as equivalent. However it is equally valid to not do this and define an n-ary '⇔' operator that evaluates ⇔(a1..an) as all ai have the same value. The result is different semantics for A⇔B⇔C.
I've taught and always assume ((A⇔B)⇔C). I've apparently used (A⇔B)&(B⇔C) once.
Doesn't that evaluate as true if A and B are contradictions and C is a tautology?
Whatever A⇔B⇔C means, surely it shouldn't allow for that.
Why not? The sky if green if and only if pigs can fly if and only if water is wet. The sky if green if and only if pigs can fly is true. True if and only if water is wet is true.
Ok, you've got a point, I've just never seen it used that way (though too be fair, I haven't often seen it used, probably for the reasons we're discussing).
How do you read
The error comme from the use of the equivalence operator instead of the material Implication operator =>
I wish someone could give this a beauty treatment to make it look like Immersive Math, for instance (http://immersivemath.com/ila/index.html). This typography and formatting makes it very hard to read these notes, although the content seems to be very interesting.
There are links to pdf files near the headers of the chapters, although the pdfs are called "obsolete", so I guess they are not the latest version or miss content.
I love this. I wish I started math with these tools back in the day!!
Seems like it's hit by the HN hug of death. Am wondering is there any way for me to help out random people who I think have good content by mirroring their content and increase scale on their behalf?
Category theory is an alternative view on the foundations of mathematics that literally gets rid of sets.
Well, there is the rather prototypical category Set. So I would not say it gets rid of sets.
It's more subtle than that.
True, given any reasonable well-behaved notion of "set", there is a category Set of all sets. (Its properties will depend on the specific notion of "set" chosen.)
But this observation isn't really relevant to issues of formalization. Mathematics can be formalized in lots of systems, set theory being one, type theory being another, and category theory (more specifically ETCS) providing yet another alternative.
All of these foundations are interesting, enjoy unique features, and are interrelated. In particular, ETCS and set theory are very similar from the point of view of foundations: Basically, ordinary set theory and ETCS are two different flavors of set theory: ordinary set theory rests upon a global membership predicate ∈, while ETCS rests upon the notion of a morphism.
Closest to mathematical practice is probably type theory. (But keep in mind that the points above still stand, and that most mathematicians work informally, not knowing any details about set theory, type theory or ETCS.)
Also, there are many examples of concrete sets in there. For example, "the set of morphisms from A to B" (in a locally small category).
Yeah, you are right. Maybe I should say gets rid of sets as a the foundation of mathematical theories?
Question: Would you use 'set theory' to find patterns of sets in a hierarchy?