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.
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.
>> 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?
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.
>> 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?
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.
I can't say whether I'm an idiot or not but, indeed, my background is in logic programming, first order logic and automated theorem proving (and other fields, not related to our discussion). Thus, I know that there is no formal concept of "proof" in logic. Even in automated theorem proving we formally define derivations, or deductions (which can be represented by the "mathematical objects" in your comment), but not proofs. As far as I know there is no mathematical or computational procedure that can construct "a proof", only arrive at a result that can be considered a proof, when the result is inspected by a human mathematician or computer scientist.
The concept of "proof" is, to my knowledge, only an informal concept, that only makes sense, and is only communicated, between humans. In mathematics that is even more so than in computer science. Certainly I wouldn't expect any expert on logic and proofs, to say that proofs "Just are". That sounds mystical, practically Platonic.
To give a concrete example (and you will excuse, I hope, my penchant for rhetorical flourishes, or at least terminological clarity, when I speak of the matters of my expertise) in Resolution-based automated theorem proving the derivation of the empty clause during a Resolution-refutation of a goal clause can be considered as a proof-by-refutation of the complement of the initial goal. That is so because we know that, if a set of clauses, Π, is unsatisfiable, then the empty clause is a logical consequence of Π. Therefore, if we can derive the empty clause from the union of a goal, G, and a set of clauses, Σ, we can assume that G is false, with respect to Σ (or, more precisely, that G is not a logical consequence of Σ) and that, therefore, ¬G must be true. We can do all that because we have fuzzy, human-readable proofs that convince us of the relation between Σ and G, and the derivation of the empty clause from their union; for example, in the Resolution theorem by J. Alan Robinson [1]. It would not be possible to set up an automated theorem proving system without such a human-readable, and human-convincing proof. Because nobody would trust it.
In fact, the Resolution Theorem, essentially a statement of the soundness of Resolution, is a statement of such irrefutable simplicity that there can be no doubt of its truth and, as far as I know, it has only been proven once, by Robinson, then his proof cited by anyone else interested in the matter. The completeness of Resolution on the other hand is more complicated to show and there have been many different proofs of it, in different forms (i.e. the Refutation-completenss of Resolution, and the Subsumption Theorem, proved by Robinson and others in different ways). Given that there are now many different proofs of the Completeness of Resolution, arriving at it from different directions, we can also be reasonably secure in the knowledge that Resolution is complete. We may still be wrong. Some proofs have been shown to be wrong [2].
That is how proofs work in practice.
I commented to help you understand where you are wrong, and because I, in turn, was "triggered" by your arrogant insistence about things you clearly do not know as well as you think you do. I suggested you do a bit of reading to avoid polluting our common space on HN with bullish ignorance. You reacted with offense. That is a natural reaction, and I have experienced it myself, but I hope that you can nevertheless take something useful from our exchange. I have studied long and hard to acquire the knowledge that I have and I consider it my responsibility to share this knowledge. Perhaps I should refrain from doing that in the future though, if it ends up being more "triggering" than informative.
________________________
[1] A machine-oriented logic based on the Resolution principle, J. A. Robinson, journal of the ACM, Jan. 1965.
I don't doubt that this is the case. The reason why I found your response triggering is that you did not come off, in this exchange, as genuinely having that intention, from the very beginning.
To be completely frank it just looked as though you were looking for a fight.
I recognized your username among the responses. I knew you had that kind of background and wanted to hear from you.
I am not an expert nor I claim to be, mine are just fade memories, but as far as I know using "proof" to mean "derivation" is not uncommon, see for instance[1][2][3]. I was very particular about separating the "formal" and "informal" kind in any case. I don't think I can be accused of playing fast and loose with definitions.
If you are trying to correct me on something else, I don't understand what it is.
Since you brought up that point yet again, by "proofs just are", an unfortunate choice of words, I do not mean anything mystical or platonic. I never had any intention of making such claims and I certainly don't stand by anything like it. I wanted to say that derivations (I used the "proof-in-the-formal-sense" language to which you object, I am amending it here) are mathematical objects, proofs (meant as you do, informally) are social processes.
I do not understand your response as saying anything different.
As far as I understand, all you're objecting to is my use of language. This is perhaps fair, but not terribly interesting. If there's something else, I'm afraid I failed to understand what it is.
In any case, thank you for this exchange.
I would like to encourage you to keep sharing your knowledge if you can make the time. I am sure this common space would benefit from it.
Thank you for your kind comment and for your patience. I think my comments above were awkward and didn't quite get my point across, and that's obviously not your fault but mine. Hopefully we'll have the time to discuss this issue again in the future. I'm sorry that we started off on the wrong foot.
> 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.
Interesting to me is whether this "the" "radical skeptic" you're mocking is as it seems to be. I'd say it has the odor of a very convenient rhetorical strawman.
When practicing logic, don't forget the importance of ontology, as one could learn from epistemology. But then, that's a lot of work, and that sort of thinking "is" "pedantic".
Welcome to Planet Earth, circa 2023, {the culture you live in}, please enjoy your stay.
>> 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?