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.
> 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.
Formalized mathematics is just a very small subset of what mathematicians work on: in my observation people who work on (computer) formalized proofs often rather sit in CS departments.
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.
I think it's likely that axiomatic approaches, and formal approaches will continue to produce interesting results and have some effect on regular mathematics.
But this is very different to suggesting that most regular mathematics will switch to using formal proofs. There's a big ergonomics gap at the moment.
An analogy could be to look how pure mathematicians look down on applied mathematicians' work, the applied mathematicians don't care, they just get on with their own standards. You need regular mathematicians to choose to switch over en masse, what will compel them to do that?
…success by Tao and Scholze in formalizing their work and gaining appreciable benefits such as correcting technical errors.
Which is happening right now — and the younger mathematicians who are supporting those efforts (and more broadly, things like Lean libraries) are gaining the experience while making the ergonomic changes.
That is, the person you’re replying to isn’t unaware of the historic problems: they’re pointing out that migration is starting now with early adopters like Tao and Scholze.
I think a little hesitance on the overall success of these sorts of projects is prudent, given the history of axiomatic and formal expections and reality.
But let's say they make huge amounts of progress - they might improve the ergonomics enough that the formal foundations of mathematics will be brought into mathematics departments as a standard, legitimate and popular subject. But I still can't see how this would affect most mathematics.
> But I still can't see how this would affect most mathematics.
It won't, in the same way that introducing physics didn't affect philosophers. They were still free to do philosophy. But most new innovation and innovators came up doing physics instead - and that's been where all the growth had been for centuries.
In the end ungrounded theory is better than nothing. But grounded theory beats out ungrounded theory hands down.
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.
> I guess you just meant "the notion of provability is the same as the one that would later be described in Provability logic" ?
yes
> I viewed the page you linked, but I don't see anywhere where you describe the alternate notion of "provability" you have in mind.
See section "HOOO EP"
>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?)
This would be `|- p` implies `□p`, which is the N axiom in modal logic (used by Provability Logic).
In Provability Logic, you can't prove `□false => false`. If you can prove this, then Löb's axiom implies `false`, hence absurd. `□p => p` for all `p` is the T axiom in modal logic. In IPL, if have `true |- false`, then naturally you can prove `false`. So, you can only prove `□false => false` if you already have an inconsistent theory.
Provability Logic is biased toward languages that assume that the theory is consistent. However, if you want to treat provability from a perspective of any possible theory, then favoring consistency at meta-level is subjective.
> 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?
I have given this some thought before and I think it is based on fix-point results of predicates of one argument in Provability Logic. For example, in Gödel's proof, he needs to encode a predicate without arguments in order to create the Gödel sentence. In a language without such fix-points, this might not be a problem.
> 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.
The name "qubit" comes from the classical model, where you generate a random truth table using the input bit vector as seed. So, the proposition is in super-position of all propositions and hence behaves like a "qubit" in a classical approximation of a quantum circuit.
Something being random and/or undetermined is not sufficient for it to be like a qubit. You need the linear algebra aspect for the name to be appropriate, IMO.
> See section "HOOO EP"
I have looked through that section, and afaict, nowhere in it do you define an alternative notion of “provability”?
> In Provability Logic, you can't prove `□false => false`. If you can prove this, then Löb's axiom implies `false`, hence absurd.
Why do you expect to be able to prove `□false => false` ? I.e. why do you expect to be able to prove `not □false`, i.e. prove the consistency of the system you are working in.
> Provability Logic is biased toward languages that assume that the theory is consistent. However, if you want to treat provability from a perspective of any possible theory, then favoring consistency at meta-level is subjective.
I’m not really sure what you mean by “favoring [...] is subjective.” .
Also, if you want to do reasoning from within an inconsistent theory, then I’d hope it is at least paraconsistent, as otherwise you aren’t going to get much of value? Or at least, nothing with any guarantee. If you aren’t aiming at a paraconsistent logic, I don’t follow your point about not wanting to favor the assumption that the system is consistent.
> Something being random and/or undetermined is not sufficient for it to be like a qubit. You need the linear algebra aspect for the name to be appropriate, IMO.
Naming things is hard. Given how constrained Propositional Language is as a language, I do not think there is much risk of misinterpreting it. I needed something to associate with "superposition" but also fit with "quality". Both "qubit" and "quality" starts with "qu", so I liked the name.
It does not bother me if people find another better name for it.
> I have looked through that section, and afaict, nowhere in it do you define an alternative notion of “provability”?
I do not want to create a controversy around Provability Logic by making too strong claims for some people's taste. What I meant is that this section is explaining HOOO EP and my interest is in communicating what it is on its own sake, without needing to compare it to Provability Logic all the time. However, since HOOO EP is so similar to Provability Logic, it requires some clarification. I hope you found the section useful even though you were not able to see how it is an alternative notion of provability from its definition.
> Why do you expect to be able to prove `□false => false` ? I.e. why do you expect to be able to prove `not □false`, i.e. prove the consistency of the system you are working in.
I think this is trying to think about logic as a peculiar way. HOOO EP was not developed to reason about consistency. It has its own motivation that makes sense. However, once you have HOOO EP, you can start discussing how it relates to consistency of theories.
It makes sense, in a sense of consistency, from the perspective where an inconsistent theory is absurd. Absurd theories can prove anything, so there is no distinction between true and false statements. Now, if you interpret `□false` as an assumption that one can prove false, then of course, one can prove false. `□false => false` is the same as `!□false`. Does this mean that it proves its own consistency? No, because you made the assumption `□false`. You have only talked about what you can prove in the context of `□false`. From this perspective, `□false => false` is trivially true.
Provability Logic does not allow you to think of `□false` as meaning "I can prove `false`". Instead, it is interpreted as "this theory is inconsistent" but without assigning this statement a particular meaning. This means, there is a gap between "I can prove `false`" and "this theory is inconsistent". Now, if you ignore the gap, then you are just making an error of interpretation. You have to respect the formal sense, where Provability Logic can have two different notions of absurdity while naturally you would think of them as one. However, if you want to have one instead of two, then you need HOOO EP.
> Also, if you want to do reasoning from within an inconsistent theory, then I’d hope it is at least paraconsistent, as otherwise you aren’t going to get much of value?
It sounds like you are assuming HOOO EP is inconsistent? Why are you speculating about my motivations in a such context?
> Provability Logic does not allow you to think of `□false` as meaning "I can prove `false`". Instead, it is interpreted as "this theory is inconsistent" but without assigning this statement a particular meaning.
“It is provable in system X that False” and “system X is inconsistent” are the same statement. That’s what it means for a system to be inconsistent: there is a proof in the system of the statement False.
So, no, you’re wrong: in probability logic, []False can be interpreted as “it is provable (in this system) that False”.
> It sounds like you are assuming HOOO EP is inconsistent?
While I do suspect it to be, that isn’t why I said that. I was saying that because you were seemingly saying that probability logic has a bias favoring reasoning from within a consistent system. And, I was saying, “why would you want to be reasoning within an inconsistent system? Shouldn’t something be suited for reasoning within a consistent system, seeing as reasoning in an inconsistent system gives you nonsense?”
> I hope you found the section useful even though you were not able to see how it is an alternative notion of provability from its definition.
It didn’t provide me with the answer I was seeking, and so I will instead ask you directly again: what alternative notion of probability do you have in mind?
Logic by default does not have a bias toward consistency. The bias is added by people who design and use mathematical languages using logic. It does not mean that the theory you are using is inconsistent.
Asking "why do you want to be reasoning within an inconsistent system?" is like facing a dead end, because you are supposing a bias that was never there in the first place. As if, logic cares about what you want. You only get out what you put in. Bias in => bias out.
I am speculating about the following: If we don't bias ourselves in favor of consistency at the meta-level, then the correct notion of provability is HOOO EP. If we are biased, then the correct notion is Provability Logic.
In order to see HOOO EP as a provability notion, you have to interpret the axioms as a theory about provability. This requires mathematical intuition, for example, that you are able to distinguish a formal theory from its interpretation. Now, I can only suggest a formal theory, but the interpretation is up to users of that theory.
> In order to see HOOO EP as a provability notion, you have to interpret the axioms as a theory about provability.
A notion can generally be prior to a particular formalization. If you have an alternative notion of probability in mind, you should be able to express it.
> Now, I can only suggest a formal theory, but the interpretation is up to users of that theory.
Ok, well, it has no users other than yourself, so if you want to communicate how it could be useful, I recommend you find a way of expressing/communicating an interpretation of it.
—-
Also, I think your idea of a “bias towards consistency” is unclearly described at best.
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?
> 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?
Yes. One way to put it: Provability Logic is balancing on a knife-edge. It works, but just barely. However, you can turn it around and say the new notion is balancing on a knife-edge by requiring DAG (Directed Acyclic Graph) at meta-level. They way I see it, is that both approaches have implicit assumptions and you have to trade one with another.
I am working on an implementation of the new notion of provability (https://crates.io/crates/hooo), after finding the axioms last year (it took several months):
As a modal logic the difference is surprisingly small, by swapping Löb's axiom with T. `tauto_hooo_imply` is slightly stronger than K.
The major difference is that `|- p` equals `p^true` instead of implying, if you treat `|-` as internal. If you treat it as external, then you can think of it as N + T.
I needed this theory to handle reasoning about tautological congruent operators.
However, once you have this, you can perfectly reason about various modal logical theories by keeping separate modality operators, including Provability Logic, e.g. `modal_n_to : N' -> all(a^true => □a)`.
So, it is not a tradeoff that loses Provability Logic. Instead, you get a "finalized" IPL for exponential propositions. This is why I think of as a natural way of extending IPL with some notion of provability.
Thanks for your response. I'm not very familiar with reasoning in modal logic so I'm finding it hard to get an intuition for your `^` operator. Yes, it does seem like some kind of generalized provability. Does `a^b` mean `a` is provable in all worlds in which `b` is valid, i.e. taken as an axiom in the underlying proof theory, or something like that?
This is very interesting, but unfortunately I have more mundane things to get to. Hopefully I'll find some time to play with your axioms and relearn whatever modal logic I once knew.
> Does `a^b` mean `a` is provable in all worlds in which `b` is valid, i.e. taken as an axiom in the underlying proof theory, or something like that?
Yes. You can also think of it as a function pointer `b -> a`. Unlike lambdas/closures, a function pointer can not capture variables from the environment. So, if you have a function pointer of type `b -> a`, then you can produce an element of type `a` from an element of type `b`.
This sounds almost like the same thing as with lambdas/closures. The difference is that a lambda can capture variables from the environment, such that `b => a` is possible "at run-time" in a way that does not hold for every possible world. So, the distinction between function pointers and lambdas/closures can be thought of as different notions of provability at static compile-time and dynamic run-time.
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.
Within the lens of the other religion probably. Except from hardcore zealots, religious people often agree on true things that they find in common between religions (eg idol worship being a sin, murder, adultery, etc etc).
I don't think that's a problem: if there are uninteresting languages, then you must study them, then work hard to prove that they are uninteresting first. That is, mathematics indeed does study uninteresting languages.
.. mathematics is the same for me as GP said: you have a set of symbols, a set of rules, now derive true statements. (Or at least this is a good view, but other views can be also good.)
There are uninteresting languages that can be considered, but nobody considers them unless a reason arises to do so.
Attempting to prove that they are uninteresting is not itself an interesting problem, because it is easy to prove that such proofs do not generally exist. Indeed things become interesting not because they are inherently interesting in and of themselves. But because something else that is already interesting turns out to connect to the not yet interesting thing, and studying the not yet interesting therefore becomes relevant to the interesting one.
The uninteresting languages are still part of mathematics though. It’s just that we choose not to explore them because we don’t think there’s any value. If you limit it just to the languages that we find interesting, then “what is mathematics” is a fluid definition depending on what we choose to focus on today whereas my definition is a bit more durable.
Also, on the topic of “uninteresting”, if I recall correctly number theory (or discrete math) was explored by a mathematician claiming it’ll never have any application and that’s why he was doing it, only for cryptography to come by within a century after that. At least if I recall the apocryphal story told to me in class correctly. Erdos seems like he’d line up time wise and focus wise but I can’t find any quotes from him to that effect so maybe I’m misrembering?
I don't hold with drawing the strokes too broadly. If we take a broad definition of mathematics, both computer science and chess would be branches of mathematics. Such a definition doesn't capture what I want to think of as mathematics.
There is one comforting conclusions which is easy for a real
mathematician. Real mathematics has no effects on war. No one
has yet discovered any warlike purpose to be served by the theory
of numbers or relativity, and it seems very unlikely that anyone
will do so for many years.
Given that he wrote this in 1940, relativity was a bad prediction. The theory of numbers also become useful thanks to cryptography.
He also makes reference to a belief that Gauss said something like, "if mathematics is the queen of the sciences, then the theory of numbers is, because of its supreme uselessness, the queen of mathematics..." But he argues this only to undermine it.
I don’t follow. Computer science is a branch of mathematics though, at least it’s considered as such by many university curricula. Technically, I’d say it’s more of a label to a cross sectional combination of branches of mathematics or viewing existing branches through a computational lens, but plenty of mathematical proofs use bridges across branches to solve problems that neither branch could alone. CS covers number theory, graph theory, game theory, discrete math, Boolean algebra, trigonometry, geometry, etc etc etc. Granted there’s a bit of inherent element of engineering in most of it too because “see the math running in reality” is a natural desire. That and computers offer faster feedback loops to playing around with mathematical ideas.
Chess is 100% covered by the branch of mathematics connecting game theory and search and you can translate computational problems onto chess boards in a fashion [1]. So if computational math is part of math and chess is part of computational math, then chess is math.
I think the discomfort you face is that nearly everything can be described with math which means nearly everything is a part of math even if we haven’t described it mathematically yet. And then if everything is math, setting up rigid boundaries between “math” and “not math” is difficult, but I don’t think that’s a bad thing - binary classification is famously problematic when trying to apply to the real world (eg genuses in biology are a valiant but ultimately futile attempt).
Granted it’s possible the language definition is necessary but not sufficient. Something about formalism maybe? Not sure. What does math mean to you?
Thanks for that quote btw - it’s 100% the quote I recall reading.
* edit: here’s a relevant quote from Hardy’s Wikipedia page:
> A chess problem is genuine mathematics, but it is in some way 'trivial' mathematics. However ingenious and intricate, however original and surprising the moves, there is something essential lacking. Chess problems are unimportant. The best mathematics is serious as well as beautiful - 'important.'
> Also, on the topic of “uninteresting”, if I recall correctly number theory (or discrete math) was explored by a mathematician claiming it’ll never have any application and that’s why he was doing it, only for cryptography to come by within a century after that.
I know a version that the motivation was that they can't use it in wars (so the mathematician was a pacifist instead of an arse). I can't find a source for this anecdote either. I probably heard it about Paul Turán, but anyone doing discrete math at that era (number theory, graphs, combinatorics) would do.
Makes sense. I never thought the mathematician was being an arse. To me it was just a reminder that no matter how well versed you may be in mathematics, any prognostication about the uselessness of a mathematical field is likely to be proven incorrect in the long run.
English grammar can be. Buffalo is an animal, a city, and a verb meaning "to bewilder and confuse". As a result the following can be proven.
The word buffalo, repeated any number of times, can always be parsed into a valid English sentence. If the number of times it appears is prime, it can only be parsed into ONE possible English sentence.
No, it is a mathematical statement about linguistics. It should not be surprising that mathematics can be used to describe things. Everything in the universe can be described by mathematics--even truly random, acausal events have probability distributions which are described by mathematics. But being described by mathematics does not make it mathematics. That's a type error.
I think so, but it wouldn’t be very interesting. The rules of Japanese grammar mathematically could only tell you if something is in the Japanese language or not. The other challenge is that human languages tend to be filled with exceptions and intentional violations of rules for creative effect. That kind of stuff doesn’t really fly in mathematical languages.
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.
I agree that the treatment of alpha equivalence might not be the best. Isabelle/HOL has pattern unification which makes it easier.
For the type variables: it's a matter of taste! I prefer it this way, and it's quite useful if you expect terms and theorems to have free variables (quite common in automatic provers). Having free variables is a good way to specify things like rewrite rules, backward chaining clauses, etc. so it doesn't come out of the blue.
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.
Why do dependent types require universe levels to be consistent? I mostly see that in the context of the type of all types and similar, which doesn't seem especially necessary to express. A variable that denotes a type could have type 'any' or 'unspecified', as opposed to a type T^1 or similar.
You would have to not use a type-based proof system. I think those are not going to be the "as simple as possible" ones. Consider metamath for example.
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.
I don't follow. At a guess, my "definitional equality" is your "syntactic equality", but I can't infer what you mean by definitional. Perhaps our terminology is too different to communicate successfully.
(+ X X) is not definitionally equal to (* 2 X), for they are different definitions. Different pictures on the page. A proof that they are equivalent is not a proof that they are equal. A proof that they are equal is evidence that your proof system is unsound.
If you assume a symbol is not definitionally equal to itself, you can indeed prove false, but that doesn't seem particularly important since you cannot prove that a symbol has a different definition to itself.
Yeah, this is too imprecise. I tried to translate to your terminology, but failed.
My system uses "tautological equality" and this allows me to treat them the save way for all tautological congruent operators. Ofc, you can't treat them the same if an operator is neither normal nor tautological congruent.
Even if you have a such operator `foo'(x)` you can prove `foo'(x)`, `(foo'(x) == foo'(x))^true` or `foo'(x) == foo'(x)` etc. If this is what you are talking about, then this system supports it.
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.
Any links/examples of why this isn't possible? My thinking is - if all existing set theory and set theoretic proofs are expressed in finite set-theoretic statements/expressions - can't we 'encode' these expressions within the system of arithmetic?
Do I have links off the top of my head that directly address this, no unfortunately I do not. I do have links to different pieces that you can use to understand this, however. First is the notion of the consistency strength of a formal system which basically is the ability of one formal system to prove the consistency of another formal system [1].
ZFC is strictly stronger than PA in the sense in that ZFC can prove the consistency of PA [2].
From this, however, it follows that PA can not prove the consistency of ZFC. If PA could prove the consistency of ZFC then ZFC would be able to prove the consistency of itself, which we know from Godel's incompleteness theorem would mean that ZFC is inconsistent [3].
So this gives one concrete proof that ZFC can produce that PA can not produce, namely the consistency of PA itself.
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.
Oh, it does give you special insight, but it doesn't make you infallible. It is easier to reach for something if you feel that it must be out there, and you just haven't got it right yet. That's how most mathematicians feel. Gödel was a Platonist, and I'd say he had really special insights.
So there's no actual advantage, since you can still be wrong and grasping for something that doesn't exist or that you can't define properly. It's just adding more mysticism to mathematics.
No, it is actually the opposite. It is removing mysticism (which I hate) and adds clarity. There are real things out there, and we can go and use them for our purposes. These things are so flexible that we can shape them into pretty much anything we want, bar inconsistency.
But yes, you need to state clearly the properties you are talking about. These can be axioms (and must be to a certain extent), but most of your math will consist of definitions (and theorems about them). And by doing all of this in a logic, on a computer, there is really no way to be much clearer and less mystic.
Thinking purely conceptual notions are real is mysticism. It's a confusion of layers, like in an Escher print: The hand is drawing itself, the water is going around infinitely, because the background is bleeding into the foreground and there's no consistent hierarchy. Well, an idea I have doesn't get to be as real as I am, too; I can't make a sphere be just as real as I am just because I imagined a sphere, any more than I can put a million dollars into my hand just because I imagined it to exist.
> But yes, you need to state clearly the properties you are talking about.
This is normal mathematics. It isn't unique to Platonism.
> And by doing all of this in a logic, on a computer, there is really no way to be much clearer and less mystic.
A software object, as a pattern of charge in memory circuits or in a storage device, isn't a Platonic form. It is real and it has all of the limits a real, physical object does, just like a bunch of marks on a blackboard or ink on a page. It is, conceptually, just notation, albeit one which is much more useful in some ways than paper notation. Platonism, as I understand it, posits that the purely conceptual is real, and partakes of forms, and all representations of those concepts are shadows of those forms.
Except... is Number a Form? If so, it would have one consistent set of properties, yet mathematicians have a lot of different kinds of numbers, with different properties, all useful and consistent within a given axiom system. Real numbers, Integers, Natural numbers, Complex numbers, Quaternions, Octonions, and Sedenions are all numbers, but no two of them are the same, and no two of them can, therefore, be of the same Form. In fact, we can apply what's called the Cayley-Dickson construction to create as many different kinds of numbers as we wish, to infinity, no two of which are the same but all of them are consistent and have some claim on Number-ness. If the form Number can be stretched that far, it isn't very good at predicting the properties things will have, and so it isn't all that useful, even aside from the objections I have to abstract concepts being real on the same level as me.
> Thinking purely conceptual notions are real is mysticism.
No, it is not. We just have to disagree here. What is 1? What is 2? Is it real? Of course it is. Is 3.5 + πi real? Yes, because what are you talking about if it is not? Something unreal?
> This is normal mathematics. It isn't unique to Platonism.
You can do mathematics without any philosophical grounding. In fact, most people do. It's just the way you study mathematics at university, it is pretty much platonic. Here is a vector space, deal with it. And it is pretty much the only philosophical grounding that makes sense to me. Of course a Turing machine is real. At the same time it is a purely mathematical object. So this mathematical object is real, and so are many others. You can make new concepts up as you go, and they are all real, if they are consistent. That's not mystic, it is a simple fact of life you should accept. It is not more mystic than life itself. Many concepts are real. That's why you can apply logic to them, and it works. And for some concepts, you can write them down, but they are inconsistent. And these are not real.
Writing down a concept in logic, I use a physical tool, the computer, but I really write it down in a mathematical object, represented on a computer. In my work, in Abstraction Logic. Abstraction Logic is real, even more real than the particular physical manifestation in form of software, for example. The software is just a shadow of the real Abstraction Logic. And only if I did not made a mistake implementing it. What is a mistake? Well, if my shadow doesn't match up to the real mathematical object that is Abstraction Logic.
> Fictionalism, on the other hand, is the view that (a) our mathematical sentences and theories do purport to be about abstract mathematical objects, as platonism suggests, but (b) there are no such things as abstract objects, and so (c) our mathematical theories are not true. Thus, the idea is that sentences like ‘3 is prime’ are false, or untrue, for the same reason that, say, ‘The tooth fairy is generous’ is false or untrue—because just as there is no such person as the tooth fairy, so too there is no such thing as the number 3.
Who knows, maybe they are right. For me personally, this view is not helpful, and it doesn't make sense to me.
The advantage of a robust philosophy of mathematics is that what you're doing actually makes sense. Some people care about conceptual clarity, and others don't. To each their own.
> 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.
> Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations,"
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.