> That’s a lovely fantasy, but Gödel shows that there are fundamental epistemic limits to the universe, things that no genius will help us to know, no alien race could teach us, no machine could be built to solve, and no new kinds of mathematics will uncover.
That's not quite true. As an example, take differential calculus. It is hard to see how that would have been an idea to arrive at automatically by an algorithm, but a few geniuses (Newton/Leibniz) got there anyway. Similarly, even when a theorem doesn't follow from the usual axioms (and neither does its negation), maybe another genius comes along with an axiom that is quite obvious, and allows us to prove the theorem (just like peano axioms are axioms we would just accept as being obvious).
So it is not that we cannot know everything, it's just that there is no guarantee and no obvious way of doing so.
But, that's not what Gödel proved. Not that things are hard, or non-obvious. But, that there are actual limits we won't be able to get past regardless of how much time and cleverness we apply to them. The limits might be very large. Might be unlimited for practical purposes. But, they are there waiting for us.
I don't understand his theorems well enough to pretend to explain them to this audience. But, this is my understanding of them.
> But, that there are actual limits we won't be able to get past regardless of how much time and cleverness we apply to them.
Nope, all he proved is that there is no automatic and purely formal way of arriving at truth. Doesn't mean that for any particular truth we cannot stumble upon a way to understand it anyway.
For example, we cannot write a program (= automatic and purely formal way) to determine in general if an input program halts. But for a particular input program, we might be able to understand whether it halts anyway. There is just no a-priori guarantee that we will.
I really don't think that this is the case. Godel proved that some truths cannot be proven. That seems pretty fundamental, and I think that's what made him so impactful, e.g. much more than e.g. the halting problem, which is about computation solely.
What Godel also showed was that we can expand our a prioris, e.g. add another truth that "feels" intuitive to the axioms, and then we can understand some theorem or truth (ie. look under the hood, understand its mechanics). But that means expanding the system by some sort of oracle, some sort of "genius intuition". Fair enough, mathematicians will agree by consensus if it's the right think to do, but it's also infinitely regressive. So I'd agree with corysama here "we won't be able to get past regardless of how much time and cleverness we apply to them".
If by proof you mean using a fixed formal axiom system, then yes, you are right. But let's look at one particular such thing that cannot be proven formally within itself: The consistency of Peano arithmetic. But, I don't need a formal proof for that: It's obviously consistent, because the natural numbers form a model for Peano arithmetic. So I just gave you a proof, but it is not a formal one. Yet, I don't see how anyone of sound mind can reject this proof.
So Peano arithmetic is obviously something we can assume when proving other, more complicated truths. And nobody can say, not even Gödel, that we will not keep finding similarly obvious truths for the more complicated truth we otherwise care about, but which might not be provable from the currently established axioms. Given that Gödel is a Platonist, he would probably agree with me on that.
I'm not sure you're responding to the same point by the GP. GP claims some truths cannot be proven. You took one claim that could be proven ( https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof ) and tried to proclaim its truth without referring to the proof.
Even the GP's claim is problematic. The Gödel's theorems don't prove that some truths cannot be proven. It only proves either ZF is inconsistent, or some truths in it cannot be proven.
Ironically GP's implicit assumption that ZF is indeed consistent mirrors your response in which you claim Peanno is consistent... :D
That said, if you somehow proved that "some truths cannot be proven within a fixed formal axiom system (that is sufficiently powerful)", and then you also take into account the Church-Turing thesis, i.e. that Turing machines can fully model our thoughts, then the proof of the claim about "some truths cannot be proven" is more or less complete.
Of course you can always posit the existence of some "unknown unknowns" that are outside of our wildest imaginations and thus invalidating whatever we thought we have known. But that's outside of our current ability to reason.
I could go on and talk about what I understand about divine inspiration and knowledge, but I suppose those topics are a bit too speculative for the crowd here...
> I could go on and talk about what I understand about divine inspiration and knowledge, but I suppose those topics are a bit too speculative for the crowd here...
you're appealing to common sense to demonstrate the consistency of peano arithmetic. this has two main problems:
1. it's subjective and culturally dependent. most people intuitively reject peano arithmetic in their childhood; until they have been repeatedly told otherwise, they intuitively believe that there must be some biggest number. often in english-speaking countries they think that number is called 'infinity'
2. common sense is also what tells us that the earth is flat, the sun goes around the earth, it's impossible to create a vacuum, things only keep moving as long as there's some force impelling their continued motion, people can't fly, if a vacuum did exist rockets wouldn't work in it, and so on
it turns out that once people stopped relying on common sense so much and started using formal axiom systems, they were able to learn a lot of things in only a few centuries that not even their smartest ancestors had ever been able to figure out during thousands of centuries
This I learned from GEB too I think, the aha moment around 200 years ago when people understood formal axiom system can be arbitrary, and even counterintuitive. Rather than creating a crisis of confidence, and the collapse of the field, it was the start of a whole new era for mathematics (and eventually physics, e.g. it's hard to imagine something like, I don't know, relativity, if math/physics had remained rooted in "common sense").
note that this isn't the first time; you can see it clearly in eudoxus, euclid, archimedes, and the antikythera mechanism, and lucio russo's book tells the story of how science was rapidly developing until the roman conquest brought it to a crashing halt
So you are saying Kepler and Galileo used formal axiom systems? Give me a break.
1. needs a citation. I never believed such a nonsense.
Common sense with respect to the physical world is different to common sense with respect to the world of mathematical objects.
In fact I don't like the word "common sense" when applied to mathematics, I prefer the expression "mathematical reasoning". In fact we model the physical world by representing it via mathematical objects, because mathematical reasoning is so much more reliable than common sense with respect to the physical world. In fact the advantage of such a mathematical model which we can subject to mathematical reasoning are so big that we are OK with the fact that the model might only be approximating physical reality.
In the mathematical world formal logic is a great tool for mathematical reasoning. Mathematical reasoning tells us that if we can represent our reasoning via formal logic, then we can be sure that it is correct. But formal logic has its limits, and in the end mathematical reasoning is the final arbiter, not formal logic: The peano axioms are consistent, because the natural numbers exist. Which is obvious and doesn't require a formal proof (which does not exist, by the way, and will never exist; but that we can know this, is a testament to the power of mathematical reasoning).
no, kepler and galileo didn't understand formal axiom systems; even today you can read galileo's mystified remarks upon encountering that manner of thought in the surviving fragments of eudoxos
when you say 'because the natural numbers exist' what you are really saying is 'because i am a platonist'. while that is a perfectly reasonable reason for you to believe things, it's not going to convince anyone else, in many cases not even other platonists. i reserve the term 'mathematical reasoning' for things that do, and i think that's a more widespread definition than the one you are using
Well, show me a mathematician who does not believe in the natural numbers. And yes, I am a Platonist, just as Gödel is. If you are not a Platonist, your view cannot be defended. It is as simple as that. I don't really care to convince non-Platonists, except for them to become Platonists.
What is your definition of mathematical reasoning then? If it is just formal logic, we could not even work with natural numbers. Even better, we could not even justify formal logic.
I am a big fan of formal logic, so much that I got myself a PhD in implementing formal logic on a computer. I want to do as much mathematical reasoning using formal logic as I can. But it is clear that formal logic has its limits, but that doesn't mean that mathematical reasoning has the same limits. The natural numbers show us otherwise.
mathematics probably began as platonism, but eudoxos put it on a purely hypothetico-deductive basis before platon's corpse was cold, so this debate has been going on for a while already. however, from the end of the hellenistic age until the 19th century, mathematics was utterly dominated by platonism
the social situation is quite different today. as you and i both know, there are plenty of formalists in mathematics, and quite a few constructivists as well, and none of them are platonists; we might even argue that at this point formalism is more popular than platonism among people working on foundations of mathematics. wildberger, a constructivist, is probably the most notorious living anti-platonist extremist who's still within the mainstream (i.e., he's a real mathematician, not just some bozo like me): https://njwildberger.com/2021/10/07/finite-versus-infinite-r... is a sample of his anti-platonist rhetoric. and, as you are certainly aware, voevodsky's extremely influential hott is fundamentally constructivist. https://en.wikipedia.org/wiki/Ultrafinitism is (or was) full of mathematicians who do (or did) not believe in the natural numbers. and it's easy to find working mathematicians saying things like https://old.reddit.com/r/math/comments/fx6bqv/why_did_brouwe...:
> I don't even know if 7 "exists," let alone pi. Such questions may be interesting, but they're philosophy, not math. Meanwhile, it's useful and mathematically interesting to count to 7, so we do it.
from a sociological perspective, a reasonable definition of 'mathematical reasoning' might be 'whatever arguments platonists can use to convince formalists and constructivists, or vice versa, without resorting to empirical evidence'. (this obviously isn't a logical definition, but i would argue that definitions of commonly used words and phrases are always sociological rather than logical in nature, though we can certainly stipulate a logical definition within the context of a given discussion.) this excludes, for example, which territory rightfully belongs to belgium, whether the earth orbits in an ellipse, or whether the natural numbers exist or not; but it includes the area inside a particular proposed national border for belgium, the properties of ellipses, and the consequences of the peano axioms
i think it is correct that formalists do not believe that formal logic is justified in any fundamental sense, but i haven't actually asked them
Here's the thing: any definition of mathematical reasoning that excludes the natural numbers, isn't a definition of mathematical reasoning.
For example, I cannot convince some constructivists that A or not A is always true when it comes to mathematical reasoning. But it is always true, anything else just doesn't make sense. So a constructivist who doesn't acknowledge that, I cannot take anything serious they say. Note that this is different from coming up with interpretations of ∨ and ¬ such that A ∨ ¬A is not always ⊤, such as Heyting Algebras, for example. And it is different from doing constructive mathematics, which is a very interesting subject.
Voevodsky was not a constructivist. He was looking for a way to do the kind of mathematics he likes on a computer to ensure correctness. He first visited the Isabelle development group to find about that, but simple type theory was not flexible enough for his purposes. So afterwards he fell into the hands of the dependent type theorists, who are all constructivists. He tried to do classical mathematics in their framework, that's where his univalence axiom comes from, but that didn't really work out well so far, and I doubt it ever will (but I don't really understand it, so that's just my opinion).
certainly you have to be able to do mathematical reasoning about natural numbers, but that doesn't necessarily imply determining their ontological status
another useful definition of mathematical reasoning is 'arguments strong enough to convince someone who cannot take seriously anything you are saying and does not trust you at all'
i appreciate the correction about voevodsky; i don't have a phd in the field myself, so that may not be all i got wrong
> certainly you have to be able to do mathematical reasoning about natural numbers, but that doesn't necessarily imply determining their ontological status
That's true, of course you can use something without understanding it, but can you use something, and then deny its existence?
I want to correct what I said earlier about the natural numbers and infinity. Of course you could add infinity to the natural numbers, if you wanted to. This can be done in different ways. It's just that natural numbers without infinity are a simpler starting point.
if i use monopoly dollars to buy the b&o railroad, does that entail that i believe that monopoly dollars exist? surely not in the same platonic sense that you and i believe that 53 exists. monopoly dollars are, i think uncontroversially, merely a socially constructed consensus hallucination, like national borders, google, or adultery; as far as i can tell, formalists claim that 53 is too. for that matter, subjective idealists like berkeley claim that so are physical objects like electrons
i haven't seen a satisfying formalist explanation of why mathematicians of different cultures come to identical conclusions about 53 but vastly different conclusions about national borders and adultery. (borges' tlön, uqbar, and orbis tertius famously makes a similar point satirically about subjective idealism.) but i am forced to admit that the formalists themselves do exist and do make this assertion about 53, and while many working mathematicians are unwilling to wholeheartedly embrace formalism (and even fewer constructivism, though, as you point out, for example in type theory constructivists are ubiquitous), fairly few of them are willing to wholeheartedly reject it and declare certainty about platonic realism, as you are
what i was saying about the natural numbers and infinity is that the "common sense" of many children (though perhaps not your own childhood self) insists to them not that a maximum natural number is logically consistent, which i agree with you that it is, but that it is logically necessary, which of course the peano axioms reject. this, to me, is good evidence that common sense is not a solid enough foundation for reaching mathematical truth
by the way, i want to express gratitude for your willingness to discuss epistemology and ontology without descending into the kinds of vicious personal attacks i generally expect on this website, or more generally when discussing epistemology
A most interesting book in this context is [1]. It has introductory discussions of logicism, intuitionism, and formalism by Carnap, Heyting, and von Neumann, and interestingly, they were not aware yet of Gödel's results at that point which were published in the same year. After that, Heyting's "Dispute" is a nice exposition of the different view points, and I find myself agreeing with much of the intuitionist point of view, namely that mathematical reasoning cannot be reduced to formalism (but I don't agree that intuitionistic reasoning is the only allowed form of mathematical reasoning). I mean, Gödel's incompleteness result is as hard a proof of this as you will ever get! And again, in a later piece by Paul Bernays, "On platonism in mathematics", Bernays states: 'Is it possible to draw an exact boundary between what is evident, and what is only plausible? I believe that one must answer [this question] negatively'. In other words: Common sense is a necessary part of mathematical reasoning. Fundamentally, there is no way around this.
i'm pretty sure lots of greek people know calculus, learning latin isn't that hard, and there are actual calculus textbooks in greek now anyway
if, on the other hand, you mean classical athens (platon and sokrates and all those dudes) then, no, they weren't, archimedes wasn't even born until like 180 years later
That's not quite true. As an example, take differential calculus. It is hard to see how that would have been an idea to arrive at automatically by an algorithm, but a few geniuses (Newton/Leibniz) got there anyway. Similarly, even when a theorem doesn't follow from the usual axioms (and neither does its negation), maybe another genius comes along with an axiom that is quite obvious, and allows us to prove the theorem (just like peano axioms are axioms we would just accept as being obvious).
So it is not that we cannot know everything, it's just that there is no guarantee and no obvious way of doing so.