4 ms·

For me, the entire article can be summarised in the following quote from it: >> So there’s a big mess. We are limited in what we can do. We are limited in wha

For me, the entire article can be summarised in the following quote from it: >> So there’s a big mess. We are limited in what we can do. We are limited in what can do. All our formal systems are flawed. That's including arithmetic and Gödel proved that any system powerful enough to represent arithmetic will always be flawed. The machines we have that compute our formal systems with us -and it never stops doing my head in that it's possible to create physical machines to calculate what exists only in our thoughts- our computers, they are flawed, too, because they are based on the same flawed formal systems, the same limitations as ours. We cannot use such machines to escape their own, our own, limitations. >> But we have proven otherwise. Have we now. To whom?

qsort 3y ago
> We are limited in what can do. It's not wrong that we are limited in what we can do, but we are limited in the same sense a Turing machine is limited by the halting problem. We are limited in a very specific and precise sense. > All our formal systems are flawed. This threads dangerously close to the pop-culture take that math is flawed. I can accept this statement only if we take 'flawed' to mean 'incomplete' in the Godel sense. We don't say that integers are flawed because they aren't a field, that's how integers work. We should avoid needlessly loaded words. > Have we now. To whom? We don't prove things to someone. Proofs just are. There's a sleight of hand at play here. A proof in the technical sense (let's call them Tproofs), as a series of deductions, is a mathematical object, not unlike the number five. A proof in the common sense (let's call them Cproofs) is an informal argument to convince other human beings that there exists a Tproof with certain characteristics. In this sense it's easy to see how Cproofs are social phenomena. They are basically ways to communicate with other human beings. Not unlike how banks create money when they issue loans, backed by nothing by the community's trust, a mathematician can write a Cproof standing for a Tproof, backed by the trust of his colleagues. Mathematics could not meaningfully function without this socially constructed web of trust, exactly like the economy could not function if our only mean of exchange were physical coins. I have no problems in accepting that, in this sense, mathematics is a community effort and is strictly dependent on such community existing. But there lies my argument. A proof-checker accepting a proof offers a very strong guarantee that an equivlent Tproof exists, stronger than any number of peer-reviewers could offer. Therefore, to the extent that we deem epistemologically possible to mathematically prove a statement, a proof being accepted by a proof-checker is a mathematical proof. The radical skeptic's argument that it's not, in fact, possible to mathematically prove statements in any meaningful sense is as always both perfectly irrefutable and perfectly uninteresting.
- deleted 3y ago
  [deleted]
- YeGoblynQueenne 3y ago
  >> We don't prove things to someone. Proofs just are. I think you need to do a bit of reading, to see what others have said on this subject, because you seem convinced you have the right attitude and the right frame of mind- but you only manage to trip yourself into making absurd statements like the one above. Proofs just are? Where? I suggest you start here: https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf And here, for a bit more context: https://m-cacm.acm.org/magazines/2021/7/253448-program-verification/fulltext https://m-cacm.acm.org/magazines/2021/7/253448-program-verif...
  - qsort 3y ago
    Program verification, while interesting in its own regard, has nothing to do with what we're talking about here. Proofs as studied by mathematical logic are mathematical objects, not something you "prove to someone", that's the entire and only point, and it's extremely well-grounded in existing theory. It's not even a contentious point, it's not something reasonable people can disagree on.
    - YeGoblynQueenne 3y ago
      >> Proofs as studied by mathematical logic are mathematical objects, not something you "prove to someone", that's the entire and only point, and it's extremely well-grounded in existing theory. Which theory is that? You're saying there's some theorem that proofs are mathematical objects that "just are"? What theorem is that? Can you point to it?
      - qsort 3y ago
        A tree of derivations is a mathematical object that formally represents a proof, which is connected to the way programs are written in proof checkers via the Curry-Howard isomorphism. When we say "proof" in logic we mean that. In common parlance, a "proof" is instead an informal argument. I know that you know that, because I read your messages before and I know you are not an idiot. You are just dwelling on a rhetorical flourish for no particular reason.

qsort 3y ago

> We are limited in what can do. It's not wrong that we are limited in what we can do, but we are limited in the same sense a Turing machine is limited by the halting problem. We are limited in a very specific and precise sense. > All our formal systems are flawed. This threads dangerously close to the pop-culture take that math is flawed. I can accept this statement only if we take 'flawed' to mean 'incomplete' in the Godel sense. We don't say that integers are flawed because they aren't a field, that's how integers work. We should avoid needlessly loaded words. > Have we now. To whom? We don't prove things to someone. Proofs just are. There's a sleight of hand at play here. A proof in the technical sense (let's call them Tproofs), as a series of deductions, is a mathematical object, not unlike the number five. A proof in the common sense (let's call them Cproofs) is an informal argument to convince other human beings that there exists a Tproof with certain characteristics. In this sense it's easy to see how Cproofs are social phenomena. They are basically ways to communicate with other human beings. Not unlike how banks create money when they issue loans, backed by nothing by the community's trust, a mathematician can write a Cproof standing for a Tproof, backed by the trust of his colleagues. Mathematics could not meaningfully function without this socially constructed web of trust, exactly like the economy could not function if our only mean of exchange were physical coins. I have no problems in accepting that, in this sense, mathematics is a community effort and is strictly dependent on such community existing. But there lies my argument. A proof-checker accepting a proof offers a very strong guarantee that an equivlent Tproof exists, stronger than any number of peer-reviewers could offer. Therefore, to the extent that we deem epistemologically possible to mathematically prove a statement, a proof being accepted by a proof-checker is a mathematical proof. The radical skeptic's argument that it's not, in fact, possible to mathematically prove statements in any meaningful sense is as always both perfectly irrefutable and perfectly uninteresting.

deleted 3y ago
[deleted]
YeGoblynQueenne 3y ago
>> We don't prove things to someone. Proofs just are. I think you need to do a bit of reading, to see what others have said on this subject, because you seem convinced you have the right attitude and the right frame of mind- but you only manage to trip yourself into making absurd statements like the one above. Proofs just are? Where? I suggest you start here: https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf And here, for a bit more context: https://m-cacm.acm.org/magazines/2021/7/253448-program-verification/fulltext https://m-cacm.acm.org/magazines/2021/7/253448-program-verif...
- qsort 3y ago
  Program verification, while interesting in its own regard, has nothing to do with what we're talking about here. Proofs as studied by mathematical logic are mathematical objects, not something you "prove to someone", that's the entire and only point, and it's extremely well-grounded in existing theory. It's not even a contentious point, it's not something reasonable people can disagree on.
  - YeGoblynQueenne 3y ago
    >> Proofs as studied by mathematical logic are mathematical objects, not something you "prove to someone", that's the entire and only point, and it's extremely well-grounded in existing theory. Which theory is that? You're saying there's some theorem that proofs are mathematical objects that "just are"? What theorem is that? Can you point to it?
    - qsort 3y ago
      A tree of derivations is a mathematical object that formally represents a proof, which is connected to the way programs are written in proof checkers via the Curry-Howard isomorphism. When we say "proof" in logic we mean that. In common parlance, a "proof" is instead an informal argument. I know that you know that, because I read your messages before and I know you are not an idiot. You are just dwelling on a rhetorical flourish for no particular reason.