Mathematical proof is a social compact
quantamagazine.org
quantamagazine.org
Having studied CS in school I'm sort of triggered by this. Might be the editorialization, but this is a statement I have a problem with.
I am not one of those who think that computers will save us all. My point of view is that computers are meaningless machines that do meaningless operations on meaningless symbols unless proven otherwise. This is what gets drilled in your head in any semi-decent CS program and it's a point of view I came to agree with completely.
But we have proven otherwise.
Proof checkers like Lean, Coq, Matita, Isabelle and the like are not like normal code, they are more similar to type-systems and code expressed in their formalisms is directly connected to a valid mathematical proof (see the Curry-Howard isomorphism).
They are usually constructed as a tiny, hand-proven core, and then built on their own formalism, ensuring that what is exposed to the end user is perfectly grounded.
If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.
Of course, computers are physical machines that can potentially make all sorts of mistakes. Hardware failures, cosmic rays, whatever. But the probability of that happening on a large scale is the same probability that seven billion people collectively hallucinated elementary theory and it's in fact not true that there are infinitely many prime numbers.
edit: Just a clarification: it's only this particular statement I have a problem with. The article is very much worth your time. Do not get derailed by the title, it's not some sort of "math is racist" nonsense.
For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.
2. In that example that you gave, you would have additional evidence: if you use your system and every sort returns an empty list, you'd probably notice it quite quickly. You can also do manual or automated testing to see that it does the right thing for example inputs. If you then consider it to be unlikely that someone writes code that would exactly only work for example inputs and only satisfy the specification in the dumbest possible way, then you get some really good evidence that your algorithm is actually correct. 100% certainty is never possible, but there are still degrees.
It would not necessarily be hard to program in those incoherent definitions and get them to prove a result. That wouldn't mean much.
This is different from just programming in the conjecture and letting Lean find a complete proof.
If the proof was translated to Lean, then it would mean a lot if it managed to prove the ABC conjecture because it would mean the proof was correct. It doesn't matter if the proof used crazy definitions. The statement of the ABC conjecture would still be understandable and so the ABC conjecture would be solved.
I would like to point out that it seems like the general consensus now is that Mochizuki's proof is incorrect.
And, as people pointed out early on, one of the problems with the Mochizuki paper is that it provides no new tools or results for other problems in the space. This is quite unusual and was a significant part of the skepticism about the proof being correct.
Contrast this to Wiles proof of the Taniyama-Shimura-Weil conjecture for semistable elliptic curves which proves Fermat's Last Theorem as a consequence and then led to a full proof which later became the "modularity theorem".
If Mochizuki used the tools from his paper come at something already proven from a different direction, that would have lent a lot more credence to his claims.
I agree.
In the Metamath community, we also check all proofs with a collection of verifiers written by different people in different languages, all based on a very small kernel. That provides extremely high confidence in its correctness.
Details in this blog post: https://leanprover-community.github.io/blog/posts/lte-exampl...
So in the end, it's always a question of "community" and "belief that things seen by sufficiently many people are right", eg that after 10 years of using a CPU, we've identified and fixed most bugs, and so the program is even more likely to be valid
In other words, maybe you proved something beyond reasonable doubt, but that's completely useless if you misunderstand what it was that you proved.
Math generally has a higher bar (for better or worse..)
> If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.
I'd phrase it as "If a program is accepted by a _correct_ proof checker, then ...". That makes it clear that we can't escape having to consider how and why the proof checker is considered correct.
Edit: this is not entirely academic. from what I understand, the unsoundness of Hindley-Milner in the presence of polymorphic references was not immediately known (https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...).
Not so fast; it could be done on a _different automated system_ (say, a smaller one) than the one you're building, in which case you're now relying on that system's correctness. Or it could even not be proven at all. This is not too different from what mathematicians do when they (often) say "assuming P != NP", or "assuming GRH", or "assuming FLT", etc etc. It's simply that it's worth being careful and precise.
But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.
For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.
But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.
But we've definitely gotten it right this time...
I wouldn't really so. If you were relying on the type system to tell you about any errors you made in your program, the revelation that your type system was unsound is not "only academic" simply because your program coincidentally didn't have errors. Just like it wouldn't be "only academic" if you discovered that your car's airbags weren't functional for the last 10 years even though you never had any accidents.
Eg.
- Are you sure the compiler is correct?
- Are you sure the OS is behaving correctly?
- Are you sure the CPU isn't randomly glitching out?
There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all.
How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.
Use multiple different compilers and compare results
> Are you sure the OS is behaving correctly?
Use multiple different OSes and OS-versions
> Are you sure the CPU isn't randomly glitching out?
Use multiple different CPU types.
Just for fun, it's not unprecedented that the entire human race is disposed to mislearn basic truths about the universe which have to be unlearned when you get to the point where it matters. See quantum mechanics.
One hopes that conscientious mathematicians are careful to select axiomatizations (such as ZF set theory or the type system of Lean) which faithfully reflect reality. And, within such a system, we can be extremely confident in what we're doing. But the distinct possibility remains that the axiomatization doesn't actually match our universe and, say, admits a proof of false or implies something not physically realizable, such as that a certain computation should terminate, when no real life physical machine obeying the laws of physics can ever do so.
Euclidean geometry is intuitively good and seems to work on relatively small areas of the Earth's surface, but non-Euclidean geometries are inconsistent with it and more faithfully reflect a reality that lacks infinite flat planes.
They are incompatible sets of axioms, but they can describe the same set of shapes, although one system is going to be a lot more inconvenient than the other. The differences are logically interesting, but about as incompatible as choosing to make the origin of a euclidean system one corner of the room instead of another.
In contrast physical theories contradict each other by making different predictions which can be falsified.
Describe/represent the ones that halt using 1; and the ones that don’t halt using 0. This produces the pairs (TM1, 1), (TM2, 1), (TM3, 0) etc.
Using this encoding the problem becomes trivial. It’s all other encodings which are unwieldy, complex and inconvenient.
Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable.
So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not.
Formally speaking Turing machines are formal language recognizers, so in which formal language is the formal statement of the Halting problem expressed in?
I'd also like to see the decider for "admissible" vs "inadmissible" encodings. Input validation is an Interesting problem-domain for sure.
(Of course, this is all for the sake of maximum pedantry)
Moving to a constructive setting lets you say things like "all functions are computable" because it has a restricted notion of function. It does not give you any new information about classical objects.
So express your English adjectives in Mathematics.
What do you mean by “restricted” when you are characterising a function?
Show me the decider… for “classical” and “non-classical” objects.
That is the definition of information; is it not? The answer to a yes/no questions
Is the object classical? Yes/no.
Sure, whatever - the point is that they're different objects, and results about one are not results about the other.
> What do you mean by “restricted” when you are characterising a function?
I mean whatever the word "function" means in a given setting. A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2`. A function in intuitionistic type theory is a well-typed lambda term. A function in the categorical semantics of a type theory is an exponential object. And so on.
> Show me the decider… for “classical” and “non-classical” objects.
No such thing: it's a metatheoretical judgement, not a theorem. Same story as type errors: within the language, `stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense. There is no such object as `stringToUpperCase 5` and so nothing can be said about it internally. When we talk about it, we're talking, from outside the language, about a syntactic construct.
> That is the definition of information; is it not? The answer to a yes/no questions
No. Self-information of a given outcome with respect to a random variable, which is probably the most common sense of the word, is the negative log of its probability. Shannon entropy, also often called information, is the expected self-information of a random variable. Mutual information is the KL divergence of a joint distribution and the product of the respective marginals. There are other notions.
Sorry, I don't understand what you mean by "same" and "different".
By "same" do you mean =(x,y). And by "different" do you mean ¬=(x,y)
Or do you mean something like same(x,y) = { 1 if ??? else 0 }
>A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2
You seem to be confusing syntax and semantics here, and the infix notation isn't helping...
What does =(y1, y2) mean? What does =(x,x) mean?
>No such thing: it's a metatheoretical judgement, not a theorem.
What do you mean? Judgments are first-class citizens in Univalent Mathematics. a:R is a judgment that object a is of type R. This literally means "a proves R", and the particular expression "first class citizen" has well-understood meaning in Programming Language design ( https://en.wikipedia.org/wiki/First-class_citizen ).
>`stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense.
So I must be a miracle worker then? Expressing the inexpressible nonsense...
In [1]: def stringToUpperCase(x): return(str(x).upper())
In [2]: stringToUpperCase(int(5))
Out[2]: '5'
Speaking of randomness in a classical setting, this function exists, right?
f(x) = { 1 if random(x), else 0 }
Relations are functions.
Can you tell us more about this function which relates Mathematical concepts to physical reality?
That is how they are defined in set theory based math. The mathematical definition is not the only meaning of a word. When when start to talk about the physical world, we need additional concepts. You are welcome to read the wikipedia page about correspondence theories of truth.
If you are going to talk about the correspondence theory in the same breath as you are talking about any language - you need to solve the symbol-grounding problem.
What function/mechanism/relation (or if you don't like any of those words - pick your own) grounds symbols?
A triangle in a euclidean system is not the same shape as a triangle in spherical, etc. They are only equivalent in that they have an analogous logical definition in their separate systems.
They don't look the same. They don't describe the same physical phenonoma either. In other words, the physical correspondence is not the same, so there is no contradiction.
In what we laughingly call "normal" geometry, given a line L and a point P not on L, there is exactly one line L' through P parallel to L. In this case, the interior angles of a triangle sum to 180 degrees.
In hyperbolic geometry, there is more than one line L', L'', etc., through P that are parallel to L. In this case, the interior angles of a triangle sum to <180 degrees.
In elliptic geometry, there are no lines L' through P parallel to L. (You also have to alter Euclid's 2nd axiom, defining a line as extending indefinitely.) And in this case, the interior angles of a triangle sum to >180 degrees.
Triangles are triangles; they have three points and three line segments. Their properties, however, are inconsistent in the three axiomatic systems.
If you are operating in a relatively small area, say a bronze-age farmer's field, Euclid's axioms satisfy all your geometrizing needs. If, however, you are on the somewhat-spherical Earth and are dealing with a large enough area, you can make a triangle with three 90 degree interior angles. You can tell which geometry your "physical space" is dealing with, and if you use the wrong one then you will get wrong answers.
For more than 2000 years, geometers assumed their space was essentially Euclidian. It turns out that is not really true, and it also turns out that there are (now, common) situations where the difference matters. So when you do any applied math, you assert that your axioms "faithfully reflect reality". And you may be wrong. And you may not have any way of knowing you are wrong. And you may not even have the mathematical tools to know what "wrong" means.
Let's be careful with our terms!
There is the universe, and then there's reality. They are not the same thing, they only seem that way because that is the model everyone's been raised on, and that "fact" is reinforced and defended daily.
Major mathematical advances come from difficult problems when a new branch of mathematics is invented to solve them. Think of calculus, non-Euclidean geometry, and Turing machines (and their equivalents).
The problem I see with Coq, the proof checker I've worked with the most, and the others I've seen is that the proofs they result in are neither good, understandable programs nor good, understandable proofs. They are as complicated as complex programs, but written in something that isn't a half-way clean programming language, but they're also not written as a traditional proof. That goes back up to the article's point that the purpose of a proof is to convince and enlighten others.
Sure, I'd have to say a proposition proven in Coq is true, but how do you get from that to the ideas in the proof letting you go on to other problems?
When you develop software in Coq and the likes, it is library code. It is high impact code that is guaranteed to be correct. It is written once and not maintained – You would never build the new Twitter in Coq.
When you develop math on Coq, you build abstractions. You just need to know that theorems that you are working on. Then you pull in all the lemmas in coq to help you solve that theorem. You do not need to understand the lammas coq uses to help you prove your theorem – coq does that for you. So your math is extremely concise. This is in opposition to normal math, where you need to be able to explain the hierarchy your theorem works on top of.
Be careful, this is how you get the Ariane V first flight.
"You do not need to understand the lammas coq uses to help you prove your theorem..."
If I wanted to generalize your theorem or move it to some other base abstraction, the first thing I need to do is to read and understand your proof. If that proof is made up of Coq tactics chosen based on "whatever works", I'm going to have a bad day.
Now, many results especially in CS are made by reducing a new problem to an existing theorem, but I don't know how well that works as a general case.
Lean comes closer than Coq, but is still far from this ideal. It may be that AI will need to be involved (as in, there could be a tactic that generates proof terms using an transformer or something).
Coqobol?
That's what "declarative proofs" are for (as seen in Mizar, Isar, and formerly in the Coq plugin C-zar). Most proofs in interactive proof assistants are written as "proof scripts", which cannot be understood without playing them back in the proof assistant (in fact, specifically the version of the proof assistant that the "script" was originally written for) and checking how each step in the "script" relates to the current proof state.
Declarative proofs are more self-contained, in that the assumptions and conclusions involved in each proof step can be ascertained by just reading them in the code. They can also be naturally simplified into structural "proof sketches", where missing steps in the proof could potentially be filled by a proof-searching "AI".
Are Isar updates guaranteed not to break proofs?
@56:26 in https://youtu.be/sv7Tvpbx3lc
Every presentation by its author goes: "here's a triangle, here's a simplex, and now... ta-da... the amplituhedron is the same!"
He skips 15 steps every time. It's literally the "here's a circle, then another circle, and now just draw the rest of the owl", but in terms of theoretical physics.
It's a problem of epistemology, not logic.
Logic itself is subjective. We have a set of heuristics we use to decide if something is "true" in a mathematical and scientific sense. But fundamentally they rely on concepts like "truth" and "logic" which we experience subjectively.
We label a certain set of psychological experiences "true", a certain related set "logical", and a different related set "experimentally valid."
But all we really have is a set of experiences that are subjectively consistent (more or less) and shared.
IMO it's quite likely we're missing a lot. Far from having god-like insight into the ultimate nature of truth and reality our minds are actually quite small and limited.
Many relationships, operations, and elements of objective reality are literally invisible to us because they're far too complex for us to imagine, never mind experience and understand.
This matters because potentially AI may not have the same limitations. We're just getting started with associative cognitive modelling based on ML data compression as opposed to mechanical machine building - which is what traditional code is.
That's a fundamental difference of approach, with the potential to work with a much larger conceptual and symbolic space than we're capable of.
I suspect we'll see some quite interesting outcomes.
Not really, by your logic (heh) everything is subjective: including your own argument about logic being subjective (which in turn uses logic).
Let us say you claim "Nothing is objective". Then it doesn't take a genius to assert that your claim "Nothing is objective" isn't objective.
Using similar reasoning we can also assert that "The speed of light is objective" is not an objective claim.
And we can further assert that both the inner and outer statements are true without arriving at a contradiction.
It doesn't take a genius, merely a very thick skin and a grasp of contextuality, to hold this perfectly reasonable conclusion in a society dominated by naive understanding of non-contradiction.
Objectivity, being an unattainable philosophical ideal, it doesn't prevent us from using the term in more pragmatic/cultural/inter-subjective sense. A white lie - if you will - that only a determined pedant would scrutinize to such philosophical extent.
Just as well, such overt pedantry deserves mockery and contempt.
(One would think I'm some kind of conservative; I'm a gay, Asian American leftist who happens to have a STEM background, and so I hate reading about "socially constructed" arguments--which is what this article is a variation of.)
Relative to which objective standard for reasoning are you asserting that any given argument is "sloppy"?
It's a turning point in one's life when we come to acknowle that we don't have to like the fact that relativism is true.
In what objective system for evaluating proofs will you be presenting this “refutation”?
This whole “we have known” smells of a bandwagon fallacy already. Who do you represent?
I find it mildly ironic that I have to explain evaluation (and it’s dependency on a meta theory) on a forum full of computer scientists…
A. In what system are you presenting your argument here in your comment? Is that system objective or subjective.
B. If subjective, then I declare your argument to be false for me. End of story.
C. If objective, then congrats, you refuted yourself.
I find it wildly ironic that you condescend and resort to veiled ad hominem on top of a Logic/Philo 101 fallacy known for literal centuries.
Also, the statement “there is an objective system X” doesn’t imply “we fully know the system X”
I represent scientists and logicians and philosophers that have known this for, once again, centuries. People call X background or classical logic.
B. If you declare my “argument” subjective (and therefore false for you, but true for me) you agree with my overall claim Q.E.D
C. Is it this one then? How would you prove this?
D. It is mighty presumptuous of you to assume that I subscribe to classical logic; or even a consistent logic for that matter. Or that I subscribe to the same logic at different times of day.
E. I am not impressed neither by your religion; nor by the writings of your prophets. Nullius in verba
That is what counts as an argument! An argument is a technical term from logic and includes inferences and observations (observations are single step inferences). My bad on using logic jargon, but yes, inferences/arguments/proofs all apply here. So what system are you presenting this inference in? Is that objective or subjective?
> B. If you declare my “argument” subjective (and therefore false for you, but true for me) you agree with my overall claim Q.E.D.
No, the real beauty of subjectivity is that it allows me to disagree at any level. And I disagree with you on your point above, invoking the full power of subjectivity.
In fact, let me do 100% subjectivity on the whole set of comments here, and declare all your statements false for me.
(Also, the above is proof by cases. And step B/C's conclusions alone don't go out to the outer level alone as you seem to assume. You have to combine them both).
Now, I should be getting paid for doing a logic 101 in the comments ;)
The more of my comments you declare false - the more evidence you are providing in support of relativism. It is a peculiar way to agree to my point (via disagreement).
Is that what you call “logic”?
It looked like you were making up the interpretation as you go along…
I agree that it is this way, but does it have to be? Is it physically necessary to perceive defection from this dilemma as "pedantic" (see below, how surprising!), or might it only be culturally necessary?
Take your claim for example: you are not distinguishing between logic itself and our experience of logic. You are objectively correct that there is in fact no distinction on one level (experience), but that is not the only level that exists.
How are questions of this nature (essentially: existence) answered in the physical realm, where we have high levels of skill and experience?
Here's an elaboration of the point: https://news.ycombinator.com/item?id=37341439
Huh? How? Truth is an empirical fact, you can't possibly define it into existence.
You can argue that the is no Truth is mathematics, which is a perfectly reasonable position to take.
>> 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?
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.
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
And here, for a bit more context:
https://m-cacm.acm.org/magazines/2021/7/253448-program-verif...
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.
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?
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.
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.
https://dl.acm.org/doi/10.1145/321250.321253
A text that I recommend to anyone intersted in automated theorem proving, and proofs in general.
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.
---
[1] https://www.ams.org/notices/200811/tx081101395p.pdf [2] https://link.springer.com/referenceworkentry/10.1007/978-3-0... [3] https://monks.scranton.edu/files/courses/Math299/math-299-le...
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.
That's the fundamental problem. We're building the machines to verify an internally consistent idea that we're all pretty pleased with. For example, type systems don't tell you that your data is true or correct, they just provide a framework of assumptions to work from that turn out to be really useful. Each type system will provide a different view on your data/process/etc.
The University of Chicago has a special math class format called Inquiry-Based Learning designed around this idea, where you work together in class to put proofs together and work out a shared understanding of what is sufficient. I didn't take it but I wish I had. You can read some people's experiences with it here[0].
[0]: https://www.reddit.com/r/uchicago/comments/i1id9e/what_was_y...
I thought it was an interesting perspective.
[0] https://jdh.hamkins.org/book-review-catarina-dutilh-novaes-t...
But similarly, it makes sense that, even if a result is is "true" in a universal, objective sense, if the mathematician cannot communicate this in a convincing fashion to the rest of the mathematics world, I don't think we can call that result "proved".
These presumed facts have helped us do things like go to the moon and build skyscrapers, but then someone comes along with the old "but how do you actually know" argument of a college freshman, and then we get into a conversation about the potential social relativism of math.
All the while, people will see a half-assed psychology study with a questionable procedure, weak at best, erroneous at worst statistics and therefore tenuous at best conclusions, and this study is taken to be "true" and might legitimately impact notable institutions. Yet when we're talking about extremely complicated topics that exist on the edge of the horizon of human intuition, no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them.
Foundational fields like mathematics and physics are as objective as we can get. If you don't accept that, your belief about what is objectively true ends at cogito ergo sum and that's that. This has always been such a pointless conversation in my mind.
The people who eventually accept and internalize the distinction around things that can be objectively shown to be true are those who by in the large have done some of the work to understand these things themselves. Godel's Incompleteness Theorem is beautiful but it takes work to understand and if it didn't, it wouldn't be much of a meaningful breakthrough. Nobody is proving that 3+5=8 and then 4+5=9.
So what the average person sees is a high level language they can't speak with people being absolutely positive that this thing is special and true and incontrovertible. That raises red flags when you're dealing with folks talking about normal everyday stuff, doesn't it? It's a lot harder to say "but I don't understand" and a lot easier to say "but what if you're wrong" socially.
[1] As all college first years do, right? [2] Let's face it, lying to people is never impossible, it's just harder to be successful when you can be fact checked.
This is a pretty bold claim and you would have to do a bit of work to make it more convincing. Besides, it's not really how science works. Different theories wax and wane over time all the time. What we're really doing with science is coming up with ever better models that give us greater predictive power.
You could argue that at the macro scale we're asymptotically approaching some kind of objective truth with the whole endeavor of science, but you can't simply tunnel across that gap and make the leap to say that we know there is an objective truth.
The best that we can do is probably say something along the lines of "these are the best methods of getting closer to the truth that we have available - if anyone claims to have better methods, they are very likely wrong", but you still need to have the humility to accept that even the best models that we have to date are not infallible. They do not give us the objective truth, nor do they promise to, but they are the most effective tools that we have available to us at the current time. This is critically not the same as claiming that they give us the objective truth.
You could say that for all intents and purposes/everyday usage, "sure, these are objective facts about reality" - but I don't actually think that helps anyone and it serves to foment mistrust towards science and scientists. I think the best chance we have at preserving the status of science and scientists in our society starts by being honest about what it actually is giving us - which is quite a lot, but let's not oversell it for the sake of convience or whatever.
On that account, do you lean more towards flat earth theory?
No, flat earth "theory", if you can call it that, has close to zero supporting evidence and AFAIK has no actual predictive power. Stick with consensus science if you want actually useful theories, but that is very different from claiming they are giving you objective truth.
Let me ask you this, when a theory that was previously accepted as consensus science loses support in light of new evidence and gets supplanted by a new and better theory, does that mean that the objective truth changed?
You reject objective facts but respond with a claim about objectivity.
E: I should mention that it's not just a binary yes or no here, there is a 3rd option of "I don't know" and I would rabidly defend the "I don't know" camp until someone can convincingly argue one way or the other. All of this has nothing to do with the actual usefulness of science which is unquestionable in my opinion.
This is strictly talking about science "overreaching" into the philosophical realm if you will, where even from the start, methodologically it doesn't have the right tools to answer these questions. You don't prove scientific theories "true", you just accumulate more and more supporting evidence. It never hits a magical moment where the neon lights turn on and a sign says "Your theory is now true! Congratulations!". And even if it did, it would be fleeting anyway because there are no sacred cows here - your theory can just as easily get supplanted by a better theory in light of more evidence.
That's a neat trick(s)! ;)
[1] The context, or set and setting, makes a big difference in how they will behave. But the range of behavior is actually pretty simple, far simpler than much of the programming problems we breeze through on a daily basis, without even thinking twice about it. I'd say the problem isn't so much that it's hard, it's more so that it is highly counterintuitive, a lot like Einstein's relativity when first encountered (or even after understood).
And the mode -- we invented it as it is because of a whim of history, because it is a game, and we like the game, and it's useful for us. But as far as facts go, Nietzsche summed it up the most concisely: "there are no facts, only interpretations."
Yes, but is mathematics like that? Is it even science?
> The best that we can do is probably say something along the lines of "these are the best methods of getting closer to the truth that we have available - if anyone claims to have better methods, they are very likely wrong", but you still need to have the humility to accept that even the best models that we have to date are not infallible.
This last sentence slightly conflates the scientific method with the models they produce. I am not claiming that the models are "true", I am claiming that the scientific method is the only reasonable means of gaining a reliable understanding of the objective nature of reality, assuming it exists; and that you cannot pick and choose what you believe in based on your intuition.
Quantum principles have been proven in experiments that have as tight a margin of error as measuring the width of the United States to one human hair, producing shockingly consistent and effective models that were absolutely critical to the development of modern technology. Yet some people somehow refuse to accept these models as an "accurate" reflection of reality, whereas they'll take, at face value, psych/sociological/economic studies that are frankly nothing short of pathetic in comparison.
In regards to science, I am saying that there is a hierarchy of belief. You can draw the line wherever you like in terms of what you think is "true", but you cannot reorder this hierarchy and believe these sorts of psych studies while at the same time questioning the physical models that power the technology that is used to publish them.
And this isn't speaking about math, which is a particularly special case given that it is not scientific but still produces shockingly effective results.
This is basically what I'm arguing - no matter how accurately our theories line up with observation, we can never be sure that we have reached "the final theory" AKA the truth. I think this is where a lot of misunderstanding and mistrust for science originates. It will never deliver to us the truth - if it did, how would we ever know?
It is a method of getting closer and closer to what we believe is the truth. But there is still a gap there, however small it might be in the case of quantum mechanics. The scientific method by it's very construction is unable to bridge that gap.
Still, to date there does not exist a more effective method we know of as a species at getting closer to what we believe to be the truth. I think the above is a maybe subtle distinction there that is worth pointing out and educating people on. Just sort of making that distinction between the process and the results. That it is the best process we have, but even so, it cannot cross that gap and definitively say "this is the truth". That that is a gap we have to choose whether to cross ourselves with a leap of faith (or sometimes a very tiny hop of faith in the case of quantum mechanics). I think that might help people cement their faith in the process even if they dont necessarily place their faith in the results (in the case of questionable psych studies for example).
...
> Yet when we're talking about extremely complicated topics that exist on the edge of the horizon of human intuition, no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them.
I think the intersection of these two groups is the null set.
> Foundational fields like mathematics and physics are as objective as we can get.
Objective? Yes. But objective does not equate to "true"[1]. One requires data, and the other lives only in the mind. It is not at all problematic to ponder over whether mathematics is "true" - most mathematicians have an opinion one way or another, and they are not unanimous in their opinions.
[1] True w.r.t reality, not true in the logic sense.
It often describes the fundamental truth, because much of its origins was for that purpose, not because all mathematics is fundamentally true.
There's plenty of mathematics that is not modeled by the measurable world - almost by design. Just pick a different set of axioms and you'll get mathematical truths that may conflict with reality.
According to many mathematicians, uncountable infinities don't exist, and they focus on doing math without relying on them. There goes the real number line. From a scientist's perspective, either they exist or they don't. Both cannot be true. From a mathematician's perspective, both are truths.
Similarly, either the Axiom of Choice is true or it isn't. Yet the bulk of mathematics is fine with or without it.
Such as?
> "but how do you actually know" argument of a college freshman
Epistemology has been studied by some of the greatest thinkers since the ancient greeks ( probably even before ) and not just college freshmen.
> no matter how obvious the impact some people just refuse to accept things as objective simply because they fail to intuitively understand them.
If you have to intuitively understand them, it isn't very objective is it?
> Foundational fields like mathematics and physics are as objective as we can get.
What in math are objective facts about the nature of reality? Where in nature is the number 1? Also do you realize that many mathematicians don't even accept the 'reality' of real numbers.
I think as you think more deeply about these topics, you will change your tune.
They were talking about things that you don't have to (and indeed can't) intuitively understand.
> What in math are objective facts about the nature of reality? Where in nature is the number 1?
In all sorts of places, not least counting things. Mathematics is about equivalences; the point of saying 2 + 2 = 4 isn't to make some funny marks on paper or pray to the platonic void, it's to say that if you have something that's 2-like and combine it with something that's 2-like in a way that's +-like, then the result will be =-like to something 4-like, in the same sense of "like".
He was talking about objective things that people fail to to intuitively understand.
> In all sorts of places, not least counting things.
So where? Just one. Give me where 1 exists so I can check it out.
> Mathematics is about equivalences;
No. Mathematics is about theorem generation. Going from axioms to theorems via proofs. Though some go from theorems to find axioms.
> it's to say that if you have something that's 2-like and combine it with something that's 2-like in a way that's +-like, then the result will be =-like to something 4-like, in the same sense of "like".
What you are describing is just arithmetic. That's the interpretation or model for one particular set of axioms, theorems, etc. What's objective about 2-like? Feels abstract.
Funny I asked a simple question and yet you rambled on about nonsense you don't even understand.
Like I said, multiple objects objectively exist in nature.
> What you are describing is just arithmetic. That's the interpretation or model for one particular set of axioms, theorems, etc.
That the theorems are true under those axioms is an objective fact.
> Funny I asked a simple question and yet you rambled on about nonsense you don't even understand.
As the great philosophers say, no U.
I'm not specifying them, I'm referencing their existence. You can take them not to exist, but in that case good luck explaining the measurable consistency that every human on earth observes. In fact, if you truly believed this, there would be no point in even speaking leaving a comment because then you could not believe in the ability of language to communicate ideas or even in the existence of language itself.
> Epistemology has been studied by some of the greatest thinkers since the ancient greeks ( probably even before ) and not just college freshmen.
Yes but it is somehow seems to always be the college freshman that raise this question for fields that have contributed the most to humanity like mathematics and physics, all the while not feeling the need to question any number of academic fields built on an absolutely pathetic scientific process in comparison. It is simply because of their failure of intuition and understanding of mathematics and physics that they raise these questions - I'm not saying that these questions are not part of a worthwhile conversation in general.
> If you have to intuitively understand them, it isn't very objective is it?
I'm not understanding your argument here. The failure of a human mind to understand something does not mean that this thing is not objective. Nobody on Earth understood why lightning occurs for most of human history. This does not mean that the existence of lightning and the reasons for its occurrence are not objective qualities of nature.
> What in math are objective facts about the nature of reality?
The existence of concepts that map to reality in producing models that yield consistent, effective, and measurable results.
If there were no conscious beings, the Earth would continue its orbit around the sun and this order is what is captured by the human-invented language of mathematics. Saying that "mathematics" isn't objective may be true depending on how you define mathematics, but there is no denying that there are objective relationships which exist beyond human experience. If you deny this, you are left with cogito ergo sum which was my original argument.
Indeed, mathematics and any other STEM field is deeply political. People are politics. But to confuse that--that STEM as practiced is socially constructed and political--and to make a sloppy ontological conclusion about what STEM/math is, is a deeply neoliberalizing argument. So I'm inclined to make the argument that it is actually the neoliberal intellectuals who try to spin this as fundamentally only a human enterprise, because it privileges their social standing as the "correct" practitioners of this compact: capitalism requires that mathematicians be able to "sell" each other the truth of their proofs.
Indeed, the article mentions the Mochizuki controversy but I don't think they understood the social problem. See, it doesn't matter if Mochizuki is right or wrong, or if people understood his 500 pages or not. It is that in principle it could be shown that he is right or wrong. And that's unlike, say, the Bible, which is also a social compact. Reduction of STEM to social construct throws the baby out with the bathwater.
Hard sciences are the same, yes?
Water is two parts hydrogen, one part oxygen.
If you study a broad range of subjects, you'd realize in mathematics the level of convergence is quite high relative to the other subjects, even the "hard" sciences. I wouldn't say it's 100% though.
E.g. Axiom of Choice, ZFC, constructivism.
1 + 2 + 3 + 4 + ... = -1/12 [1]
[1] https://media.tenor.com/Mbl5heTtzDoAAAAC/obi-wan-kenobi-cert...
Math kind of lost me at the uncountable sets. Given the results from Gödel, the justification of law of excluded middle really needs a serious reconsideration.
But that's why I'm not a mathematician. (I suspect this aspect of self-selection facilitates convergence, but I don't see why it wouldn't apply to almost all fields of study)
No. See Brouwer–Hilbert controversy.
They can't even agree on what makes mathematical logics.
> Some terrific developments have happened with proof verification. Like [the proof assistant] Lean, which has allowed mathematicians to verify many proofs, while also helping the authors better understand their own work, because they have to break down some of their ideas into simpler steps to feed into Lean for verification. […] I’m not saying that I believe something like Lean is going to make a lot of errors. […] They can be a very valuable tool for getting things right — particularly for verifying mathematics that rests heavily on new definitions that are not easy to analyze at first sight. There’s no debate that it’s helpful to have new perspectives, new tools and new technology in our armory.
In between (the "[…]"s above), he says:
> But is this foolproof? Is a proof a proof just because Lean agrees it’s one? In some ways, it’s as good as the people who convert the proof into inputs for Lean. Which sounds very much like how we do traditional mathematics. […] I’m just not sure it’s any more secure than most things done by humans. […] I’m afraid I have a lot of skepticism about the role of computers. […] what I shy away from is the concept that we’re now going to have perfect logical machines that produce correct theorems. You have to acknowledge that we can’t be sure things are correct with computers. Our future has to rely on the sense of community that we have relied on throughout the history of science: that we bounce things off one another. That we talk to people who look at the same thing from a completely different perspective. And so on.
The latter part is less about the correctness and more about community: the main goal of mathematics is not merely a "true" theorems, but (human) mathematical understanding. I wrote an answer about this on math.SE in 2014 (mostly quoting Thurston and Rota): https://math.stackexchange.com/questions/632705/why-are-math...
But when he says that he doesn't believe that a proof in Lean is "more secure than most things done by humans" I fundamentally disagree.
But yes, I wouldn't want computer proofs to "replace" the proofs we have now.
That, or an error in the specification (ie.: not the implementation).
(I very much am with you that his attitude / way of framing it is a bit weird)
Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics.
(I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).
I originally picked up the book because I was trying to understand Euler's polyhedral formula better -- which in retrospect is kind of like reading Zen and the Art of Motorcycle Maintenance because you wanted to fix a motorcycle.
I'm not wired for pure math -- I loved real analysis then quit while I was ahead. Still it's fun to pretend sometimes, and Lakatos does a great job of making you feel like you're learning inside knowledge about what mathematicians do. He introduces fun concepts like "monster-barring" (the way people sometimes carve out special cases in a proof when they encounter counterexamples).
I've never made it the whole way through, but I like to go back every few months and absorb a little more.
edit to add: I just now skimmed the author's Wikipedia entry and the Stanford Encyclopedia of Philosophy's story about the author's interaction with someone named Éva Izsák and I have a ton of questions.
I hope this isn't too far off topic, but can someone clarify exactly how this problem indicts axioms? As an uninformed and naive musing, it occurs to me that an issue with the statement "this statement is false" is this. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components.
Unfortunately, what Gödel showed is that any logical system that is strong enough to capture addition and multiplication over natural numbers - and nothing more - includes self-referentiality.
That includes the language of arithmetic - you can write down formulas that refer to themselves - and Turing machines (via the recursion theorem, any Turing Machine is equivalent to a machine that knows its own source code). The constructions are a bit technical, but it's possible.
Of course once you get into Turing machines it all flows more naturally, what with all of us being accustomed to "code is just data".
You can write down "P is provable" as a first-order sentence of arithmetic (which involves some number theoretic tricks), and you can also do the diagonalisation trick that gives you self-referentiality. That's really all you need.
As for this particular issue I think this wikipedia page is relevant: https://en.wikipedia.org/wiki/Impredicativity
An alternative approach is purely syntactic and sees a logical system as collection of valid transformation rules that can be applied to the axioms. In this view, a sentence is true if it can be obtained from the axioms by applying a sequence of valid transformation rules. This purely syntactic notion of truth is known as “provability”.
Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide.
It's even more subtle than that. They do coincide in a sense, which is proven by Gödel's completeness theorem (well, at least in First-Order Logic). That one just says that a sentence is provable from some axioms exactly iff it's true in every interpretation that satisfy the axioms.
So one thing that Gödel's first incompleteness theorem shows it's that it's impossible to uniquely characterise even a simple structure such as the natural numbers by some "reasonable"[0] axioms - precisely because there will always be sentences that are correct in some interpretations but not in others.
Unless you use second-order logic - in which case the whole enterprise breaks down for different reasons (because completeness doesn't hold for second order logic).
[0] reasonable basically means that it must be possible to verify whether a sentence is an axiom or not, otherwise you could just say that "every true sentence is an axiom"
There, the obstacle is in some sense of a simplest nature: if your set of axioms admits a countable model, then it admits models of all infinite cardinalities. In other words, it shows that there is something fundamentally impossible in trying to capture an infinite structure (like numbers) by finite means (e.g. recursively axiomatizable).
Let me just point out for other readers that Löwenheim-Skolem applies to ANY first order theory (in a countable language, or also in an uncountable language if stated in the form that a theory with an infinite model with cardinality at least that of the language has infinite models in all cardinalities at least as big as that of the language), it doesn't care about how complex the axioms are from a computability point of view
You can't capture an infinite structure fully by "finitary" methods, either you use FOL and then you run into L-S, or you use higher-order logic (for which L-S doesn't apply) but then you don't have a complete proof system anymore.
To tie it all together, L-S and incompleteness are about different flavours of "not being able to capture something". L-S is about models of different cardinalities. These models do still all satisfy exactly the same sentences. Incompleteness is about different models actually satisfying different sentences.
He's alluding to the fact that unlike what one might naively intuit, it's impossible to formulate a set of axioms that can formally express all mathematics.
Because of Godel's incompleteness theorems, any formal system that's sufficiently powerful to formulate basic arithmetic (see for instance Robinson arithmetic) and consistent (that is, it cannot prove false statements) is both incomplete (meaning that it's possible to formulate a wff within that system that the system itself can neither prove nor disprove) and can't prove it's own consistency.
This fact is often portrayed in popular media as being a "bug" or a "missing foundation" of mathematics. That is inaccurate -- it's just a property of how logical systems work -- but it does prove that the search for the holy grail of a grand unified system of axioms for all of mathematics is destined to remain fruitless.
Modern mathematics is most often implicitly assumed to be formulated in a formal system called ZFC, but there are alternatives.
Hilbert wanted to show that, even if you don't "believe" in ZFC, we could at least try to convince you that it doesn't lead to contradictions, but that fundamentally didn't work.
It makes sense, Godel's first could be mostly seen as a version of the halting problem, while the second is "game over" for a Hilbert-like foundation program.
p.s. Just wanted to point out that it's funny how we wrote two mostly identical sets of comments. Great minds think alike? :)
That's the characterisation I got from Peter Smith's book about Gödel's theorems. I didn't verify original sources or anything, but it sounds very plausible to me.
And it also kind of answers the question about why we should care: if a system can't prove its own consistency, well that's not terribly interesting (even if it could, we would have to believe the system a priori to trust its own consistency proof). But if it also can't prove a stronger system consistent, then that's much more interesting.
> Great minds think alike?
That would be a bit too self-aggrandizing for me. :D I'm very curious about logic (and maths in general), that's why I know some stuff about it, but I'm no maths genius.
When you say "you can keep consistency or completeness but not both" you are essentially stating Godel's first.
Morally speaking, Godel's first is "no system is complete", but there are two exceptions: if the system isn't powerful enough to formulate the Godel sentence then the proof doesn't work, and any inconsistent system is trivially complete because ex falso quodlibet sequitur, i.e. any wff is true.
The part about a system not being able to prove its own consistency is Godel's second theorem.
But the theorem only does what it says on the tin: the system not being able to prove its own consistency doesn't mean that it being inconsistent! [1] This is the case for ZFC, for example. We can't prove ZFC's consistency within ZFC: that would violate Godel's second, and we know that either ZFC is inconsistent (that is, you can derive an absurd from the axioms) or ZFC is incomplete (that is, there exists a well-formed formula of ZFC that cannot be proved or disproved within ZFC).
We don't know which one it is.
[1] This implication and similar ones are often made in pop-culture presentations of the foundation problem. I generally vigorously object to them because they're not only imprecise -- that's understandable -- but they leave a layman with a completely wrong impression.
Another funny thing that can happen is that a system proves its own inconsistency, despite being consistent. The short summary is to never trust a system talking about its own consistency.
To mathematicians and non-mathematicians.
Being unable to prove or disprove certain statements is a rainy cloud. Like maybe the Riemann hypothesis is just impossible to prove.
It doesn't mean math is "broken" but it is disappointing, no?
This being said, your intuition is absolutely correct, the crux of the issue is with ‘this‘. What mathematicians realized is that if you are not careful with your choice of axioms, the resulting logical system becomes too “powerful” in the sense that it becomes self-referential: you can construct sentences that refer to themselves in a self-defeating manner.
As others have mentioned, this is the idea underlying Gödel's incompleteness theorem but also, to some extent, Russel's paradox that came before and is what the article is referring to. In Russel's paradox, the contradiction comes from constructing the set of all sets that contain themselves.
E.g. why did we care about the parallel postulate? Why not just have geometry without a fith axiom? Well, because without it the axioms are, well, incomplete: there are statements in the language of geometry that cannot be proven from the other four axioms. You can have spherical geometry, planar geometry, and projective geometry, and they all conform to the first four axioms, but sometimes one of these geometrical statements will be true in one and false in another. So neither is "the" geometry, it matters which specific version of geometry you work in, and we need that fifth axiom to have a complete theory of (planar) geometry.
We'd hope to avoid that kind of situation with the natural numbers - if we need any additional "parallel postulate", we'd like to know about it, and if we don't, we'd like to be able to prove that we don't need one rather than just assuming it because we haven't stumbled across it yet. But Goedel proved that we cannot have a provably complete theory of the natural numbers with addition and multiplication, because he found a way to encode a statement akin to "this statement is false" in the language of the natural numbers. Which indicts any axiomatization of arithmetic - either your axiomatization proves this statement is true (in which case it's inconsistent), it proves this statement is false (in which case it's also inconsistent), or it doesn't prove this statement one way or another (in which case it's incomplete).
> As an uninformed and naive musing, it occurs to me that an issue with the statement "this statement is false" is this. The whole of the statement, that is, the thing having truth or falsehood, cannot be addressed by one of its components.
Well, yes, getting around that is the clever part of Goedel's proof :).
There are also extensions to these (eg. presburger extended to multiplication by constants) that are also known to be complete and consistent.
These systems do not require any social compact. Any theorems proven through them are absolute truth, although the the range of statements that these systems can express is limited.
One may require a social compact for Peano, ZFC, and such other powerful formal systems.
That the software implementations like Coq and Lean are bug free may also require a social compact, if the nature of being bug free cannot be formally proved, although it seems determining this should be an easier problem.
So meaning is about correspondences, but also about achieving goals. We communicate for many reasons, maybe in this case to help us understand problems better. The weather simulation helps us plan activities. The Roomba’s map helps it clean the room. So there’s also an element of intentionality.
What is the intention behind these mathematical proofs? What are their correspondences to other information and goals?
[*] Note that the claim is "many" (ie.: a subset), not "all".
This is not AI.
Combining Theorem Provers with AI is promising:
I also haven't watched this video, but I'm linking it because I can't find an earlier one where she points out that the basis of logic is in rhetoric.
It would be great if mathematics was widely presented and taught in this messy, practical, human, truthful way rather than the purist, mystical, mythical manner.
Calculus wasn't "discovered", it was painstakingly developed by some blokes that were trying to solve physical problems.
Is incorrect proof still a "proof", just one which is incorrect?
If Curry-Howard holds then programs are "proofs". To write a proof is to write a program.
But what about a program that has a bug in it? We say it is an incorrect program. But we still call it a program. By the same logic an incorrect proof is still a "proof" as well.
And typically it is a proof - of something. Every formally valid proof proves SOMETHING, right?
Instead of asking "Is this proof correct?" we should ask: "Does this proof prove what we claim it proves, or something else"?
It reminds me of my old days in high-school when I was intrigued by unconventional ways of doing maths, I often had the habit of mixing many different domains into one derivation (which often led to people interpreting it as nonsense). I realize that even if I were "right", whether it is or not is dependent on a subjective, mutual, and shared convention.
A "social construct" is quite different, that's something entirely constructed by society, like manners or nationalism.
Here is Daniel Dennett talking it. https://youtu.be/32u12zjgJww
I like the no miracles argument in favour of science. If our scientific theories don't track reality, how are they successful in prediction the future.
Similarly the social aspect of mathematical proofs can be replaced with requirements like being in congruence with established facts (i.e explanatory power), predictive power, and efficient representation (i.e. elegant compression) which means faster programs / less computational steps required.
DeMillo, Lipton, Perlis
Social Processes and Proofs of Theorems and Programs
It's odd that the article doesn't spell out Zermelo–Fraenkel, and instead uses the shorthand ZFC axioms. At a fundamental level, axioms are simultaneously solid and slippery. The entire purpose of a set of axioms is to serve as a backstop. Without axioms there are no proofs, and instead you wind up riding infinite regress; turtles all the way down. In short, proofs without axioms are impossible.
But once you have a set of axioms, proofs are precisely that, proofs. The notion that mathematics is a social compact is aggrandizing the role of the axiom, and minimizing the rest of mathematics. It is certainly the case that axioms are in fact a "social compact" in the sense that if we cannot agree that a set of given axioms are true without proof, then we can prove nothing. But the goal of axioms is to make that compact as narrow and clear as possible.
The brief discussion of Godel's incompleteness theorem elides the fundamental nuance that incompleteness has only been demonstrated in the context of self reference. There is a longer and better discussion of how this relates to logic, science, and consciousness in Hofstadter's seminal work "Godel, Escher, Bach"
https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...
I'm not a math person but this Shinichi Mochizuki sounds like a hack job.
> In fact, the reason he got any attention at all is because of his initial record of nonbullshit
Sure, if he didn't have a reputation to burn he would be dismissed a priori as a crank. No one should have the time to parse and debunk random 500-page manifestos.
My issue with pure math is that, for any given (sub)*field, there are at best a handful of experts, and the probability of that small clique of experts being willing to spend time debunking/criticizing each other is low. Quid-pro-quo back-scratching has far better payout. We have an environment with low accountability, but also low stakes.
Basically, my position is that pure math is chock full of arcane nonsense (bullshit is admittedly a strong term that implies bad faith). But, it also doesn't cause harm, so it's not a big deal. Still, it behooves anyone entering or established in mathematics to understand the reality of the game. You will deal with charlatans and it's acceptable if your own work isn't perfect or even remotely correct or applicable.