4 ms·

> It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even i

> It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even if it seems unassailable, even if built into an automated checker, is still a product of the human mind. Usually there is a level of logic that can challenge even what seems so basic as to be fool-proof. I think you are mistaken. I used to be very troubled by the notion that no single set of axioms really can be agreed on to do mathematics, but I have been convinced finally that the truth of the matter is a very subtle point; that the truth of mathematics is absolute; it merely is not finitely-axiomatisable. With a sufficiently weak proof system, clearly we can conceive of a system where the irrationality of the square root of 2 is not provably true, but no consistent proof system can prove that the square root of 2 is rational. Certain mathematical constructs, indeed most(*) of known mathematics, that which is constructible by constructivist methods, are irrefutably there in any consistent mathematical universe, and in that sense, true. Yet, no single axiom system can encompass all mathematical truth, as is well known from Goedel's theorems, but neither does that mean that the set of axioms to be worked with can be arbitrarily chosen. The chosen set of axioms must be consistent. The question, then, is whether consistency of axioms can possibly be an objective fact; and even though for any sufficiently strong set of axioms, its consistency cannot be proven in of itself, it consistency can in fact be objectively established - objectively established, but not finitely established. My evidence for this perspective is Scott Aaronson's construction of a Turing-Machine encoding of the ZFC axioms. What the construction of this encoding implies, is that the revelation of the uncomputable busy-beaver (BB) function for value 8000, which is a finite, well defined, and an objectively irrefutable, albeit unthinkably massive, number, constitutes a proof of the consistency of ZFC axioms. A similar procedure I believe can be applied to any set of axioms that one wishes to work with. The part where the magic occurs, I believe, is in the uncomputable nature of the BB function, by which it is possible to finally and objectively establish consistency of sets of axioms. Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values; that is the nature I now take of mathematics as well.

auggierose 4y ago
> Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values That is kind of obvious, isn't it? But some people need more convincing than others :-)
dorchadas 4y ago
But what this doesn't get at is that the very system of logic we use to make proofs is a social construct. Other cultures have had other systems of logic, and called valid arguments that we wouldn't today precisely because they were using a different system of logic. So the very foundations of mathematics, the logic we use behind our proofs, is inherently a social construct that arose out of Greek philosophy as it was adapted in the west.
- naasking 4y ago
  > But what this doesn't get at is that the very system of logic we use to make proofs is a social construct. Other cultures have had other systems of logic, and called valid arguments that we wouldn't today precisely because they were using a different system of logic. I think you need to separate the process of developing mathematics, from the self-consistency and validity of the logical argument or mathematical structure itself. The process is social but the validity and mathematical structure itself is not. Computer science has led to an explosion in different logics. We've never had more logics/formal systems than we do today, but whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus.
  - musingsole 4y ago
    > whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus. The definition of "consistent" seems completely entangled with a given social group's ideas of "rational". You might imply that our word for it hints at a Platonic ideal of "consistent", but if that's true, then you're caught in an infinite cascade of which nuances of meaning between the Platonic Ideal and our concrete reality are actually reflections of the truth or corruption of it.

auggierose 4y ago

> Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values That is kind of obvious, isn't it? But some people need more convincing than others :-)

dorchadas 4y ago

But what this doesn't get at is that the very system of logic we use to make proofs is a social construct. Other cultures have had other systems of logic, and called valid arguments that we wouldn't today precisely because they were using a different system of logic. So the very foundations of mathematics, the logic we use behind our proofs, is inherently a social construct that arose out of Greek philosophy as it was adapted in the west.

naasking 4y ago
> But what this doesn't get at is that the very system of logic we use to make proofs is a social construct. Other cultures have had other systems of logic, and called valid arguments that we wouldn't today precisely because they were using a different system of logic. I think you need to separate the process of developing mathematics, from the self-consistency and validity of the logical argument or mathematical structure itself. The process is social but the validity and mathematical structure itself is not. Computer science has led to an explosion in different logics. We've never had more logics/formal systems than we do today, but whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus.
- musingsole 4y ago
  > whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus. The definition of "consistent" seems completely entangled with a given social group's ideas of "rational". You might imply that our word for it hints at a Platonic ideal of "consistent", but if that's true, then you're caught in an infinite cascade of which nuances of meaning between the Platonic Ideal and our concrete reality are actually reflections of the truth or corruption of it.