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.
> It seems like it should be possible, in theory, but it takes too much work.
The definition of a valid mathematical proof that I've heard mathematicians use is if it convinces other mathematicians. I think there's integrity in depth in mathematical proofs for lots of reasons, tying back to an axiomatic basis is a lot of extra work for likely no benefit.
On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.
> On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.
In the old days there were philosophers. They sought truth through thought and wisdom. Some started to measure reality and compare thought against that measurement, but real philosophers paid little heed for it didn't matter.
Testing their theory became known as physics. It turned out the testing against reality can be used without the theory, which we call engineering. We still have philosophers and they still pay little heed to measurement.
There is a similar disaster inbound for mathematicians. Formal mathematics is tedious and mostly only shows things that you were pretty sure were true anyway, so why bother.
It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.
this may be changing. as we speak. terence tao has recently been working to formalize existing work in lean. and has already found a bug in one of his published proofs. i think there will always ish be a need for mathematical proofs in the contemporary sense, but at this point i don't think its too implausible to suggest a future where the mathematical mainstream moves towards some hybrid mathematical exposition of computationally verified artefact.
The canonical paper on this was written by De Millo, et al., but it has a rather ungrammatical and incomprehensible title that does it no favors. However, the al. include Lipton and Perlis, so listen up...
Social Processes and Proofs of Theorems and Programs
I think the most exciting work in mathematics today is in the formal foundations. However, I can also understand mathematicians who are thinking like this:
1. I only need normal congruence
2. I only need perfect information games
Under problems that are solvable using these two assumptions, there is little benefit in tying proofs back to an axiomatic basis. Once you drop one of these two assumptions, proofs get much harder and a solid foundation gets more important.
> Now that part is pretty much solved, we are fairly confident that the foundations of mathematics are consistent.
Well, if you want them to be. I’m quite fascinated by the field of inconsistent mathematics, which attempts to show one can do real and useful mathematics given foundations which are at least tolerant of inconsistency (or even actually inconsistent)
Mathematicians have always been about equally certain that their foundations were consistent, but have gone from not knowing what they really were to expecting to eventually prove them consistent to knowing they can't be proven 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.
I suppose my followup to that is, why is this a problem? Does it lead to bad mathematics? (For what definition of “bad”?) Would we be able to solve unsolved problems if we tied things back to foundations more? Mathematicians have never really done much mathematics that ties back to the foundational axioms — why change? Rigor is not really much of an end in itself - surely people do mathematics because it is useful or beautiful, or both?
Much progress has been made in mathematics by demonstrating that problems in one realm are logically equivalent to solved problems in another realm, allowing proofs from the other realm to support proofs in the first. The most obvious example is the solution to Fermat's Last Theorem by Andrew Wiles, which wended far afield through the Taniyama–Shimura conjecture involving elliptic curves and modularity.
So in theory, with a solid foundation for mathematics, and new work rigorously tied back to it, this sort of thing should be both easier and more efficient.
If somebody makes a proposition and nobody is able to properly vet it, or if you just get a bunch of white heads to nod sagely and endorse it, very little prevents there existing a flaw that invalidates the whole thing which might go unnoticed for decades and ruin anything anyone tries to build atop of the result.
It's the same as security hardening in code, or checking for med interactions at the pharmacists. Or checking to make sure that the absolutely correct pill is being dispensed and not mixed up "Buttle/Tuttle" style with some other similar looking pill.
Formal rigor paved all the way from the proposition to the axioms is not 100%, nothing is 100%. But formal rigor paved over that entire distance redistributes all potential for error to the proof chain itself which is now far easier for a non-AI computer to verify, and to the strength of the axioms themselves which have had more scrutiny paid to them than any other statements in the history of mathematics.
Another important point is that you do not have to go all the way back to the axioms if someone else has already formally proved other complex statements you can rely upon instead, then you only have to pave the length of your driveway to the nearest communal road.
I think AI for mathematics will help us solve unsolved problems. There should be a virtuous cycle during its development.
1. More formalized training data makes the math AI better
2. Better math AI helps us formalize more known mathematics
But right now math AI is not very useful. It isn't at the point where ChatGPT is for programming, where the AI is really helpful for a lot of programming tasks even if it isn't superhuman yet. So the virtuous cycle hasn't started yet. But I think we will get there.
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.
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.
Are you saying that Löb's axiom, which states that the provability of "the provability of p implies p" implies the provability of p, necessarily prejudices some implicit assumption of consistency to the meta-language?
How so, and/or, what are the axioms, or derived properties, of this new notion of provability you have uncovered?
I've recently found out String Theory got so big partially because Calabi-Yau manifolds have some neat, mathematically tractable properties. (The one I somewhat understand is, being manifolds, they are locally smooth everywhere, which... doesn't seem like it should be a hard requirement for building blocks of reality.) Feels like that joke about looking for your lost keys under the streetlamp because there is light there, even though you lost the keys somewhere completely different.
> 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.
Your assertion about the inevitability is true only under specific axioms. If you are willing to drop the notion that infinity exists, or the law of excluded middle (and maybe others), the problems that arise from Gödel's incompleteness theorems don't necessarily apply.
I'm very far from mathematician circles so I don't know how they actually interpret Gödel, but the idea of being "fairly confident" that math foundations are consistent while knowing that either there are true statements that we can't prove, or that the foundations aren't consistent, feels like a pretty weird thing to me.
I always thought most mathematicians just looked at Gödel like he discovered an interesting novelty, then ignored him and went back to doing whatever math they were already doing, instead of losing sleep over what his theorem implied.
That there are statements which might be true but we don't know how to prove was always the reality in mathematics. That this is not a temporary reality but something we're doomed to was thus not a huge revelation. Definitely not something I would expect anyone to lose sleep over.
Also, is it true that constructive mathamtics actually escapes Godel's theorems? My understanding was that any system strong enough to contain regular arithmetic is subject to it. Either way, constructive math is more limited in what it accepts as proofs, so there will be more, not fewer statements that are true but unprovable with such a system.
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.
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.
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.
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:
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.
> Mathematics includes the natural numbers and plane and solid geometry.
That, to me, feels similar to Euclid’s fifth postulate, in the sense that it isn’t something you’d want to include in a definition.
Maybe, the similarity doesn’t end there, and we have multiple mathematics, just as pure mathematicians don’t talk about algebra, but about an algebra, with some of them being more interesting than others, and it not always being easy to show that two algebras are different from each other.
For example, we have mathematics without the law of the excluded middle and with it, ones without the axiom of choice and with it, etc.
> For example, we have mathematics without the law of the excluded middle and with it, ones without the axiom of choice and with it, etc.
This is a bit off-topic. Elsewhere in comments [1] people talk about Terence Tao and his recent work in Lean. Lean is based on intuitionistic logic, a base which doesn't include axiom of choice and the excluded middle.
Since Tao and other classical mathematicians need excluded middle for proofs by contradiction.
The Classical library in Lean starts by declaring axiom of choice [2] and after some lemmas introduces excluded middle as a theorem, called "em" for brevity [3]. I like how Lean makes this particular choice for classical mathematics very obvious.
A mathematician, like a painter or a poet, is a maker of patterns. If his patterns are more permanent than theirs, it is because they are made with ideas” (Hardy, 1992 , p. 84)
I lean towards patterns of ideas, relations, structures and organizations.
Correct me if I’m hallucinating, anybody. Doesn’t a foundation have to change and adapt in relation to what is grounded in it? If the foundation is to be all encompassing, to abstract enough to allow and absolutely account for every possible superstructure that it may ever ground, would not the foundation itself be contentless, inexpressive? “Silence contains all sound”, and “Every moment has an infinite amount of time” are constructs that came to my mind as isomorphic to the questioning. As mathematical structures gets finer and more intricate, purely on the basis of necessity (survival of the mathematician, mankind and mathematics itself) and experimentation, so their foundations must undergo at least some change? Even though such changes are purely virtual, and of interpretative nature? The same ideology, but “taken as” something else, thus, ultimately, subjective? There also seems to emerge an issue of ordering, of a demand for primality and derivation, which screams paradox. Could all of mathematics fit within itself, being itself employed to bootstrap its own, with no second system? A sort of ontological auto-genesis? Could our conception of paradox be itself primal, and perhaps, in some plane, could it be something ranking higher, of first-class? Also, I’ve been thinking, recently, on the role of time in structures. There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
In mathematics, the roof holds up the building, not the foundation. Since humans use mathematics a lot, we design foundations to our specific needs. It is not the building we are worried about, we just want better foundations to create better tools.
Not only are we going to treat mathematics as subjective, but also having formal theories that reason about different notions of subjectivity. https://crates.io/crates/joker_calculus
> Could our conception of paradox be itself primal, and perhaps, in some plane, could it be something ranking higher, of first-class?
> Also, I’ve been thinking, recently, on the role of time in structures. There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
Path semantical quality models this relation, where you have different "moments" in time which each are spaces for normal logical reasoning. Between these moments, there are ways to propagate quality, which is a partial equivalence. https://github.com/advancedresearch/path_semantics
Doesn’t a foundation have to change and adapt in relation to what is grounded in it?
No. An infinite number of possible papers about number theory could be written without having to change ZFC.
There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
ZFC stands as a counterexample.
Building on ZFC, we can build mathematical structures that represent the universe with time. Not the other way around.
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]
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.
If you want something as simple as possible, look at HOL and similar simple logics! CIC is powerful but it's also quite complex in comparison. Proof assistants based on HOL are plenty and they're definitely usable (see Isabelle/HOL, HOL light, etc.)
I did study HOL Light. Although it is very simple, I found parts of it to be a bit ugly. It treats the left of the turnstyle (|-) as a kind of set where you sometimes have to remove all alpha-equivalent terms. I.e., the DEDUCT_ANTISYM_RULE in https://en.wikipedia.org/wiki/HOL_Light. Another thing that I found ugly in HOL Light is that if one looks at the very basic code that is the kernel of the system all variables carry their type around with them. I think the lambda calculus where (\x: T, body) just has the type of x in the lambda and not in every instance of x inside body is just nicer.
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.
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.
Once you have an infinite hierarchy of types, including universe levels, can the proof assistant really be "as simple as possible"?
I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect.
That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.
Well, I tried to have only one universe level but I found that I could not do some rather simple constructions without proof irrelevance. And that generally proof irrelevance seems to make quite a few things quite a bit easier, also requiring fewer axioms. The thing with proof irrelevance is, though, that it more or less forces one to have universe levels. If there is only one universe level then Prop and Set have to share that. In fact, in that kind of simple setup Prop and Set are just the same thing and one can just use two words as a syntactic sugar but not as anything meaningful. However, proof irrelevance then implies that every set only has one element, which is no good. So, then we we have at least two universe levels. But impredicativity is only consistent in the lowest universe level so then one is more or less automatically led to an infinite tower of universes.
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
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
Equality works out cleanly if you distinguish between definitional equality and equivalence. Definitional sometimes gets called syntactic. As in the definitions are the same symbols in the same arrangement.
(lambda (x) (+ x x)) != (lambda (x) (* 2 x))
In particular, that's decidable on any finite expressions. Walk the expressions like an AST comparing the nodes on each side.
Equivalence / observational equality covers whether two expressions compute the same thing. As in find a counterexample to show they're not equivalent, or find a proof that both compute the same things, or that each can be losslessly translated into the other.
Requiring that your language can decide observational equivalence on the computation of any two terms seems obviously a non-starter to me, but it also looks like the same thing as requiring a programming language type system be decidable.
I want to reason hypothetically, which is why I don't use syntactic equality. I only use syntactic inequality in a very limited sense, e.g. two symbols `foo'` and `bar'` are symbolic distinct, so one can introduce `sd(foo', bar')`.
The reason is that if I have a proof `((x + x) == (2 * x))^true`, then I can treat objects as if they were definitionally equal.
When definitional equality and syntactic equality are the same, one is assuming `(!(sd(a, b)) == (a == b))^true`, which obtains a proof `!sd(a, a)` for all `a`. This destroys the property of reasoning hypothetically about exponential propositions in Path Semantics. For example, I might want to reason about what if I had `sd(a, a)`, does this imply `a ~~ a` by `q_lift : sd(a, b) & (a == b) -> (a ~~ b)`? Yes!
However, if I already have `!sd(a, a)` for all `a`, then the above reasoning would be the same absurd reasoning.
I can always assume this in order to reason about it, but I don't have to make this assumption a built-in axiom of my theory.
When assuming tautological congruence e.g. `(a == b)^true` in a context, one is not enforcing observational equality. So, it is not the same as requiring the type system to be decidable. I can also make up new notions of equivalences and guard them, e.g. not making them tautological congruent.
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”.
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.
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.
> 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?
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.
You're getting at the problem with saying "foundation". If you can reach the same conclusions from a large number of starting points, there isn't any special set of ideas on which everything rests.
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.
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.
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.
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.
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?
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.
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
(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.
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.
> 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.
> 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.
This sounds kind of similar to something I've thought about, but which makes approximately one fewer assumption, while also remaining closer to set theory.
Namely, the theory of first order logic (without equality), with one binary relation symbol, and no axioms (unless you count the laws of inference of FOL, which you shouldn't).
If you name this binary relation symbol \in_0 , and are willing to use a "definition schema" to define, for each natural number in your meta-theory, binary relations \in_n and =_n (any sentence using these \in_n and =_n can be expanded out to a longer sentence in FOL using just quantifiers and \in_0),
then, in the meta theory, you can prove a fair number of nice things about "for all natural numbers n, it is provable in the object theory that [some statement which uses relations \in_n and/or =_n]".
For example, you can show that, for all n, you can show in the object-theory that =_n is transitive and reflexive, and that if x =_n y, then x =_{n+1} y as well,
and that for all A, B, if A \subseteq_n B , then A \subseteq_{n+1} B,
and you can define notions of one object being a power set of another object at level n (and any two power sets of an object at level n, will be equal at level n), and can show that, for all n, it is provable in the object theory that if A \subseteq_n B , and if PA is a powerset of A at level n, and PB is a powerset of B at level n, then PA \subseteq_n PB , and all sorts of similar things.
I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim, but I haven't looked closely.
Are you familiar with the metamath project? aiui, metamath is based in string rewrite rules, and is therefore fully general in the way it sounds like you are going for?
> I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim
And rightfully so. I've discovered Abstraction Logic (AL) over the course of the last two years, and in the beginning I didn't know exactly what I had there. In later papers on abstractionlogic.com I understand AL better, the latest being "Logic is Algebra". I would not say anymore that AL is in between first-order and second-order logic. Instead I would say that AL combines the benefits of first-order logic (one undivided mathematical universe U) with the benefits of higher-order logic (general binders). And there certainly is a second-order aspect to it, because an operator is a function that takes operations as arguments, and returns a value in the mathematical universe U; here an operation is a function that takes values in U as arguments, and also returns a value in U.
> Are you familiar with the metamath project
Yes, I know it. I would say the main difference is that metamath doesn't really have a proper semantics. It has some rules to manipulate syntax, but they don't mean anything on their own. Only by making the rules of metamath simulate the deduction rules of logics like first-order logic, meaning enters the picture, by inheriting meaning from the simulated logic. On the other hand, Abstraction Logic has a proper and simple semantics of its own.
> unless you count the laws of inference of FOL, which you shouldn't
So the laws for your quantifiers are not counted, I guess, but given as a built-in feature of FOL? In AL, quantifiers are just ordinary operators, and can be introduced via axioms (or not be introduced at all, if you prefer that for some reason).
If mathematics were the study of real objects, why didn't Platonists realize set theory was ill-founded a long time before Russell did? After all, Plato predates Russell by a few years.
The same reason it took so long to develop theories of gravity: nobody smart enough spent the time applying the tools needed to come to with it. The tools in this case being logic as the OP described.
> 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.
> 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.
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.
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.
> It seems like it should be possible, in theory, but it takes too much work.
The definition of a valid mathematical proof that I've heard mathematicians use is if it convinces other mathematicians. I think there's integrity in depth in mathematical proofs for lots of reasons, tying back to an axiomatic basis is a lot of extra work for likely no benefit.
On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.
> On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.
In the old days there were philosophers. They sought truth through thought and wisdom. Some started to measure reality and compare thought against that measurement, but real philosophers paid little heed for it didn't matter.
Testing their theory became known as physics. It turned out the testing against reality can be used without the theory, which we call engineering. We still have philosophers and they still pay little heed to measurement.
There is a similar disaster inbound for mathematicians. Formal mathematics is tedious and mostly only shows things that you were pretty sure were true anyway, so why bother.
It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.
1 reply →
this may be changing. as we speak. terence tao has recently been working to formalize existing work in lean. and has already found a bug in one of his published proofs. i think there will always ish be a need for mathematical proofs in the contemporary sense, but at this point i don't think its too implausible to suggest a future where the mathematical mainstream moves towards some hybrid mathematical exposition of computationally verified artefact.
https://mathstodon.xyz/@tao/111287749336059662
4 replies →
The canonical paper on this was written by De Millo, et al., but it has a rather ungrammatical and incomprehensible title that does it no favors. However, the al. include Lipton and Perlis, so listen up...
Social Processes and Proofs of Theorems and Programs
https://dl.acm.org/doi/pdf/10.1145/359104.359106 [pdf]
I think the most exciting work in mathematics today is in the formal foundations. However, I can also understand mathematicians who are thinking like this:
1. I only need normal congruence
2. I only need perfect information games
Under problems that are solvable using these two assumptions, there is little benefit in tying proofs back to an axiomatic basis. Once you drop one of these two assumptions, proofs get much harder and a solid foundation gets more important.
> Now that part is pretty much solved, we are fairly confident that the foundations of mathematics are consistent.
Well, if you want them to be. I’m quite fascinated by the field of inconsistent mathematics, which attempts to show one can do real and useful mathematics given foundations which are at least tolerant of inconsistency (or even actually inconsistent)
https://plato.stanford.edu/entries/mathematics-inconsistent/
https://ir.canterbury.ac.nz/server/api/core/bitstreams/d6722...
Mathematicians have always been about equally certain that their foundations were consistent, but have gone from not knowing what they really were to expecting to eventually prove them consistent to knowing they can't be proven 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.
I suppose my followup to that is, why is this a problem? Does it lead to bad mathematics? (For what definition of “bad”?) Would we be able to solve unsolved problems if we tied things back to foundations more? Mathematicians have never really done much mathematics that ties back to the foundational axioms — why change? Rigor is not really much of an end in itself - surely people do mathematics because it is useful or beautiful, or both?
Much progress has been made in mathematics by demonstrating that problems in one realm are logically equivalent to solved problems in another realm, allowing proofs from the other realm to support proofs in the first. The most obvious example is the solution to Fermat's Last Theorem by Andrew Wiles, which wended far afield through the Taniyama–Shimura conjecture involving elliptic curves and modularity.
So in theory, with a solid foundation for mathematics, and new work rigorously tied back to it, this sort of thing should be both easier and more efficient.
The real benefit is certainty.
If somebody makes a proposition and nobody is able to properly vet it, or if you just get a bunch of white heads to nod sagely and endorse it, very little prevents there existing a flaw that invalidates the whole thing which might go unnoticed for decades and ruin anything anyone tries to build atop of the result.
It's the same as security hardening in code, or checking for med interactions at the pharmacists. Or checking to make sure that the absolutely correct pill is being dispensed and not mixed up "Buttle/Tuttle" style with some other similar looking pill.
Formal rigor paved all the way from the proposition to the axioms is not 100%, nothing is 100%. But formal rigor paved over that entire distance redistributes all potential for error to the proof chain itself which is now far easier for a non-AI computer to verify, and to the strength of the axioms themselves which have had more scrutiny paid to them than any other statements in the history of mathematics.
Another important point is that you do not have to go all the way back to the axioms if someone else has already formally proved other complex statements you can rely upon instead, then you only have to pave the length of your driveway to the nearest communal road.
And you can apply it, when you do, it really works.
I think AI for mathematics will help us solve unsolved problems. There should be a virtuous cycle during its development.
1. More formalized training data makes the math AI better
2. Better math AI helps us formalize more known mathematics
But right now math AI is not very useful. It isn't at the point where ChatGPT is for programming, where the AI is really helpful for a lot of programming tasks even if it isn't superhuman yet. So the virtuous cycle hasn't started yet. But I think we will get there.
> It seems like it should be possible, in theory, but it takes too much work.
Biologists don't model behaviors based on the four fundamental forces of physics.
It seems like it should be possible, in theory, but it takes too much work.
they don't, but they use chemistry
i guess that a point can be made that, even though chemistry is just applied quantum electrodynamics, people seldom derive it from first principles
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.
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.
6 replies →
I'm attempting to understand you, so:
Are you saying that Löb's axiom, which states that the provability of "the provability of p implies p" implies the provability of p, necessarily prejudices some implicit assumption of consistency to the meta-language?
How so, and/or, what are the axioms, or derived properties, of this new notion of provability you have uncovered?
4 replies →
> Recently I found another notion of "provability"
Any pointers to that alternative notion?
1 reply →
I've recently found out String Theory got so big partially because Calabi-Yau manifolds have some neat, mathematically tractable properties. (The one I somewhat understand is, being manifolds, they are locally smooth everywhere, which... doesn't seem like it should be a hard requirement for building blocks of reality.) Feels like that joke about looking for your lost keys under the streetlamp because there is light there, even though you lost the keys somewhere completely different.
> 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.
Your assertion about the inevitability is true only under specific axioms. If you are willing to drop the notion that infinity exists, or the law of excluded middle (and maybe others), the problems that arise from Gödel's incompleteness theorems don't necessarily apply.
I'm very far from mathematician circles so I don't know how they actually interpret Gödel, but the idea of being "fairly confident" that math foundations are consistent while knowing that either there are true statements that we can't prove, or that the foundations aren't consistent, feels like a pretty weird thing to me.
I always thought most mathematicians just looked at Gödel like he discovered an interesting novelty, then ignored him and went back to doing whatever math they were already doing, instead of losing sleep over what his theorem implied.
That there are statements which might be true but we don't know how to prove was always the reality in mathematics. That this is not a temporary reality but something we're doomed to was thus not a huge revelation. Definitely not something I would expect anyone to lose sleep over.
Also, is it true that constructive mathamtics actually escapes Godel's theorems? My understanding was that any system strong enough to contain regular arithmetic is subject to it. Either way, constructive math is more limited in what it accepts as proofs, so there will be more, not fewer statements that are true but unprovable with such a system.
1 reply →
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/
More information about the Metamath Proof Explorer database (based on ZFC + classical logic) is here: https://us.metamath.org/mpeuni/mmset.html
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.
The way you put it, I find it pretty fucking interesting. Thanks for the comment.
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
Thank you friend
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: 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.
> Mathematics includes the natural numbers and plane and solid geometry.
That, to me, feels similar to Euclid’s fifth postulate, in the sense that it isn’t something you’d want to include in a definition.
Maybe, the similarity doesn’t end there, and we have multiple mathematics, just as pure mathematicians don’t talk about algebra, but about an algebra, with some of them being more interesting than others, and it not always being easy to show that two algebras are different from each other.
For example, we have mathematics without the law of the excluded middle and with it, ones without the axiom of choice and with it, etc.
> For example, we have mathematics without the law of the excluded middle and with it, ones without the axiom of choice and with it, etc.
This is a bit off-topic. Elsewhere in comments [1] people talk about Terence Tao and his recent work in Lean. Lean is based on intuitionistic logic, a base which doesn't include axiom of choice and the excluded middle.
Since Tao and other classical mathematicians need excluded middle for proofs by contradiction.
The Classical library in Lean starts by declaring axiom of choice [2] and after some lemmas introduces excluded middle as a theorem, called "em" for brevity [3]. I like how Lean makes this particular choice for classical mathematics very obvious.
[1] https://github.com/leanprover-community/lean/blob/cce7990ea8...
A mathematician, like a painter or a poet, is a maker of patterns. If his patterns are more permanent than theirs, it is because they are made with ideas” (Hardy, 1992 , p. 84)
I lean towards patterns of ideas, relations, structures and organizations.
edit: from https://maa.org/press/periodicals/convergence/mathematics-as...
Correct me if I’m hallucinating, anybody. Doesn’t a foundation have to change and adapt in relation to what is grounded in it? If the foundation is to be all encompassing, to abstract enough to allow and absolutely account for every possible superstructure that it may ever ground, would not the foundation itself be contentless, inexpressive? “Silence contains all sound”, and “Every moment has an infinite amount of time” are constructs that came to my mind as isomorphic to the questioning. As mathematical structures gets finer and more intricate, purely on the basis of necessity (survival of the mathematician, mankind and mathematics itself) and experimentation, so their foundations must undergo at least some change? Even though such changes are purely virtual, and of interpretative nature? The same ideology, but “taken as” something else, thus, ultimately, subjective? There also seems to emerge an issue of ordering, of a demand for primality and derivation, which screams paradox. Could all of mathematics fit within itself, being itself employed to bootstrap its own, with no second system? A sort of ontological auto-genesis? Could our conception of paradox be itself primal, and perhaps, in some plane, could it be something ranking higher, of first-class? Also, I’ve been thinking, recently, on the role of time in structures. There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
In mathematics, the roof holds up the building, not the foundation. Since humans use mathematics a lot, we design foundations to our specific needs. It is not the building we are worried about, we just want better foundations to create better tools.
Not only are we going to treat mathematics as subjective, but also having formal theories that reason about different notions of subjectivity. https://crates.io/crates/joker_calculus
> Could our conception of paradox be itself primal, and perhaps, in some plane, could it be something ranking higher, of first-class?
Yes! Paradoxes are statements of the form `false^a` in exponential propositions. https://crates.io/crates/hooo
> Also, I’ve been thinking, recently, on the role of time in structures. There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
Path semantical quality models this relation, where you have different "moments" in time which each are spaces for normal logical reasoning. Between these moments, there are ways to propagate quality, which is a partial equivalence. https://github.com/advancedresearch/path_semantics
Doesn’t a foundation have to change and adapt in relation to what is grounded in it?
No. An infinite number of possible papers about number theory could be written without having to change ZFC.
There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
ZFC stands as a counterexample.
Building on ZFC, we can build mathematical structures that represent the universe with time. Not the other way around.
Is mathematics just the study of all possible languages that are constructed from strict internally consistent rules?
Mathematics is the study of things you can convince people are true without physical evidence.
5 replies →
No, because some possible languages are far more interesting than others.
7 replies →
So Japanese grammar is math?
3 replies →
Mathematics is the study of structure.
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%20w...
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."
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.
If you want something as simple as possible, look at HOL and similar simple logics! CIC is powerful but it's also quite complex in comparison. Proof assistants based on HOL are plenty and they're definitely usable (see Isabelle/HOL, HOL light, etc.)
I did study HOL Light. Although it is very simple, I found parts of it to be a bit ugly. It treats the left of the turnstyle (|-) as a kind of set where you sometimes have to remove all alpha-equivalent terms. I.e., the DEDUCT_ANTISYM_RULE in https://en.wikipedia.org/wiki/HOL_Light. Another thing that I found ugly in HOL Light is that if one looks at the very basic code that is the kernel of the system all variables carry their type around with them. I think the lambda calculus where (\x: T, body) just has the type of x in the lambda and not in every instance of x inside body is just nicer.
1 reply →
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.
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.
Once you have an infinite hierarchy of types, including universe levels, can the proof assistant really be "as simple as possible"?
I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect.
That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.
Well, I tried to have only one universe level but I found that I could not do some rather simple constructions without proof irrelevance. And that generally proof irrelevance seems to make quite a few things quite a bit easier, also requiring fewer axioms. The thing with proof irrelevance is, though, that it more or less forces one to have universe levels. If there is only one universe level then Prop and Set have to share that. In fact, in that kind of simple setup Prop and Set are just the same thing and one can just use two words as a syntactic sugar but not as anything meaningful. However, proof irrelevance then implies that every set only has one element, which is no good. So, then we we have at least two universe levels. But impredicativity is only consistent in the lowest universe level so then one is more or less automatically led to an infinite tower of universes.
What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
5 replies →
Is your goal to have as few axioms as possible, or as few syntactic constructions as possible?
Both really. Just as few givens as possible whether they are baked in or added on as axioms.
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
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
Equality works out cleanly if you distinguish between definitional equality and equivalence. Definitional sometimes gets called syntactic. As in the definitions are the same symbols in the same arrangement.
In particular, that's decidable on any finite expressions. Walk the expressions like an AST comparing the nodes on each side.
Equivalence / observational equality covers whether two expressions compute the same thing. As in find a counterexample to show they're not equivalent, or find a proof that both compute the same things, or that each can be losslessly translated into the other.
Requiring that your language can decide observational equivalence on the computation of any two terms seems obviously a non-starter to me, but it also looks like the same thing as requiring a programming language type system be decidable.
I want to reason hypothetically, which is why I don't use syntactic equality. I only use syntactic inequality in a very limited sense, e.g. two symbols `foo'` and `bar'` are symbolic distinct, so one can introduce `sd(foo', bar')`.
The reason is that if I have a proof `((x + x) == (2 * x))^true`, then I can treat objects as if they were definitionally equal.
When definitional equality and syntactic equality are the same, one is assuming `(!(sd(a, b)) == (a == b))^true`, which obtains a proof `!sd(a, a)` for all `a`. This destroys the property of reasoning hypothetically about exponential propositions in Path Semantics. For example, I might want to reason about what if I had `sd(a, a)`, does this imply `a ~~ a` by `q_lift : sd(a, b) & (a == b) -> (a ~~ b)`? Yes!
However, if I already have `!sd(a, a)` for all `a`, then the above reasoning would be the same absurd reasoning.
I can always assume this in order to reason about it, but I don't have to make this assumption a built-in axiom of my theory.
When assuming tautological congruence e.g. `(a == b)^true` in a context, one is not enforcing observational equality. So, it is not the same as requiring the type system to be decidable. I can also make up new notions of equivalences and guard them, e.g. not making them tautological congruent.
2 replies →
Yes. Although my take on this is that it's about VM design, or the ISA for a VM upon which mathematics runs.
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”.
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.
“A pretty good one.” Right. The amount of generalization and insight is incomparable.
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.
And yet, there are times to use the other theories:
Eg, type theory has more succinct proofs of unique inverses.
> 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?
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.
You're getting at the problem with saying "foundation". If you can reach the same conclusions from a large number of starting points, there isn't any special set of ideas on which everything rests.
Why does the foundation need to be unique? It seems intuitive to me that they must not be unique.
Is it also possible to define set theory in terms of arithmetic?
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.
1 reply →
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.
2 replies →
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.
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...
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/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?
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.
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
I'm a bit sad the he doesn't mention univalent foundations, which is based on ∞-groupoids instead of sets.
(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.
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.
> The objects in category theory are equipped with structure
I am sure everything else in the article is correct.
The sentence parses here - the objects have associated introduction and elimination rules which get called 'structure' - what error do you see?
In the abstract setting, morphisms do not "preserve structure" - they are just arrows, and there is no structure to preserve to begin with.
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"?
> 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, page 12, theorem 7
[1] http://abstractionlogic.com
> 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.
This sounds kind of similar to something I've thought about, but which makes approximately one fewer assumption, while also remaining closer to set theory.
Namely, the theory of first order logic (without equality), with one binary relation symbol, and no axioms (unless you count the laws of inference of FOL, which you shouldn't).
If you name this binary relation symbol \in_0 , and are willing to use a "definition schema" to define, for each natural number in your meta-theory, binary relations \in_n and =_n (any sentence using these \in_n and =_n can be expanded out to a longer sentence in FOL using just quantifiers and \in_0), then, in the meta theory, you can prove a fair number of nice things about "for all natural numbers n, it is provable in the object theory that [some statement which uses relations \in_n and/or =_n]".
For example, you can show that, for all n, you can show in the object-theory that =_n is transitive and reflexive, and that if x =_n y, then x =_{n+1} y as well, and that for all A, B, if A \subseteq_n B , then A \subseteq_{n+1} B, and you can define notions of one object being a power set of another object at level n (and any two power sets of an object at level n, will be equal at level n), and can show that, for all n, it is provable in the object theory that if A \subseteq_n B , and if PA is a powerset of A at level n, and PB is a powerset of B at level n, then PA \subseteq_n PB , and all sorts of similar things.
I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim, but I haven't looked closely.
Are you familiar with the metamath project? aiui, metamath is based in string rewrite rules, and is therefore fully general in the way it sounds like you are going for?
> I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim
And rightfully so. I've discovered Abstraction Logic (AL) over the course of the last two years, and in the beginning I didn't know exactly what I had there. In later papers on abstractionlogic.com I understand AL better, the latest being "Logic is Algebra". I would not say anymore that AL is in between first-order and second-order logic. Instead I would say that AL combines the benefits of first-order logic (one undivided mathematical universe U) with the benefits of higher-order logic (general binders). And there certainly is a second-order aspect to it, because an operator is a function that takes operations as arguments, and returns a value in the mathematical universe U; here an operation is a function that takes values in U as arguments, and also returns a value in U.
> Are you familiar with the metamath project
Yes, I know it. I would say the main difference is that metamath doesn't really have a proper semantics. It has some rules to manipulate syntax, but they don't mean anything on their own. Only by making the rules of metamath simulate the deduction rules of logics like first-order logic, meaning enters the picture, by inheriting meaning from the simulated logic. On the other hand, Abstraction Logic has a proper and simple semantics of its own.
> unless you count the laws of inference of FOL, which you shouldn't
So the laws for your quantifiers are not counted, I guess, but given as a built-in feature of FOL? In AL, quantifiers are just ordinary operators, and can be introduced via axioms (or not be introduced at all, if you prefer that for some reason).
If mathematics were the study of real objects, why didn't Platonists realize set theory was ill-founded a long time before Russell did? After all, Plato predates Russell by a few years.
The same reason it took so long to develop theories of gravity: nobody smart enough spent the time applying the tools needed to come to with it. The tools in this case being logic as the OP described.
9 replies →
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
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
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 :
> "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities" (2018)
https://scholar.google.com/scholar?cites=9763697449338277760... and sorted by date: 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...
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.
From > [...] is it ever shown that Quantum Logic is indeed the correct and sufficient logic for propositional calculus and also for all physical systems?
( Quantum statistical mechanics: https://en.wikipedia.org/wiki/Quantum_logic#Relationship_to_...