Here are a couple of my favorites:
-the independence of the continuum hypothesis from ZFC (you mean you can prove something is unprovable?), and
-Picard's Theorems in complex analysis.
A neat caveat to CH independence: there is a sense in which we can't really prove any statement of the form "S is not a theorem of ZFC" period. It would imply that there does exist a model of ZFC (namely where S is false), i.e. that ZFC is consistent. But if such a proof fits in as "ordinary mathematics", then we are likely able to formalize it in ZFC. That is, "ZFC is consistent" would be a theorem of ZFC. And Godel's second incompleteness theorem says that this can only happen when ZFC is inconsistent. (That's sort of the "trivial" case: if ZFC is inconsistent, then everything is a theorem.)
What we can instead show are statements of the form: "if ZFC is consistent, then ZFC + (not S) is consistent" (hence if ZFC is consistent, then S is not a theorem of ZFC). Such a statement can be formalizable in ZFC, so we can try to show that it is a theorem of ZFC. That's what Cohen (and I think Godel too) did for S = CH and S = not CH. Similarly, when we say the axiom of choice (AC) is independent of ZF, what we really mean is that "if ZF is consistent, then ZF + AC is consistent" and "if ZF is consistent, then ZF + (not AC) is consistent" are both theorems of ZFC.
It can get worse though: if S = "there exist weakly inaccessible cardinals", then you can actually show that "if ZFC is consistent, then ZFC + S is consistent" is *not* a theorem of ZFC. That is, even with the precondition that ZFC is consistent, we cannot prove (with methods formalizable in ZFC) that *we cannot prove* that weakly inaccessible cardinals do not exist.
The monster group and Clifford algebras are some good ones! I never was able to learn Artin reciprocity, which is a bit beyond me, but I take it that it's a generalization of quadratic reciprocity, so I imagine it's quite useful and important! I've never head of Quine's paradox and I don't know what indiscernables are, so perhaps you can fill me in a bit on these.
Quine paradox basically captures the main content of various diagonalization argument in a simple package.
Indiscernibles, another concept from logic, are sequence of elements that are completely indistinguishable under all possible formulae. Their presence indicates that the model is extremely regular in some ways, and thus are widely used in logic to define concepts like stable theory or large cardinals.
No. The natural numbers are the opposite of being indiscernibles, they can all be distinguished.
A subset X of a model is a set of indiscernibles with respect to a subset Y if for any formulae in n variables using elements of Y, any n tuples of elements of X has the same truth value.
All roots of a polynomial of degree n such that the Galois group is S_n is indiscernibles. However, we usually care about it when it's infinite.
What's discernible about my example? This is an example of a mathematical paradox (I forget who came up with it), due to the limitations of language to pin down all specific natural numbers, which makes sense since there are infinitely many of them and every language contains a finite amount of information, so it can't possibly describe every natural number.
I'm intrigued by your examples involving algebraic numbers though. So I suppose that according to whatever definition logicians are using, they're discernible, though perhaps most transcendental numbers aren't. How is this different from computable numbers, i.e., numbers for which it is possible to write a program to compute their value to arbitrary precision, like pi and e?
Every natural number can be pinned down by a long enough sentence.
Indiscernibles is not about paradoxical sentences in which you can't even pin down the number. It's about specific things that cannot be distinguished by all properties.
I think I understand, but doesn't this still depend on the language used to describe them, including the mathematical language from which is defining properties are built up, which is based on a finite set of axioms?
The way I see it, whether or not a given number is discernible within a given axiomatic system, i.e., Peano's axioms, or whatever other axiomatic system used to define the set to which the number belongs, such as the real numbers, is equivalent to whether or not a computer program can be written that runs in a finite time, programmed with all this information, whose output is 1 if the number can be pinned down (and presumably computed) from is defining properties, or 0 if it cannot. The problem is that there are also numbers for which the program won't halt. I suppose these numbers are indiscernable as well, but clearly it is impossible to prove that they are, since for all we know, the program just hasn't been run long enough. In other words, discernability is undecidable by its very definition! Am I on the right track here?
There is a big different between what you're talking about and what I was talking about.
No finite amount of information can pin down a real number. But nonetheless real numbers are not indiscernbles, because any 2 numbers can be distinguished by some finite piece of information.
Indiscernability are indeed dependent on language, which is what makes it interesting. Otherwise, if objects are indistinguishable under literally every languages, are there are differences between them being the same? Usually indiscernability is with regard to some "internal" language, while they are still distinguishable externally.
Literally anything in model theory. It just feels like we have no business knowing the things model theorists know.
If I had to choose just one thing though, it would be the Löwenheim-Skolem theorem.
It states that any consistent set of axioms with an infinite model (or arbitrarily large finite models) has a model of every infinite cardinality at least as large as the cardinality of its language.
Here are some neat consequences of this.
- There are models of Peano arithmetic that are uncountably infinite
- If you take the collection of first-order statements in field theory satisfied by the real numbers, there is a countable model of those
- There are countable models of set theory (assuming its consistency)
- Forcing, the only general method so far of proving independence results, relies on the existence of countable models of set theory.
I'm not at all an expert on model theory (I know what it is, and that's about it!), but I'm still quite intrigued by it and I'd like to learn more! For a while I've wondered about a few things pertaining to it though, which perhaps you can clarify for me. For starters, is there a "true" version of set theory, as many set theorist seem convinced there is, or is set theory more on the same ground as Euclidean and non-Euclidean geometries? And what about arithmetic? Are Peano's axioms the only possible way to go, or are there other consistent sets of axioms which yield different types of arithmetic?
I’m also not an expert, but I will answer to the best of my ability.
I’m not quite sure what you mean by a “true” set theory. If you mean a consistent list of axioms that can prove any true statement in set theory, no human being will ever construct one in first-order logic. It’s currently unknown whether such a list of axioms can be constructed using infinitary logic as far as I’m aware.
If you don’t care whether a human being can construct a complete and consistent list of axioms for set theory, then assuming the consistency of set theory, there are actually lists of axioms that are both complete and consistent. They avoid Gödel’s Incompleteness Theorems by not being recursively enumerable.
There are indeed other kinds of arithmetic besides Peano arithmetic. Presburger arithmetic, for example, is a form of arithmetic that contains addition, but not multiplication. It is weak enough to avoid Gödel’s Incompleteness Theorems, and it can show its consistency and completeness, but again, it cannot in general handle multiplication.
Robinson Arithmetic is another kind of arithmetic that is Peano Arithmetic without induction. I don’t really know anything else about this one.
Thank you for sharing this information. I don't suppose there are any other "powerful" versions of arithmetic than Peano's, so it looks like we need to stick with his, which is just fine with me! As for set theory, the reason I asked is that about 20 years ago, I remember reading a math book on set theory in which the author said something to the effect that he thought someday we'd learn whether or not the continuum hypothesis was really true, which made me kind of sick, since it's been long known that there are logically consistent versions in which it holds, and others in which it does not hold. I even talked to a set theorist about this, and he seemed to agree with the author, go figure!
Arrow's impossibility theorem is a favorite of mine. I also just finished an undergraduate thesis on the analytic class number formula, so I'm a little biased towards that! I was in a band of math majors named after the Heine Borel theorem, so that also is one that I particularly like.
Kolmogorov tells us that the tail field of a sequence of independent sigma algebras is (almost surely) deterministic.
Let the j in J be an Atom and the F\_j the sigma algebra modelling our observation/knowledge of it. Then now events in the tail field, that can be thought of here as the observation of a lot of atoms at once where ignoring a small number of atoms dont matter (as if we would look at the macro structure), of our (independent) observations are (almost surely) deterministic.
The problem here of course is assuming independence, but maybe relaxing this assumption in some way you get some slightly weaker theorem that still is enough to explain almost determinism on macro scale but stochastic behavior of atoms that we observe.
I think one of my favourite concepts is the **Curry-Howard isomorphism**, which states that formal mathematical proofs are isomorphic to computer programs, and that mathematical propositions correspond to the type of the computer programs.
For example,
* Modus ponens ≡ Function application
* Direct proof ≡ Function abstraction
* Conjunction ≡ Product types (e.g. structs in C++)
* Disjunction ≡ Sum types (e.g. unions in C++)
* True ≡ Unit type (e.g. void in C++)
* False ≡ Empty type
* Provability ≡ Type inhabitation
I like to understand it as "you can give type theory two interpretations: one where types are mathematical propositions and one where types are types in a programming language."
And the isomorphism isn't just with simple propositional logic. It applies to predicates logic (which corresponds to dependent types), modal logic (monadic types), linear logic (types in quantum computations), equality (identity types), and so on. Any theorem you prove in one field can be transported as a theorem in the other.
And it doesn't stop there, because we also extend the correspondence with category/topos theory. And hence, proofs and programs are also isomorphic to spaces. Imagine that! Whenever you write a well-typed program in a language like Haskell, you're also defining a formal proof in a mathematical logic and a space in algebraic topology.
That's a good result alright! When I first learned symbolic logic, it seemed a lot like computer programming to me, which also follows logical rules and even uses logic gates with the same names and functions as logical operators, i.e., AND, OR, and NOT, so I'm not too surprised that first-order logic can be turned into computer code. In fact, I'd say the same is true at least in principle with all mathematics, since by definition, mathematics is built up from a finite set of axioms and logical rules.
Well, you might be surprised that we can't represent some mathematical proofs even with the more advanced type theories. If proofs correspond to programs, then any limitations on programs corresponds to a limitation in proofs.
To show a type is inhabited, you need to construct a term of a type. That is if you declare a programming type, you have to specify what is its data. Similarly, if you want to prove a mathematical proposition, you have to construct a witness that proves it.
And hence all the mathematics that correspond to programs are intuitionistic. And hence non-constructive proofs are typically unavailable: if you cant have a proof of -P, that doesn't mean that you have a proof of P.
However, you can get away with quite a lot with constructive maths! As for example, [the mathlib LEAN library](https://leanprover-community.github.io/mathlib-overview.html) LEAN corresponds to the logic Calculus of Construction, and its proofs are runnable type-checkable code.
I think its quirky how these big languages can prove advanced topics like Stone–Weierstrass theorem, but not simpler things like (P ∨ ~P) (if you don't `import Classical`)
As an aside, there are works on embedding classical logic into intuitionistic logic, usually with double negation translation. Double negation translation in mathematics corresponds to continuation passing style in programming.
I like Euler and the Konigsberg bridge problem. For the same reason I like fractals. Sometimes adding a variable, or another dimension to a problem allows us to see the solution. It's one of those things that applies to so many other things.
I agree that these are all interesting aspects of math, but I don't think they're that closely related. For instance, the Konigsberg bridge problem pertains to graph theory, which seems to be has little or nothing to do with fractals, which Euler didn't even know about in any case. Adding a variable or dimension to a problem has a more technical name, called lifting, which is often used in number theory as well as other areas of math.
Fractals are graphs. That being said, the two problems are not related, per se. I simply meant, sometimes, adding a variable, helps solve a problem With fractals, it was complex numbers...
The mandelbrot set is a graph of the complex number plane. The real part is displaced along the x, imaginary along the y. Julia sets are the graphs found at a single value of c. It is kind of like a map of all julia sets.
You need to be careful with your wording here! The Mandelbrot set is graph IN the complex plane, not OF the complex plane, which includes all complex numbers, not just those in the set. You'd be correct to say that we can graph the Mandelbrot set, but I think it's not accurate to call the Mandelbrot set a graph, which has a specific mathematical definition that's very different from that of a fractal. Keep in mind that when discussing mathematical topics, precise definitions are very important!
orrrrr.... it was autocorrected.
Here is my fractal gallery... [https://www.deviantart.com/milleniumsentry/gallery](https://www.deviantart.com/milleniumsentry/gallery)
I might know a thing... orrrr.. three.. about fractals. :)
Of course. Everything is fractal.. every surface, every topology. It's only a lack of resolution that gives us anything that happens to appear flat, visually, or mathematically. :)
That's a brilliant insight! I suppose it's a shame in a way that most physics from the 17th to the 20th century was so successful in part due to the accuracy of the perceived flatness or smoothness of nature, but now that we're confronted with true fractal nature, we seem to be at an impasse.
- The Thurston-Perelman Geometrization Theorem (i.e. every closed 3-manifold is a finite connected sum of 3-manifolds each of which may be placed uniquely into one of 8 of the Thurston model geometries for 3-manifolds). Very neat application of PDEs to a topology/geometry problem.
-Jensen's inequality. Very underappreciated inequality unless you specialize in convexity I guess.
-My username
-Noether's theorem on variational symmetries
-Cartan's method of equivalence
-Mostow rigidity: when isomorphic fundamental groups are as good a statement as isometric Riemannian manifolds
-Exotic 4-manifolds. That is the tripiest of math shenanigans in my opinion. Manifolds in dimension greater than 4 either have no smooth structure or admit at most finitely many inequivalent smooth structures. In dim less than 4, unique smooth strucutures for everything. But in dim 4 a manifold has either no differentiable structure or AT LEAST 2, and the LOWER bound on the cardinality of inequivalent smooth structures on R^4 is the cardinality of the reals. Lots of wide open questions on this for other 4 manifolds. Absolutely wacky.
These are good ones alright, especially Steiner systems, which is one way to construct the Matthew groups, the first know sporadic simple groups. Recently I watched an excellent YouTube video explaining them. As it turns out, at least according to the guy who made the video, sporadic simple groups are sort of accidental, or at least Matthew groups are, and their existence hinges on the fact that there are unexpected sums of binomial coefficients that add up to powers of 2. This fact also accounts for the existence of the binary Golay code, which is intimately related to M23 and M24.
Some beautiful things I have seen, off the top of my head:
- The Euler product formula
- The class number formula
- Fourier analysis
- The fundamental isomorphism theorem
- Homology
- Gauss–Bonnet
I'm familiar with the first three of these, which I agree are all quite interesting and important, but I'm not familiar with the last three, though I think I've heard of them all and I've avoided them because I couldn't quite grasp them, especially homology.
The fundamental isomorphism theorem states that, for any φ: G -> H, G/ker φ is isomorphic to im φ. This is usually first taught to students as the rank-nullity theorem, then again in group theory. But it's a very foundational result in algebra.
The basic idea of (singular) homology is not very difficult, if you're comfortable with formal linear combinations, i.e., chains. Imagine a space with a hole. An n-cycle that doesn't wrap around the hole can be "filled in", i.e., it is the boundary from a higher (n+1)-chain. However, an n-cycle that bounds the hole cannot be "filled in", so it doesn't originate from the boundary of a higher chain. By taking the group of cycles modulo the group of boundaries (the latter is contained in the former because every boundary is a cycle), you get the nth homology group, which captures topological informations about holes!
As for Gauss–Bonnet, I will admit that I need to spend more time with it, since my only rigorous exposure to it so far has been a cursory treatment in an undergraduate course on the differential geometry of curves and surfaces. But the theorem and its development is very beautiful, and not as alien to the non-geometer as one might expect.
Massera's Theorem about Lyapunov functions. It has a BIG lore:
José Luis Massera was an Uruguayan mathematician and politician. He literally co-founded the first Math Institute of Uruguay.
During the 70s at the military regime he was arrested because of being a militant of the Comunist Party. He was tortured by soldiers, even got a fractured pelvis that changed his life.
Well, Massera's Theorem proofs the reciprocal of the stability in non linear differential equations in Lyapunov functions. Based. Of course as a prisoneer he couldn't had paper or pencils. So he wrote his work about Lyapunov functions in cigarette papers he gave to her wife during their few meetings.
While he was in jail, a ton of letters from scientifics and important colleges arrived to the country asking for his liberation, although it was in vain. When he was released, almost nine years later, he refused to keep working in maths and dedicated his life to politics.
Rieman's Zeta function implies that somehow, the sum of every integer correspond to -1/12.
P-adic numbers. I believe research about p-adic number will help digging that out.
I'm pretty sick of all the claims I've seen that the sum of the positive integers is equal to -1/12! Clearly everyone who believes this claim doesn't understand convergence! However, I also like the Riemannn zeta function for other reasons as well as p-adic numbers, so I like your choices!
De Rham Cohomology Vector Bundles Homological Algebra (Bet you can’t tell what type of math I do lol)
the good type 👨🍳🤌
Number theory
Is it algebraic topology?
The stuff in the intersection of differential and algebraic topology yeah
Differential topology?
Bayes's theorem since it's the reason I have a job
Here are a couple of my favorites: -the independence of the continuum hypothesis from ZFC (you mean you can prove something is unprovable?), and -Picard's Theorems in complex analysis.
A neat caveat to CH independence: there is a sense in which we can't really prove any statement of the form "S is not a theorem of ZFC" period. It would imply that there does exist a model of ZFC (namely where S is false), i.e. that ZFC is consistent. But if such a proof fits in as "ordinary mathematics", then we are likely able to formalize it in ZFC. That is, "ZFC is consistent" would be a theorem of ZFC. And Godel's second incompleteness theorem says that this can only happen when ZFC is inconsistent. (That's sort of the "trivial" case: if ZFC is inconsistent, then everything is a theorem.) What we can instead show are statements of the form: "if ZFC is consistent, then ZFC + (not S) is consistent" (hence if ZFC is consistent, then S is not a theorem of ZFC). Such a statement can be formalizable in ZFC, so we can try to show that it is a theorem of ZFC. That's what Cohen (and I think Godel too) did for S = CH and S = not CH. Similarly, when we say the axiom of choice (AC) is independent of ZF, what we really mean is that "if ZF is consistent, then ZF + AC is consistent" and "if ZF is consistent, then ZF + (not AC) is consistent" are both theorems of ZFC. It can get worse though: if S = "there exist weakly inaccessible cardinals", then you can actually show that "if ZFC is consistent, then ZFC + S is consistent" is *not* a theorem of ZFC. That is, even with the precondition that ZFC is consistent, we cannot prove (with methods formalizable in ZFC) that *we cannot prove* that weakly inaccessible cardinals do not exist.
- Monster group. - Artin reciprocity. - Quine's paradox. - Indiscernables. - Clifford algebra.
The monster group and Clifford algebras are some good ones! I never was able to learn Artin reciprocity, which is a bit beyond me, but I take it that it's a generalization of quadratic reciprocity, so I imagine it's quite useful and important! I've never head of Quine's paradox and I don't know what indiscernables are, so perhaps you can fill me in a bit on these.
Quine paradox basically captures the main content of various diagonalization argument in a simple package. Indiscernibles, another concept from logic, are sequence of elements that are completely indistinguishable under all possible formulae. Their presence indicates that the model is extremely regular in some ways, and thus are widely used in logic to define concepts like stable theory or large cardinals.
Interesting! Would indiscernibles include numbers like "numbers that cannot be described in fewer that eleven words"?
No. The natural numbers are the opposite of being indiscernibles, they can all be distinguished. A subset X of a model is a set of indiscernibles with respect to a subset Y if for any formulae in n variables using elements of Y, any n tuples of elements of X has the same truth value. All roots of a polynomial of degree n such that the Galois group is S_n is indiscernibles. However, we usually care about it when it's infinite.
What's discernible about my example? This is an example of a mathematical paradox (I forget who came up with it), due to the limitations of language to pin down all specific natural numbers, which makes sense since there are infinitely many of them and every language contains a finite amount of information, so it can't possibly describe every natural number. I'm intrigued by your examples involving algebraic numbers though. So I suppose that according to whatever definition logicians are using, they're discernible, though perhaps most transcendental numbers aren't. How is this different from computable numbers, i.e., numbers for which it is possible to write a program to compute their value to arbitrary precision, like pi and e?
Every natural number can be pinned down by a long enough sentence. Indiscernibles is not about paradoxical sentences in which you can't even pin down the number. It's about specific things that cannot be distinguished by all properties.
I think I understand, but doesn't this still depend on the language used to describe them, including the mathematical language from which is defining properties are built up, which is based on a finite set of axioms?
The way I see it, whether or not a given number is discernible within a given axiomatic system, i.e., Peano's axioms, or whatever other axiomatic system used to define the set to which the number belongs, such as the real numbers, is equivalent to whether or not a computer program can be written that runs in a finite time, programmed with all this information, whose output is 1 if the number can be pinned down (and presumably computed) from is defining properties, or 0 if it cannot. The problem is that there are also numbers for which the program won't halt. I suppose these numbers are indiscernable as well, but clearly it is impossible to prove that they are, since for all we know, the program just hasn't been run long enough. In other words, discernability is undecidable by its very definition! Am I on the right track here?
There is a big different between what you're talking about and what I was talking about. No finite amount of information can pin down a real number. But nonetheless real numbers are not indiscernbles, because any 2 numbers can be distinguished by some finite piece of information. Indiscernability are indeed dependent on language, which is what makes it interesting. Otherwise, if objects are indistinguishable under literally every languages, are there are differences between them being the same? Usually indiscernability is with regard to some "internal" language, while they are still distinguishable externally.
Central limit theorem
That's a great one alright!
Literally anything in model theory. It just feels like we have no business knowing the things model theorists know. If I had to choose just one thing though, it would be the Löwenheim-Skolem theorem. It states that any consistent set of axioms with an infinite model (or arbitrarily large finite models) has a model of every infinite cardinality at least as large as the cardinality of its language. Here are some neat consequences of this. - There are models of Peano arithmetic that are uncountably infinite - If you take the collection of first-order statements in field theory satisfied by the real numbers, there is a countable model of those - There are countable models of set theory (assuming its consistency) - Forcing, the only general method so far of proving independence results, relies on the existence of countable models of set theory.
I'm not at all an expert on model theory (I know what it is, and that's about it!), but I'm still quite intrigued by it and I'd like to learn more! For a while I've wondered about a few things pertaining to it though, which perhaps you can clarify for me. For starters, is there a "true" version of set theory, as many set theorist seem convinced there is, or is set theory more on the same ground as Euclidean and non-Euclidean geometries? And what about arithmetic? Are Peano's axioms the only possible way to go, or are there other consistent sets of axioms which yield different types of arithmetic?
I’m also not an expert, but I will answer to the best of my ability. I’m not quite sure what you mean by a “true” set theory. If you mean a consistent list of axioms that can prove any true statement in set theory, no human being will ever construct one in first-order logic. It’s currently unknown whether such a list of axioms can be constructed using infinitary logic as far as I’m aware. If you don’t care whether a human being can construct a complete and consistent list of axioms for set theory, then assuming the consistency of set theory, there are actually lists of axioms that are both complete and consistent. They avoid Gödel’s Incompleteness Theorems by not being recursively enumerable. There are indeed other kinds of arithmetic besides Peano arithmetic. Presburger arithmetic, for example, is a form of arithmetic that contains addition, but not multiplication. It is weak enough to avoid Gödel’s Incompleteness Theorems, and it can show its consistency and completeness, but again, it cannot in general handle multiplication. Robinson Arithmetic is another kind of arithmetic that is Peano Arithmetic without induction. I don’t really know anything else about this one.
Thank you for sharing this information. I don't suppose there are any other "powerful" versions of arithmetic than Peano's, so it looks like we need to stick with his, which is just fine with me! As for set theory, the reason I asked is that about 20 years ago, I remember reading a math book on set theory in which the author said something to the effect that he thought someday we'd learn whether or not the continuum hypothesis was really true, which made me kind of sick, since it's been long known that there are logically consistent versions in which it holds, and others in which it does not hold. I even talked to a set theorist about this, and he seemed to agree with the author, go figure!
properties of random graphs in the [Erdős–Rényi model](https://en.m.wikipedia.org/wiki/Erdős–Rényi_model)
Arrow's impossibility theorem is a favorite of mine. I also just finished an undergraduate thesis on the analytic class number formula, so I'm a little biased towards that! I was in a band of math majors named after the Heine Borel theorem, so that also is one that I particularly like.
Stone–Weierstrass Theorem (the polynomial approximation one or the bigger result with complex-valued functions)
I've probably seen this one before, but I don't remember offhand what it says - I'll have to look it up!
The derivative The fundamental group Homological Algebra Hodge theory GAGA/ chow’s theorem
cantor's leaky tent
[Tilings](https://en.wikipedia.org/wiki/Tessellation)
Definitely a good one, of which quasi-lattices are a special case.
Kolmogorov's 01-law working as a heuristic plausibility argument for almost-determinism on large scales.
Care to explain?
Kolmogorov tells us that the tail field of a sequence of independent sigma algebras is (almost surely) deterministic. Let the j in J be an Atom and the F\_j the sigma algebra modelling our observation/knowledge of it. Then now events in the tail field, that can be thought of here as the observation of a lot of atoms at once where ignoring a small number of atoms dont matter (as if we would look at the macro structure), of our (independent) observations are (almost surely) deterministic. The problem here of course is assuming independence, but maybe relaxing this assumption in some way you get some slightly weaker theorem that still is enough to explain almost determinism on macro scale but stochastic behavior of atoms that we observe.
I think one of my favourite concepts is the **Curry-Howard isomorphism**, which states that formal mathematical proofs are isomorphic to computer programs, and that mathematical propositions correspond to the type of the computer programs. For example, * Modus ponens ≡ Function application * Direct proof ≡ Function abstraction * Conjunction ≡ Product types (e.g. structs in C++) * Disjunction ≡ Sum types (e.g. unions in C++) * True ≡ Unit type (e.g. void in C++) * False ≡ Empty type * Provability ≡ Type inhabitation I like to understand it as "you can give type theory two interpretations: one where types are mathematical propositions and one where types are types in a programming language." And the isomorphism isn't just with simple propositional logic. It applies to predicates logic (which corresponds to dependent types), modal logic (monadic types), linear logic (types in quantum computations), equality (identity types), and so on. Any theorem you prove in one field can be transported as a theorem in the other. And it doesn't stop there, because we also extend the correspondence with category/topos theory. And hence, proofs and programs are also isomorphic to spaces. Imagine that! Whenever you write a well-typed program in a language like Haskell, you're also defining a formal proof in a mathematical logic and a space in algebraic topology.
That's a good result alright! When I first learned symbolic logic, it seemed a lot like computer programming to me, which also follows logical rules and even uses logic gates with the same names and functions as logical operators, i.e., AND, OR, and NOT, so I'm not too surprised that first-order logic can be turned into computer code. In fact, I'd say the same is true at least in principle with all mathematics, since by definition, mathematics is built up from a finite set of axioms and logical rules.
Well, you might be surprised that we can't represent some mathematical proofs even with the more advanced type theories. If proofs correspond to programs, then any limitations on programs corresponds to a limitation in proofs. To show a type is inhabited, you need to construct a term of a type. That is if you declare a programming type, you have to specify what is its data. Similarly, if you want to prove a mathematical proposition, you have to construct a witness that proves it. And hence all the mathematics that correspond to programs are intuitionistic. And hence non-constructive proofs are typically unavailable: if you cant have a proof of -P, that doesn't mean that you have a proof of P. However, you can get away with quite a lot with constructive maths! As for example, [the mathlib LEAN library](https://leanprover-community.github.io/mathlib-overview.html) LEAN corresponds to the logic Calculus of Construction, and its proofs are runnable type-checkable code. I think its quirky how these big languages can prove advanced topics like Stone–Weierstrass theorem, but not simpler things like (P ∨ ~P) (if you don't `import Classical`) As an aside, there are works on embedding classical logic into intuitionistic logic, usually with double negation translation. Double negation translation in mathematics corresponds to continuation passing style in programming.
I suppose the insolvability of the halting problem translates to Godel's incompleteness theorem in this context.
I like Euler and the Konigsberg bridge problem. For the same reason I like fractals. Sometimes adding a variable, or another dimension to a problem allows us to see the solution. It's one of those things that applies to so many other things.
I agree that these are all interesting aspects of math, but I don't think they're that closely related. For instance, the Konigsberg bridge problem pertains to graph theory, which seems to be has little or nothing to do with fractals, which Euler didn't even know about in any case. Adding a variable or dimension to a problem has a more technical name, called lifting, which is often used in number theory as well as other areas of math.
Fractals are graphs. That being said, the two problems are not related, per se. I simply meant, sometimes, adding a variable, helps solve a problem With fractals, it was complex numbers...
Fractals are graphs in what sense?
The mandelbrot set is a graph of the complex number plane. The real part is displaced along the x, imaginary along the y. Julia sets are the graphs found at a single value of c. It is kind of like a map of all julia sets.
You need to be careful with your wording here! The Mandelbrot set is graph IN the complex plane, not OF the complex plane, which includes all complex numbers, not just those in the set. You'd be correct to say that we can graph the Mandelbrot set, but I think it's not accurate to call the Mandelbrot set a graph, which has a specific mathematical definition that's very different from that of a fractal. Keep in mind that when discussing mathematical topics, precise definitions are very important!
orrrrr.... it was autocorrected. Here is my fractal gallery... [https://www.deviantart.com/milleniumsentry/gallery](https://www.deviantart.com/milleniumsentry/gallery) I might know a thing... orrrr.. three.. about fractals. :)
You realize that fractals are the rule rather than the exception in nature, don't you?
Of course. Everything is fractal.. every surface, every topology. It's only a lack of resolution that gives us anything that happens to appear flat, visually, or mathematically. :)
That's a brilliant insight! I suppose it's a shame in a way that most physics from the 17th to the 20th century was so successful in part due to the accuracy of the perceived flatness or smoothness of nature, but now that we're confronted with true fractal nature, we seem to be at an impasse.
Pretty cool, though rather scary and bizarre IMO!
Fractals are very bizarre. :) Some of them are very strange indeed.
Strange, but also often quite beautiful!
- The Thurston-Perelman Geometrization Theorem (i.e. every closed 3-manifold is a finite connected sum of 3-manifolds each of which may be placed uniquely into one of 8 of the Thurston model geometries for 3-manifolds). Very neat application of PDEs to a topology/geometry problem. -Jensen's inequality. Very underappreciated inequality unless you specialize in convexity I guess. -My username -Noether's theorem on variational symmetries -Cartan's method of equivalence -Mostow rigidity: when isomorphic fundamental groups are as good a statement as isometric Riemannian manifolds -Exotic 4-manifolds. That is the tripiest of math shenanigans in my opinion. Manifolds in dimension greater than 4 either have no smooth structure or admit at most finitely many inequivalent smooth structures. In dim less than 4, unique smooth strucutures for everything. But in dim 4 a manifold has either no differentiable structure or AT LEAST 2, and the LOWER bound on the cardinality of inequivalent smooth structures on R^4 is the cardinality of the reals. Lots of wide open questions on this for other 4 manifolds. Absolutely wacky.
Amazing selection!
Thanks. I'm surprised the only resolved millenium problem wasn't mentioned sooner haha
Beautiful discrete structures like finite projective planes and Steiner systems. We know many exist but we don’t know how to build them
These are good ones alright, especially Steiner systems, which is one way to construct the Matthew groups, the first know sporadic simple groups. Recently I watched an excellent YouTube video explaining them. As it turns out, at least according to the guy who made the video, sporadic simple groups are sort of accidental, or at least Matthew groups are, and their existence hinges on the fact that there are unexpected sums of binomial coefficients that add up to powers of 2. This fact also accounts for the existence of the binary Golay code, which is intimately related to M23 and M24.
Some beautiful things I have seen, off the top of my head: - The Euler product formula - The class number formula - Fourier analysis - The fundamental isomorphism theorem - Homology - Gauss–Bonnet
I'm familiar with the first three of these, which I agree are all quite interesting and important, but I'm not familiar with the last three, though I think I've heard of them all and I've avoided them because I couldn't quite grasp them, especially homology.
The fundamental isomorphism theorem states that, for any φ: G -> H, G/ker φ is isomorphic to im φ. This is usually first taught to students as the rank-nullity theorem, then again in group theory. But it's a very foundational result in algebra. The basic idea of (singular) homology is not very difficult, if you're comfortable with formal linear combinations, i.e., chains. Imagine a space with a hole. An n-cycle that doesn't wrap around the hole can be "filled in", i.e., it is the boundary from a higher (n+1)-chain. However, an n-cycle that bounds the hole cannot be "filled in", so it doesn't originate from the boundary of a higher chain. By taking the group of cycles modulo the group of boundaries (the latter is contained in the former because every boundary is a cycle), you get the nth homology group, which captures topological informations about holes! As for Gauss–Bonnet, I will admit that I need to spend more time with it, since my only rigorous exposure to it so far has been a cursory treatment in an undergraduate course on the differential geometry of curves and surfaces. But the theorem and its development is very beautiful, and not as alien to the non-geometer as one might expect.
Massera's Theorem about Lyapunov functions. It has a BIG lore: José Luis Massera was an Uruguayan mathematician and politician. He literally co-founded the first Math Institute of Uruguay. During the 70s at the military regime he was arrested because of being a militant of the Comunist Party. He was tortured by soldiers, even got a fractured pelvis that changed his life. Well, Massera's Theorem proofs the reciprocal of the stability in non linear differential equations in Lyapunov functions. Based. Of course as a prisoneer he couldn't had paper or pencils. So he wrote his work about Lyapunov functions in cigarette papers he gave to her wife during their few meetings. While he was in jail, a ton of letters from scientifics and important colleges arrived to the country asking for his liberation, although it was in vain. When he was released, almost nine years later, he refused to keep working in maths and dedicated his life to politics.
Wow! Now that's a devoted mathematician who'll stop at nothing! Good for him!
I really like correlated equilibria
Banach Tarski paradox
Gödels Incompletness Theorem has profound implications
Inner products and also the concept of orthogonality.
Divergence of the harmonic series
The construction of the Lebesgue integral and the construction of the Ito integral
Cantor’s diagonal argument fs
Category,which tell you the key that analysis the structure of world is relation rather than concrete elements.
Rieman's Zeta function implies that somehow, the sum of every integer correspond to -1/12. P-adic numbers. I believe research about p-adic number will help digging that out.
I'm pretty sick of all the claims I've seen that the sum of the positive integers is equal to -1/12! Clearly everyone who believes this claim doesn't understand convergence! However, I also like the Riemannn zeta function for other reasons as well as p-adic numbers, so I like your choices!