12 ms·

What do we mean by "the foundations of mathematics"?

139 points by JoelMcCracken 3y ago

daoboy 3y ago
A good opportunity to break out my favorite Bertrand Russell quote: "Everything is vague to a degree you do not realize till you have tried to make it precise."
hiAndrewQuinn 3y ago
Category theory is a pretty good one. But I think a lot of people would get a surprising amount of value from reading Halmos's slim _Naive Set Theory_, to see just how much work we can create using sets alone.
- Koshkin 3y ago
  “A pretty good one.” Right. The amount of generalization and insight is incomparable.
  - zmgsabst 3y ago
    And yet, there are times to use the other theories: Eg, type theory has more succinct proofs of unique inverses.
  - hiAndrewQuinn 3y ago
    Let me qualify my claim. I'm thinking of the average HN reader, who is a software professional who may never have touched proof based math before - not you or I who got a perfect score on the abstract algebra final after skipping linear. _Naive Set Theory_ was a much faster and more accessible read than even _Seven Sketches in Compositionality_ for me, and correspondingly I read it much earlier in my mathematical life. Seeing the natural numbers defined in Chapter 17 or so out of the building blocks of sets alone, more as an afterthought / convenience, was indeed what got me interested in taking a math minor in the first place. And it took, what, two weeks of self study for me to get to that point? Fantastic ROI.
deleted 3y ago
[deleted]
btilly 3y ago
We can't define "foundations of mathematics" without defining mathematics. My favorite stab at this is from Thurston's On Proof and Progress in Mathematics. Which may be read in full at https://www.math.toronto.edu/mccann/199/thurston.pdf https://www.math.toronto.edu/mccann/199/thurston.pdf: Could the difficulty in giving a good direct definition of mathematics be an essential one, indicating that mathematics has an essential recursive quality? Along these lines we might say that mathematics is the smallest subject satisfying the following: - Mathematics includes the natural numbers and plane and solid geometry. - Mathematics is that which mathematicians study. - Mathematicians are those humans who advance human understanding of mathematics. In other words, as mathematics advances, we incorporate it into our thinking. As our thinking becomes more sophisticated, we generate new mathematical concepts and new mathematical structures: the subject matter of mathematics changes to reflect how we think. The foundations of mathematics then refers to the essential core that we have based our mathematical thinking on. Which is something that most of us only wish to think about when our thinking has run into problems and we need a better foundation.
- vlovich123 3y ago
  Is mathematics just the study of all possible languages that are constructed from strict internally consistent rules?
  - saalweachter 3y ago
    Mathematics is the study of things you can convince people are true without physical evidence.
    - adastra22 3y ago
      I like this one. Succinct and to the point. However this would also include religion :\
      - saalweachter 3y ago
        Two different religionists can have a conversation and agree on what is true?
westurner 3y ago
https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... : > Today, Zermelo–Fraenkel set theory [ZFC], 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. Foundation of mathematics: https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics Implementation of mathematics in set theory: https://en.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory https://en.wikipedia.org/wiki/Implementation_of_mathematics_... : > The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) and in NFU, the version of Quine's New Foundations shown to be consistent by R. B. Jensen in 1969 (here understood to include at least axioms of Infinity and Choice). > What is said here applies also to two families of set theories: on the one hand, a range of theories including Zermelo set theory near the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundations article. These correspond to different general views of what the set-theoretical universe is like IEEE-754 specifies that float64s have ±infinity and specify ZeroDivisionError. Symbolic CAS with MPFR needn't be limited to float64s. HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT https://github.com/HoTT/Coq-HoTT What is the relation between Coq-HoTT & Homotopy Type Theory and Set Theory with e.g. ZFC? Homotopy Type Theory: https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory : > "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities" (2018) https://scholar.google.com/scholar?cites=9763697449338277760&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=9763697449338277760... and sorted by date: https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=0,43&cites=9763697449338277760&scipsc=&q=&scisbd=1 https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=... What does Mathlib have for SetTheory, ZFC, NFU, and HoTT? leanprover-community/mathlib4// Mathlib/SetTheory: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/SetTheory https://github.com/leanprover-community/mathlib4/tree/master...
- JonChesterfield 3y ago
  Homotypy is a constructive one. It drops the assumption that any given proposition is either true or false, on the grounds that lots of propositions are undecidable and that's fine. A consequence of no law of the excluded middle (the p or ~p one) is no axiom of choice, so ZFC isn't going to be compatible with it, but ZF probably is. Personally I'm convinced constructive maths is the right choice and will cheerfully abandon whatever wonders the axiom of choice provides to mathematics, because I'm not a mathematician and I care about computable functions.
nyc111 3y ago
Mathematics is built on definitions. There are definitions on the foundations of mathematics. Axioms are definitions that are kept constant by consensus. Euclid starts with definitions. If you don't like Euclid's definitions you make your own definitions. You create your own geometry etc.
- deltasepsilon 3y ago
  Okay, but where do the definitions come from and what do they refer to? If you don't care, fine. You simply are only concerned with the utility of this so called "mathematics". But at some point, and with some sophistication, you get bothered about how well it all works and how some surprising connections are made that seem all too natural. Then you end up writing an essay like Wigner. [1] I write this to say, no wonder people are bothered about a "foundations". Whether it bothers you or not is immaterial, but you can understand why people get bothered. [1] https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness_of_Mathematics_in_the_Natural_Sciences https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...
smokel 3y ago
For those who like to read biographies of the brilliant minds, instead of the actual mathematics they produced, I can highly recommend "Journey to the Edge of Reason: The Life of Kurt Gödel" (2021) by Stephen Budiansky, which is nice.
wisnesky 3y ago
A foundation for mathematics is any formalism sufficient to prove the results typically taken as axioms in practical mathematics. For example, in ZFC you can define numbers as sets in many different ways and prove that 1+1=2 for each of them - other foundations include higher order logic, topos theory, other set theories, etc.
- wubrr 3y ago
  Is it also possible to define set theory in terms of arithmetic?
  - wisnesky 3y ago
    Yes, at least with a strong enough arithmetic (such as Peano's), but that is usually more complicated; for example, you might have to create a Godel numbering or some other "deep embedding" to represent each set as a number. There's also so-called "reverse mathematics", which tries to determine the weakest axiom system capable of establishing a particular result.
    - wubrr 3y ago
      Interesting, thanks!
  - Kranar 3y ago
    You can certainly define some set theories using arithmetic but arithmetic as formalized by first-order Peano arithmetic can not define a set theory powerful enough to prove results about uncountable sets, such as large cardinal axioms or even properties of real numbers.
    - wubrr 3y ago
      Any links/examples of why this isn't possible? My thinking is - if all existing set theory and set theoretic proofs are expressed in finite set-theoretic statements/expressions - can't we 'encode' these expressions within the system of arithmetic?
tromp 3y ago
Jeremy Avigad made available a 54-page draft chapter on mathematical logic and foundations [1]. Quoting from the abstract: > The formal foundation of a proof assistant is the formal deductive system with respect to which the correctness of the proof assistant’s implementation is judged. The foundation specifies a language for defining objects and saying things about them, and it determines the means that can be used to prove that such statements are true. This chapter presents some general background in logic that is helpful for thinking and reasoning about formal systems, and it describes the three main families of foundations that are commonly used in proof assistants today. [1] https://arxiv.org/abs/2009.09541 https://arxiv.org/abs/2009.09541
- _aaed 3y ago
  Thank you friend
cjfd 3y ago
I have a project to write a proof assistant that is as simple as possible while still usable. A kind of turing tar pit but for proofs instead of programs. Some early attempts did not quite work out. I try to get it off the ground using the calculus of constructions (not the calculus of inductive constructions) together with a small set of axioms. As axioms I aim, at the moment, to use a hilbert epsilon operator to contstruct objects from theorems that state their existence, proof irrelevance and an infinity axiom that states that an infinite set exists. Also I do use an infinite hierarchy of Types a bit like the universes of coq. I am still debating with myself whether I also should provide the luxury of not having to specify universe levels and just keep constraints between them like in coq. The article proposes the calculus of inductive constructions but I think that is just too big and complicated to be a good candidate for a foundation of mathematics. I think it makes more sense to use a more concise foundation and maybe attempt to prove that the calculus of inductive constructions is a conservative extension of that.
- bvssvni 3y ago
  Is your goal to have as few axioms as possible, or as few syntactic constructions as possible?
  - cjfd 3y ago
    Both really. Just as few givens as possible whether they are baked in or added on as axioms.
- zarzavat 3y ago
  The calculus of inductive constructions is not very big? It seems simpler than ZFC to me. The version that Coq uses is quite large, but that's the difference between theory and practice: Coq is designed to be maximally usable not minimally simple.
  - cjfd 3y ago
    Well, inductive constructions need positivity conditions to be consistent. These are complicated enough to suggest that they need to be proven instead of accepted as part of the formal system.
aaimnr 3y ago
Reminds me of Wilfrid Sellars: “The aim of philosophy, abstractly formulated, is to understand how things in the broadest possible sense of the term hang together in the broadest possible sense of the term”. "Hanging together" doesn't impose as many assumptions as "having specific foundation". It's a very distinct philosophical stance to assume that any kind of human knowledge has a specific foundation, and a naive one at that.
practal 3y ago
> That the solution could lie in something as simple as Zermelo’s separation axiom and the conception of the cumulative hierarchy of sets was seemingly not anticipated. It was a miracle. If you are a Platonist (I am), then it is not really a miracle. Mathematical objects are real, and logic is a tool to study them. The paradoxes can only exist, because math is real: a paradox shows that something is not real, and if there were no real mathematical objects to begin with, paradoxes would be meaningless. As it stands, a paradox is a tool to distinguish reality from that which is not real. Have fun making any kind of sense if you are a formalist or intuitionist (hint: you can't). It is indeed cool that something as simple as set theory covers so much. But it doesn't cover everything. The Banach-Tarski Paradox shows that sets are not what we imagine them to be (but they are still real): we need to add the property of measurability, which acts then as an additional axiom, to get closer to that. And in order to solve BB(748), ZFC is not enough [0, theorem 7]. So, one set theory is not enough. Depending on which properties we ascribe to sets, or in other words, which axioms we add to set theory, we also get different set theories. > I give up. Set theory is cool, but it is not special. In the end it describes a fragment of the (real) mathematical universe, but there is more to this universe than just set theory. And depending on which properties you pick for your sets, you get different fragments. It is interesting that Larry says that Automath is not a Foundation, and that neither is Isabelle, which he created. Maybe I am putting words in his mouth here, but that is how I interpret his "Isabelle/Pure is in the same spirit". I think he is right. BUT, Isabelle is SO close to a foundation. All you have to do is to drop the types :-D. All of them. That's what I did, and you then basically get Abstraction Logic [1]. Abstraction Logic makes no assumptions whatsoever about your mathematical universe, except that it is non-empty, and it better have more than 1 object in it. It doesn't assume that sets exist, or types, or anything else. It doesn't force you to define natural numbers or other mathematical objects as sets. You can define any operator you want, and with each choice of axioms you are exposed to the risk of doing nonsense and creating paradoxes. And therefore I believe it is the right foundation for mathematics, and I think it is the only right one. Yes, there is a single logical foundation. Sounds too simple? So did set theory. Yes, I think Abstraction Logic is a miracle, but on the other hand, it simply manifests logic as it is. [0] https://www.scottaaronson.com/papers/bb.pdf https://www.scottaaronson.com/papers/bb.pdf, page 12, theorem 7 [1] http://abstractionlogic.com http://abstractionlogic.com
wannabebarista 3y ago
For those interested in recent systematic discussions of foundations, I find Penelope Maddy's recent work compelling. For instance, see the paper "What do we want a foundation to do?" [0] [0] https://sites.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want%20-%20final https://sites.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20w...
lacker 3y ago
100 years ago everyone was worrying about whether the foundations of mathematics were consistent. We figured out some details that we had been taking for granted, like the axiom of choice, how to prevent Russell's paradox, and the inevitable difference between "true" and "provable" (ie Godel's incompleteness). Now that part is pretty much solved, we are fairly confident that the foundations of mathematics are consistent. IMHO the problem now is that the foundations of mathematics are impractical. Most mathematicians don't actually do mathematics that can be tied back to the foundational axioms. It seems like it should be possible, in theory, but it takes too much work. So most mathematicians prefer communicating their proofs in PDFs rather than in a more rigorous format.
- bvssvni 3y ago
  One thing I would like point out with Gödel's incompleteness theorems, is that there are different notions of provability. Gödel uses the notion of "provability" you get from Provability Logic, which is a modal logic where you introduce terms from e.g. Sequent Calculus. Recently I found another notion of "provability" where Löb's axiom, required in Provability Logic, is absurd. It turns out that this notion fits better with Intuitionistic Propositional Logic than Provability Logic. This allows integrating the meta-language into object-language. This is pretty recent, so I think we still have much to learn about the foundations of mathematics.
  - layer8 3y ago
    > Recently I found another notion of "provability" Any pointers to that alternative notion?
    - bvssvni 3y ago
      I'm implementing it in this project: https://crates.io/crates/hooo https://crates.io/crates/hooo
  - drdeca 3y ago
    This makes it kind of sound as if Löb's axiom is used in the proof of Gödel's incompleteness theorems, but Gödel was working in (I think) PA, not in Provability Logic? I guess you just meant "the notion of provability is the same as the one that would later be described in Provability logic" ? I viewed the page you linked, but I don't see anywhere where you describe the alternate notion of "provability" you have in mind. "Provability" in the sense of Gödel's incompleteness theorems, is just, "There exists a proof of it in [the chosen system of axioms + rules of inference]", yes? I don't see how any other notion would be fitting of the name "provability". "provable" , "possible to prove", "a proof exists", all the same thing? Oh, I guess, if you want to use "there exists" in a specifically constructive/intuitionistic way? (so that to prove "[]P" you would have to show that you can produce a proof of P?) I think I've seen other people try to do away with the need for a meta-language / make it the same as the object-language, and, I think this generally ends up being inconsistent in the attempts I've seen? edit: I see you have written 'Self quality a ~~ a is equivalent to ~a, which is called a "qubit".' I don't know quite what you mean by this, but, _please_ do not call this a qubit, unless you literally mean something whose value is a vector in a 2d Hilbert space.
bvssvni 3y ago
The foundations of mathematics are all about language design. To answer this question, one must say something about which language a foundation of mathematics is using. For example, Set Theory is formalized in First Order Logic. However, First Order Logic uses Propositional Logic, so to build an alternative foundation to Set Theory, you might consider starting with Propositional Logic and extending it another way. First Order Logic extends Propositional Logic with predicates. This might seem like a good design at first, until you try to reason about uniqueness. In Set Theory, one requires an equality operator in addition to set membership, in order to be able to reason about uniqueness, at all. This equality operator is ugly, because you have to rebuild objects that are isomorphic but using different encodings. Predicates causes problems because they are unconstrained. For easier formalizing of advanced theories, I suggested Avatar Logic, which replaces predicates with binary relations, avatars and roles. You can try it here: https://crates.io/crates/avalog https://crates.io/crates/avalog Also, most theories assume congruence for all predicates, which is bad for e.g. foundations of randomness. The next crisis in "the foundations of mathematics" will be "tautological congruence". Luckily, this is already being worked on, by extending Intuitionistic Propositional with exponential propositions. This theory is known as "HOOO EP" and is demonstrated here: https://crates.io/crates/hooo https://crates.io/crates/hooo
- dboreham 3y ago
  Yes. Although my take on this is that it's about VM design, or the ISA for a VM upon which mathematics runs.
  - zmgsabst 3y ago
    Modern mathematics deals with ISA design from the perspective of application: A CPU, an FPGA, and an GPU are all Turing complete substrates, yet they’re useful for wildly different things. Category theory, type theory, and set theory all can embed arbitrary mathematics — but the encodings you get lend themselves to different applications. Eg, category theory is very useful at abstracting structures to check if they’re “the same”.
- JonChesterfield 3y ago
tutfbhuf 3y ago
I'm a bit sad the he doesn't mention univalent foundations, which is based on ∞-groupoids instead of sets.
graycat 3y ago
(1) Common K-12 math. (2) A text on set theory, especially axiomatic set theory. (3) Abstract algebra, i.e., the natural numbers, the rationals, the reals, the complex numbers, the basic properties, and some on groups, rings, fields, and vector spaces. That's enough for the foundations.
Koshkin 3y ago
> The objects in category theory are equipped with structure I am sure everything else in the article is correct.
- JonChesterfield 3y ago
  The sentence parses here - the objects have associated introduction and elimination rules which get called 'structure' - what error do you see?
  - Koshkin 3y ago
    In the abstract setting, morphisms do not "preserve structure" - they are just arrows, and there is no structure to preserve to begin with.
AndrewKemendo 3y ago
I have studied math for a long time and when you reach the limits of asking a chain of why questions enough it’s basically - we started counting on our fingers (finger bones for the base 60 Babylonians out there) and just went from there. I think the most important aspect of AI is laying bare how human actions are mostly arbitrary and lacking in a formal epistemology that isn’t simply an artifact of human biology
doubloon 3y ago
well technically the word "math" is just greek for "learning" and foundation is something you build a building on top of. https://www.etymonline.com/word/mathematics https://www.etymonline.com/word/mathematics https://www.etymonline.com/word/foundation https://www.etymonline.com/word/foundation this begs the question - why do you need to build a building on top of something? why cant you just build the building on the ground. well its because of the Earth itself, it moves, its unstable, it has water in some places and not in others, sand in some places and not in others, and so forth. different climates and different needs. now this makes me wonder, if you were not born on Earth, but on some place where buildings did not need foundations, would you ever wonder what the foundations of mathematics were? and if you were on a planet where, say, music was considered the ultimate form of knowledge, rather than you know, high frequency trading algorithms or dark patterns to drive advertising engagement, would the connotation of math be entirely different and would the meaning of the word math have evolved differently?
dwheeler 3y ago
I would have expected to see at least more of a discussion about Metamath. Metamath by itself does not pick any particular foundation. It just lets you state axioms, then prove theorems from axioms and other proven theorems (letting you stack them up). So you can choose your axioms. Set theory with classical logic? Or with intuitionistic logic? Maybe you'd prefer simple type theory? Carry on! That said, the largest Metamath database (set of axioms and proven theorems) is the "Metamath Proof Explorer". It's based on ZFC set theory with classical logic. It turns out that ZFC set theory is quite enough to model structures. This database does add the Tarski–Grothendieck Axiom for certain uses of category theory (the same axiom added by Mizar), but it's only used when it's needed and that is quite rare. Heck, even the axiom of choice turns out to be unneeded in many cases. You certainly don't have to use ZFC with classical logic as your fundamental starting point (indeed, someone who rejected classical logic would not accept it). But you can go a long way with it. More information about Metamath is here: https://us.metamath.org/ https://us.metamath.org/ More information about the Metamath Proof Explorer database (based on ZFC + classical logic) is here: https://us.metamath.org/mpeuni/mmset.html https://us.metamath.org/mpeuni/mmset.html
- pilgrim0 3y ago
  The way you put it, I find it pretty fucking interesting. Thanks for the comment.
- JonChesterfield 3y ago
  Metamath is superb. Linear time proof checking is especially good. I haven't got past the distinct variable side conditions, though it's an interesting take on the variable free in term / capture avoiding substitution equivalent in lambda calculus.
galaxyLogic 3y ago
Doesn't it all come down to: What is the meaning of "is"? Mathematics is all about statements like "a is bigger than b". "3 is prime". Etc. But what is (sic!) the meaning of "is"?
vintermann 3y ago
> Calculus of inductive constructions (Coq, Lean): the original paper (describing a weaker system) begins “The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style,” and the paper makes no foundational claims. Coquand’s retrospective paper makes no such claims either. Since it turns out to be significantly stronger than ZF set theory, Whoa, whoa, hold your horses here. Why didn't THAT claim come with an explanatory hyperlink?

139 points by JoelMcCracken 3y ago

A good opportunity to break out my favorite Bertrand Russell quote: "Everything is vague to a degree you do not realize till you have tried to make it precise."

hiAndrewQuinn 3y ago

Category theory is a pretty good one. But I think a lot of people would get a surprising amount of value from reading Halmos's slim _Naive Set Theory_, to see just how much work we can create using sets alone.

Koshkin 3y ago
“A pretty good one.” Right. The amount of generalization and insight is incomparable.
- zmgsabst 3y ago
  And yet, there are times to use the other theories: Eg, type theory has more succinct proofs of unique inverses.
- hiAndrewQuinn 3y ago
  Let me qualify my claim. I'm thinking of the average HN reader, who is a software professional who may never have touched proof based math before - not you or I who got a perfect score on the abstract algebra final after skipping linear. _Naive Set Theory_ was a much faster and more accessible read than even _Seven Sketches in Compositionality_ for me, and correspondingly I read it much earlier in my mathematical life. Seeing the natural numbers defined in Chapter 17 or so out of the building blocks of sets alone, more as an afterthought / convenience, was indeed what got me interested in taking a math minor in the first place. And it took, what, two weeks of self study for me to get to that point? Fantastic ROI.

deleted 3y ago

[deleted]

btilly 3y ago

We can't define "foundations of mathematics" without defining mathematics. My favorite stab at this is from Thurston's On Proof and Progress in Mathematics. Which may be read in full at https://www.math.toronto.edu/mccann/199/thurston.pdf https://www.math.toronto.edu/mccann/199/thurston.pdf: Could the difficulty in giving a good direct definition of mathematics be an essential one, indicating that mathematics has an essential recursive quality? Along these lines we might say that mathematics is the smallest subject satisfying the following: - Mathematics includes the natural numbers and plane and solid geometry. - Mathematics is that which mathematicians study. - Mathematicians are those humans who advance human understanding of mathematics. In other words, as mathematics advances, we incorporate it into our thinking. As our thinking becomes more sophisticated, we generate new mathematical concepts and new mathematical structures: the subject matter of mathematics changes to reflect how we think. The foundations of mathematics then refers to the essential core that we have based our mathematical thinking on. Which is something that most of us only wish to think about when our thinking has run into problems and we need a better foundation.

vlovich123 3y ago
Is mathematics just the study of all possible languages that are constructed from strict internally consistent rules?
- saalweachter 3y ago
  Mathematics is the study of things you can convince people are true without physical evidence.
  - adastra22 3y ago
    I like this one. Succinct and to the point. However this would also include religion :\
    - saalweachter 3y ago
      Two different religionists can have a conversation and agree on what is true?

westurner 3y ago

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... : > Today, Zermelo–Fraenkel set theory [ZFC], 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. Foundation of mathematics: https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics Implementation of mathematics in set theory: https://en.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory https://en.wikipedia.org/wiki/Implementation_of_mathematics_... : > The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) and in NFU, the version of Quine's New Foundations shown to be consistent by R. B. Jensen in 1969 (here understood to include at least axioms of Infinity and Choice). > What is said here applies also to two families of set theories: on the one hand, a range of theories including Zermelo set theory near the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundations article. These correspond to different general views of what the set-theoretical universe is like IEEE-754 specifies that float64s have ±infinity and specify ZeroDivisionError. Symbolic CAS with MPFR needn't be limited to float64s. HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT https://github.com/HoTT/Coq-HoTT What is the relation between Coq-HoTT & Homotopy Type Theory and Set Theory with e.g. ZFC? Homotopy Type Theory: https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory : > "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities" (2018) https://scholar.google.com/scholar?cites=9763697449338277760&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=9763697449338277760... and sorted by date: https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=0,43&cites=9763697449338277760&scipsc=&q=&scisbd=1 https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=... What does Mathlib have for SetTheory, ZFC, NFU, and HoTT? leanprover-community/mathlib4// Mathlib/SetTheory: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/SetTheory https://github.com/leanprover-community/mathlib4/tree/master...

JonChesterfield 3y ago
Homotypy is a constructive one. It drops the assumption that any given proposition is either true or false, on the grounds that lots of propositions are undecidable and that's fine. A consequence of no law of the excluded middle (the p or ~p one) is no axiom of choice, so ZFC isn't going to be compatible with it, but ZF probably is. Personally I'm convinced constructive maths is the right choice and will cheerfully abandon whatever wonders the axiom of choice provides to mathematics, because I'm not a mathematician and I care about computable functions.

nyc111 3y ago

Mathematics is built on definitions. There are definitions on the foundations of mathematics. Axioms are definitions that are kept constant by consensus. Euclid starts with definitions. If you don't like Euclid's definitions you make your own definitions. You create your own geometry etc.

deltasepsilon 3y ago
Okay, but where do the definitions come from and what do they refer to? If you don't care, fine. You simply are only concerned with the utility of this so called "mathematics". But at some point, and with some sophistication, you get bothered about how well it all works and how some surprising connections are made that seem all too natural. Then you end up writing an essay like Wigner. [1] I write this to say, no wonder people are bothered about a "foundations". Whether it bothers you or not is immaterial, but you can understand why people get bothered. [1] https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness_of_Mathematics_in_the_Natural_Sciences https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...

smokel 3y ago

For those who like to read biographies of the brilliant minds, instead of the actual mathematics they produced, I can highly recommend "Journey to the Edge of Reason: The Life of Kurt Gödel" (2021) by Stephen Budiansky, which is nice.

wisnesky 3y ago

A foundation for mathematics is any formalism sufficient to prove the results typically taken as axioms in practical mathematics. For example, in ZFC you can define numbers as sets in many different ways and prove that 1+1=2 for each of them - other foundations include higher order logic, topos theory, other set theories, etc.

wubrr 3y ago
Is it also possible to define set theory in terms of arithmetic?
- wisnesky 3y ago
  Yes, at least with a strong enough arithmetic (such as Peano's), but that is usually more complicated; for example, you might have to create a Godel numbering or some other "deep embedding" to represent each set as a number. There's also so-called "reverse mathematics", which tries to determine the weakest axiom system capable of establishing a particular result.
  - wubrr 3y ago
    Interesting, thanks!
- Kranar 3y ago
  You can certainly define some set theories using arithmetic but arithmetic as formalized by first-order Peano arithmetic can not define a set theory powerful enough to prove results about uncountable sets, such as large cardinal axioms or even properties of real numbers.
  - wubrr 3y ago
    Any links/examples of why this isn't possible? My thinking is - if all existing set theory and set theoretic proofs are expressed in finite set-theoretic statements/expressions - can't we 'encode' these expressions within the system of arithmetic?

tromp 3y ago

Jeremy Avigad made available a 54-page draft chapter on mathematical logic and foundations [1]. Quoting from the abstract: > The formal foundation of a proof assistant is the formal deductive system with respect to which the correctness of the proof assistant’s implementation is judged. The foundation specifies a language for defining objects and saying things about them, and it determines the means that can be used to prove that such statements are true. This chapter presents some general background in logic that is helpful for thinking and reasoning about formal systems, and it describes the three main families of foundations that are commonly used in proof assistants today. [1] https://arxiv.org/abs/2009.09541 https://arxiv.org/abs/2009.09541

_aaed 3y ago
Thank you friend

cjfd 3y ago

I have a project to write a proof assistant that is as simple as possible while still usable. A kind of turing tar pit but for proofs instead of programs. Some early attempts did not quite work out. I try to get it off the ground using the calculus of constructions (not the calculus of inductive constructions) together with a small set of axioms. As axioms I aim, at the moment, to use a hilbert epsilon operator to contstruct objects from theorems that state their existence, proof irrelevance and an infinity axiom that states that an infinite set exists. Also I do use an infinite hierarchy of Types a bit like the universes of coq. I am still debating with myself whether I also should provide the luxury of not having to specify universe levels and just keep constraints between them like in coq. The article proposes the calculus of inductive constructions but I think that is just too big and complicated to be a good candidate for a foundation of mathematics. I think it makes more sense to use a more concise foundation and maybe attempt to prove that the calculus of inductive constructions is a conservative extension of that.

bvssvni 3y ago
Is your goal to have as few axioms as possible, or as few syntactic constructions as possible?
- cjfd 3y ago
  Both really. Just as few givens as possible whether they are baked in or added on as axioms.
zarzavat 3y ago
The calculus of inductive constructions is not very big? It seems simpler than ZFC to me. The version that Coq uses is quite large, but that's the difference between theory and practice: Coq is designed to be maximally usable not minimally simple.
- cjfd 3y ago
  Well, inductive constructions need positivity conditions to be consistent. These are complicated enough to suggest that they need to be proven instead of accepted as part of the formal system.

aaimnr 3y ago

Reminds me of Wilfrid Sellars: “The aim of philosophy, abstractly formulated, is to understand how things in the broadest possible sense of the term hang together in the broadest possible sense of the term”. "Hanging together" doesn't impose as many assumptions as "having specific foundation". It's a very distinct philosophical stance to assume that any kind of human knowledge has a specific foundation, and a naive one at that.

practal 3y ago

> That the solution could lie in something as simple as Zermelo’s separation axiom and the conception of the cumulative hierarchy of sets was seemingly not anticipated. It was a miracle. If you are a Platonist (I am), then it is not really a miracle. Mathematical objects are real, and logic is a tool to study them. The paradoxes can only exist, because math is real: a paradox shows that something is not real, and if there were no real mathematical objects to begin with, paradoxes would be meaningless. As it stands, a paradox is a tool to distinguish reality from that which is not real. Have fun making any kind of sense if you are a formalist or intuitionist (hint: you can't). It is indeed cool that something as simple as set theory covers so much. But it doesn't cover everything. The Banach-Tarski Paradox shows that sets are not what we imagine them to be (but they are still real): we need to add the property of measurability, which acts then as an additional axiom, to get closer to that. And in order to solve BB(748), ZFC is not enough [0, theorem 7]. So, one set theory is not enough. Depending on which properties we ascribe to sets, or in other words, which axioms we add to set theory, we also get different set theories. > I give up. Set theory is cool, but it is not special. In the end it describes a fragment of the (real) mathematical universe, but there is more to this universe than just set theory. And depending on which properties you pick for your sets, you get different fragments. It is interesting that Larry says that Automath is not a Foundation, and that neither is Isabelle, which he created. Maybe I am putting words in his mouth here, but that is how I interpret his "Isabelle/Pure is in the same spirit". I think he is right. BUT, Isabelle is SO close to a foundation. All you have to do is to drop the types :-D. All of them. That's what I did, and you then basically get Abstraction Logic [1]. Abstraction Logic makes no assumptions whatsoever about your mathematical universe, except that it is non-empty, and it better have more than 1 object in it. It doesn't assume that sets exist, or types, or anything else. It doesn't force you to define natural numbers or other mathematical objects as sets. You can define any operator you want, and with each choice of axioms you are exposed to the risk of doing nonsense and creating paradoxes. And therefore I believe it is the right foundation for mathematics, and I think it is the only right one. Yes, there is a single logical foundation. Sounds too simple? So did set theory. Yes, I think Abstraction Logic is a miracle, but on the other hand, it simply manifests logic as it is. [0] https://www.scottaaronson.com/papers/bb.pdf https://www.scottaaronson.com/papers/bb.pdf, page 12, theorem 7 [1] http://abstractionlogic.com http://abstractionlogic.com

wannabebarista 3y ago

For those interested in recent systematic discussions of foundations, I find Penelope Maddy's recent work compelling. For instance, see the paper "What do we want a foundation to do?" [0] [0] https://sites.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want%20-%20final https://sites.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20w...

lacker 3y ago

100 years ago everyone was worrying about whether the foundations of mathematics were consistent. We figured out some details that we had been taking for granted, like the axiom of choice, how to prevent Russell's paradox, and the inevitable difference between "true" and "provable" (ie Godel's incompleteness). Now that part is pretty much solved, we are fairly confident that the foundations of mathematics are consistent. IMHO the problem now is that the foundations of mathematics are impractical. Most mathematicians don't actually do mathematics that can be tied back to the foundational axioms. It seems like it should be possible, in theory, but it takes too much work. So most mathematicians prefer communicating their proofs in PDFs rather than in a more rigorous format.

bvssvni 3y ago
One thing I would like point out with Gödel's incompleteness theorems, is that there are different notions of provability. Gödel uses the notion of "provability" you get from Provability Logic, which is a modal logic where you introduce terms from e.g. Sequent Calculus. Recently I found another notion of "provability" where Löb's axiom, required in Provability Logic, is absurd. It turns out that this notion fits better with Intuitionistic Propositional Logic than Provability Logic. This allows integrating the meta-language into object-language. This is pretty recent, so I think we still have much to learn about the foundations of mathematics.
- layer8 3y ago
  > Recently I found another notion of "provability" Any pointers to that alternative notion?
  - bvssvni 3y ago
    I'm implementing it in this project: https://crates.io/crates/hooo https://crates.io/crates/hooo
- drdeca 3y ago
  This makes it kind of sound as if Löb's axiom is used in the proof of Gödel's incompleteness theorems, but Gödel was working in (I think) PA, not in Provability Logic? I guess you just meant "the notion of provability is the same as the one that would later be described in Provability logic" ? I viewed the page you linked, but I don't see anywhere where you describe the alternate notion of "provability" you have in mind. "Provability" in the sense of Gödel's incompleteness theorems, is just, "There exists a proof of it in [the chosen system of axioms + rules of inference]", yes? I don't see how any other notion would be fitting of the name "provability". "provable" , "possible to prove", "a proof exists", all the same thing? Oh, I guess, if you want to use "there exists" in a specifically constructive/intuitionistic way? (so that to prove "[]P" you would have to show that you can produce a proof of P?) I think I've seen other people try to do away with the need for a meta-language / make it the same as the object-language, and, I think this generally ends up being inconsistent in the attempts I've seen? edit: I see you have written 'Self quality a ~~ a is equivalent to ~a, which is called a "qubit".' I don't know quite what you mean by this, but, _please_ do not call this a qubit, unless you literally mean something whose value is a vector in a 2d Hilbert space.

bvssvni 3y ago

The foundations of mathematics are all about language design. To answer this question, one must say something about which language a foundation of mathematics is using. For example, Set Theory is formalized in First Order Logic. However, First Order Logic uses Propositional Logic, so to build an alternative foundation to Set Theory, you might consider starting with Propositional Logic and extending it another way. First Order Logic extends Propositional Logic with predicates. This might seem like a good design at first, until you try to reason about uniqueness. In Set Theory, one requires an equality operator in addition to set membership, in order to be able to reason about uniqueness, at all. This equality operator is ugly, because you have to rebuild objects that are isomorphic but using different encodings. Predicates causes problems because they are unconstrained. For easier formalizing of advanced theories, I suggested Avatar Logic, which replaces predicates with binary relations, avatars and roles. You can try it here: https://crates.io/crates/avalog https://crates.io/crates/avalog Also, most theories assume congruence for all predicates, which is bad for e.g. foundations of randomness. The next crisis in "the foundations of mathematics" will be "tautological congruence". Luckily, this is already being worked on, by extending Intuitionistic Propositional with exponential propositions. This theory is known as "HOOO EP" and is demonstrated here: https://crates.io/crates/hooo https://crates.io/crates/hooo

dboreham 3y ago
Yes. Although my take on this is that it's about VM design, or the ISA for a VM upon which mathematics runs.
- zmgsabst 3y ago
  Modern mathematics deals with ISA design from the perspective of application: A CPU, an FPGA, and an GPU are all Turing complete substrates, yet they’re useful for wildly different things. Category theory, type theory, and set theory all can embed arbitrary mathematics — but the encodings you get lend themselves to different applications. Eg, category theory is very useful at abstracting structures to check if they’re “the same”.
JonChesterfield 3y ago

tutfbhuf 3y ago

I'm a bit sad the he doesn't mention univalent foundations, which is based on ∞-groupoids instead of sets.

graycat 3y ago

(1) Common K-12 math. (2) A text on set theory, especially axiomatic set theory. (3) Abstract algebra, i.e., the natural numbers, the rationals, the reals, the complex numbers, the basic properties, and some on groups, rings, fields, and vector spaces. That's enough for the foundations.

Koshkin 3y ago

> The objects in category theory are equipped with structure I am sure everything else in the article is correct.

JonChesterfield 3y ago
The sentence parses here - the objects have associated introduction and elimination rules which get called 'structure' - what error do you see?
- Koshkin 3y ago
  In the abstract setting, morphisms do not "preserve structure" - they are just arrows, and there is no structure to preserve to begin with.

AndrewKemendo 3y ago

I have studied math for a long time and when you reach the limits of asking a chain of why questions enough it’s basically - we started counting on our fingers (finger bones for the base 60 Babylonians out there) and just went from there. I think the most important aspect of AI is laying bare how human actions are mostly arbitrary and lacking in a formal epistemology that isn’t simply an artifact of human biology

doubloon 3y ago

well technically the word "math" is just greek for "learning" and foundation is something you build a building on top of. https://www.etymonline.com/word/mathematics https://www.etymonline.com/word/mathematics https://www.etymonline.com/word/foundation https://www.etymonline.com/word/foundation this begs the question - why do you need to build a building on top of something? why cant you just build the building on the ground. well its because of the Earth itself, it moves, its unstable, it has water in some places and not in others, sand in some places and not in others, and so forth. different climates and different needs. now this makes me wonder, if you were not born on Earth, but on some place where buildings did not need foundations, would you ever wonder what the foundations of mathematics were? and if you were on a planet where, say, music was considered the ultimate form of knowledge, rather than you know, high frequency trading algorithms or dark patterns to drive advertising engagement, would the connotation of math be entirely different and would the meaning of the word math have evolved differently?

dwheeler 3y ago

I would have expected to see at least more of a discussion about Metamath. Metamath by itself does not pick any particular foundation. It just lets you state axioms, then prove theorems from axioms and other proven theorems (letting you stack them up). So you can choose your axioms. Set theory with classical logic? Or with intuitionistic logic? Maybe you'd prefer simple type theory? Carry on! That said, the largest Metamath database (set of axioms and proven theorems) is the "Metamath Proof Explorer". It's based on ZFC set theory with classical logic. It turns out that ZFC set theory is quite enough to model structures. This database does add the Tarski–Grothendieck Axiom for certain uses of category theory (the same axiom added by Mizar), but it's only used when it's needed and that is quite rare. Heck, even the axiom of choice turns out to be unneeded in many cases. You certainly don't have to use ZFC with classical logic as your fundamental starting point (indeed, someone who rejected classical logic would not accept it). But you can go a long way with it. More information about Metamath is here: https://us.metamath.org/ https://us.metamath.org/ More information about the Metamath Proof Explorer database (based on ZFC + classical logic) is here: https://us.metamath.org/mpeuni/mmset.html https://us.metamath.org/mpeuni/mmset.html

pilgrim0 3y ago
The way you put it, I find it pretty fucking interesting. Thanks for the comment.
JonChesterfield 3y ago
Metamath is superb. Linear time proof checking is especially good. I haven't got past the distinct variable side conditions, though it's an interesting take on the variable free in term / capture avoiding substitution equivalent in lambda calculus.

galaxyLogic 3y ago

Doesn't it all come down to: What is the meaning of "is"? Mathematics is all about statements like "a is bigger than b". "3 is prime". Etc. But what is (sic!) the meaning of "is"?

vintermann 3y ago

> Calculus of inductive constructions (Coq, Lean): the original paper (describing a weaker system) begins “The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style,” and the paper makes no foundational claims. Coquand’s retrospective paper makes no such claims either. Since it turns out to be significantly stronger than ZF set theory, Whoa, whoa, hold your horses here. Why didn't THAT claim come with an explanatory hyperlink?