5 ms·

> Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is no

by prmph 4y ago

> Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is not a social construct at all. I think you are mistaken. The idea that math proofs are a social construct relates to, in my view, much deeper ideas than you seem to think [1]. 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. Take the proof that the square root of 2 is irrational. The proof relies on a contradiction that arises if one assumes the root is rational, but one can imagine a logic system where such a contradiction does not imply that the original assumption is false. How possible, you say? It's all math, where one is allowed any starting assumptions, and works out the implications of those. But, there is something deeply satisfying about thinking that contradictions are (or should be) impossible in our universe, and so this "proof" seems solid. 1. https://plato.stanford.edu/entries/intuitionism/ https://plato.stanford.edu/entries/intuitionism/

qazxcvbnm 4y ago
> 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
I am very familiar with those "deep" ideas. It is really just about which axioms you are willing to accept. If you want to deny yourself the law of contradiction, that's fine, go ahead. There are structures where this law doesn't hold if you interpret the logical operators in a special sense, so there are valid reasons for doing so. For example, it is an elegant mechanism to reason inside of Kripke structures. Personally, I don't think intuitionism makes much sense on a fundamental level beyond being an elegant mechanism in certain situations. If you tell me that it is false that A is false, then certainly A is true. Anything else is really mystic mamboojamboo and not clear thinking. But that's just my opinion, and I am not gonna force it onto you, because this is not something I can prove in a proof-assistant, but just an opinion, and as such a social construct. I am not really dogmatic about this. You might be able to use intuitionism for things that cannot be done via classical reasoning, for example extract programs from a proof. I have yet to see an example where it is not simpler and more straightforward to just prove an executable program to be equivalent to the specification using classical reasoning. My point of view is the following: If you are not able to (eventually) make your case within a proof assistant, then what you are trying to tell me is not math.
zmgsabst 4y ago
> Take the proof that the square root of 2 is irrational. The proof relies on a contradiction that arises if one assumes the root is rational, but one can imagine a logic system where such a contradiction does not imply that the original assumption is false. How possible, you say? It's all math, where one is allowed any starting assumptions, and works out the implications of those. The truth or falsity of that statement in a model is independent of who observes that model. The only “social construct” you’ve described is which model to use by default — literally, a notation convention, nothing semantic. > But, there is something deeply satisfying about thinking that contradictions are (or should be) impossible in our universe, and so this "proof" seems solid. Our universe either does or doesn’t, depending on which model best represents it — we’re only debating what assumption to make about an unknown.

by prmph 4y ago

qazxcvbnm 4y ago

> 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

I am very familiar with those "deep" ideas. It is really just about which axioms you are willing to accept. If you want to deny yourself the law of contradiction, that's fine, go ahead. There are structures where this law doesn't hold if you interpret the logical operators in a special sense, so there are valid reasons for doing so. For example, it is an elegant mechanism to reason inside of Kripke structures. Personally, I don't think intuitionism makes much sense on a fundamental level beyond being an elegant mechanism in certain situations. If you tell me that it is false that A is false, then certainly A is true. Anything else is really mystic mamboojamboo and not clear thinking. But that's just my opinion, and I am not gonna force it onto you, because this is not something I can prove in a proof-assistant, but just an opinion, and as such a social construct. I am not really dogmatic about this. You might be able to use intuitionism for things that cannot be done via classical reasoning, for example extract programs from a proof. I have yet to see an example where it is not simpler and more straightforward to just prove an executable program to be equivalent to the specification using classical reasoning. My point of view is the following: If you are not able to (eventually) make your case within a proof assistant, then what you are trying to tell me is not math.

zmgsabst 4y ago

> Take the proof that the square root of 2 is irrational. The proof relies on a contradiction that arises if one assumes the root is rational, but one can imagine a logic system where such a contradiction does not imply that the original assumption is false. How possible, you say? It's all math, where one is allowed any starting assumptions, and works out the implications of those. The truth or falsity of that statement in a model is independent of who observes that model. The only “social construct” you’ve described is which model to use by default — literally, a notation convention, nothing semantic. > But, there is something deeply satisfying about thinking that contradictions are (or should be) impossible in our universe, and so this "proof" seems solid. Our universe either does or doesn’t, depending on which model best represents it — we’re only debating what assumption to make about an unknown.