You could also be thinking of Zermelo-Fraenknel set theory (ZF/ZFC), which most of modern mathematics is ultimately based upon.
I have young kids, and in exploring why boats float I suggested the four elements model. They tested it with bottles full of air and water and earth and it all kind of held up until they found a bowl that floats. Making a wrong model helped the learning process more than telling them the right model. I loved every minute of the science.
I don't know if there's a way to remove axioms, nor do I think you can change the logical foundations (which are based in type theory).
That game is called math :) Partially joking, but I do think a game version would be fun.
> Is this what pure math is about?
More or less yes for an undergrad, but when you get to research it feels different.
> I badly, direly want this
Consider checking out an abstract algebra book. Maybe Dummit and Foote or something else popular. Proofs in algebra often have a satisfying game-like quality. The more popular books will have solutions you can find online if you get stuck.
Would you mind telling more about how it feels different in research?
In research you're doing a lot more of things like reading papers, putting your thoughts into words, trying to understand something the author of the paper barely understands, feeling lost and unsure where to look next. All of that can feel good too (or it cannot depending on the person) but it's a different feeling than playing a logic game.
As one example, Euclidia is a fun meditative game. But compare the difference in feeling between doing an exercise from Euclid and trying to prove the parallel postulate. It took centuries to realize you couldn't prove it, and then there was a lot of hard work trying to figure out what geometry was like if you get rid of it.
Millennia, even
Interesting. I find them banal and deeply unsatisfying.
So then you could self-apply it and start ... deriving new rules of how you can derive new theorems and thus also new rules, from axioms?
I'm jusr confused a bit about "axioms" and "rules". What's the difference?
They're usually considered separate, because they're orthogonal to the foundational axioms you're using to build up your mathematical systems. With the exact same system of axioms, you might be able to prove or disprove certain things using some logic systems, but not others.
The article mentions it, in fact: https://adam.math.hhu.de/#/g/leanprover-community/nng4
1) It uses the term "goal" for the the current stage of the proof you're working on, which is counterintuitive. In common speech, the goal is the theorem you're trying to prove, not the current step you're on in proving it. It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
2) It doesn't warn you early on about the left-associativeness of the operator binding, or what to do about it. So you can apply what seem like valid transformations but then parentheses pop up that you don't expect, and which you have no guidance on how to deal with. I had to ask ChatGPT what was going on to solve it.
Interesting. Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work? And if we then do brush our teeth, wouldn't you say that the remaining goal is to get to work? In this scenario, if anything can be called progress, it is what's in the past (the showering etc.), not what is still to be done.
Yes, I agree! My issue is not with the reality of having reduced the problem to a different one, but with the "goal" metaphor, which is counterintuitive to how that term is normally used, especially since it connotes that each step is some brand new thing, rather than progress.
And sure, like any technical jargon, you can learn to accept some specialized term-of-art usage, but I'd prefer it be conducive to developing a correct ontology of what is going on in an assisted Lean proof.
While "subgoal" is better, I think the issue even goes back to calling the original theorem a "goal". Really, the goal is to prove the theorem. So a better term, more conducive to intuiting the Lean ontology, would be something like "[remaining] unresolved proof state", even though it's more verbose. (Perhaps you could get the best of both worlds with some kind of footnote for new users that clarifies that this is what "goal" means here.)
With that said, I appreciate the pushback, as your comment forced me to more carefully think about what I was objecting to.
I do want to note that systems usually use terms like "current goal" or "active goal", which do imply a sense of progress. I never felt that they imply that the current goal is a brand-new thing. It's a transformed version of the previous goal, hopefully made up of simpler parts that eventually become so simple as to be trivial, which then completes the overall proof.
From your questions I marked you as a high schooler.
I would say, "from a handful of axioms".
It's certainly true that when Euclid started this whole enterprise, it was thought thax axioms should be self-evident. But then, many centuries later, people discovered that there are other interesting geometries that don't satisfy the same axioms.
And when you get to reasoning about infinities, it's very unclear that anything about them can be considered self-evident (a few mathematicians even refuse to work with infinities, although it's definitely a very niche subcommunity).
Some of today's common axioms are indeed self-evident (such as "you should be able to substitute equal subterms"), but things like the axiom of choice have (at least historically) been much more controversial. I would probably say that such axioms can be considered "plausible" and that they generally allow us to be able to prove what we want to prove. But you'll definitely find mathematicians championing different axioms.
> Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.
That would be the ZFC axioms. It was originally the ZF axioms (named so after the mathematicians Zermelo and Fraenkel who worked in the early 20th century), and then later the Axiom of Choice (C) was added. It's generally considered to be the "standard" set of axioms for maths, although very few mathematicians actually work directly from these axioms. But in theory, you can take almost every mathematical proof (unless it's explicitly set in some other foundation) and recast it entirely in applications of the ZFC axioms.
Are there essentially two flavours:
- the maths based on axioms that are fundamentally, cosmically true such as x = x. And in doing so we’re formalizing on paper the universal truths and all subsequent rules we know to be true given these
- the maths that incorporate those plus additional axioms that aren’t necessarily fundamentally true (or maybe just not provable), but work very well at laying a foundation for further rules that build a practically useful, but not necessarily “correct” toolbox
With the latter, is it kind of a “they won’t hold up under normal conditions but if you accept these axioms, there’s interesting things you can explore and achieve?”
The only thing that matters is what you choose to take as granted for a particular question.
It's like how you can draw a map of a place that doesn't exist.
Or like coming up with rules for a game and then trying it to see how it plays.
Or it's like a material used for construction. You can build a house out of it, but there's no inherent "houseness" to it, despite how common such a use is.
Even given that separation (which itself is fuzzy), even the first group can't be construed as "universally true". For example there's a range of opinion around the law of the excluded middle (whether "P is not false" implies "P is true"). Most other propositional logic axioms like modus ponens are less controversial though.
As far as real world math, while ZF set theory axioms are generally viewed as the "foundation", that's due to convention more than any real primacy of ZF. Other set theories and types of "foundations" exist that seem to be just as suitable to be called a "foundation", and most math is "foundation" agnostic. Like, if all you're doing is something with prime numbers, then it doesn't matter what "foundation" you use; so long as it lets you define prime numbers, that's all that matters.
"Foundations" only come into play when you're doing really subtle things with different orders of infinities. And then, yes, the answer can be different depending on what foundation you choose. And that's fine. It doesn't mean that either foundation is wrong. They're just different. Which is why "foundation of mathematics" is a bit of a misnomer / fool's errand. Different foundations have different results on certain edge cases, and those are interesting to investigate, not something to be upset about. And like I said, most "ordinary" math is pretty foundation agnostic.
Take a look at zeroth-order logic.
Can someone please turn this into a Zachtronics style game?! I badly, direly want this. There’s a game called Euclidea that’s kind of like this for trigonometry and the whole premise of building a tower of logic is deeply attractive to me.
Is this what pure math is about? Is this what people who become math profs are feeling in their soul? The sheer thrill of adding to that dictionary of proofs?
Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.