News for hackers. Stuff that matters.
Re:Gödel, Escher, Bach: an in-depth explainer by mreid on Tuesday September 13, 2022 @06:40PM (#32831095)
It might be easiest to give a sense of what "unprovable but true" means by way of an imagined example.

Goldbach's conjecture is that "every even number bigger than 2 is the sum of exactly two prime numbers", so 4 = 2 + 2, 6 = 3 + 3, 8 = 5 + 3, etc.

For this statement to be *true* it just means that every even number there must exist two primes that add to that number. This is a statement about infinitely many integers.

A *proof* of Goldbach's conjecture consists of a finite number of formal reasoning steps that start with some axioms and end up at the statement of the result.

To this day, it seems as though Goldbach's conjecture is true. It holds for every number we've been able to test. However, no one has proved it is true or false yet (or proved that it is unprovable).

The proof of Gödel's result's involves very carefully formalizing what statements and proofs mean so that they can be encoded as statements about arithmetic. He then shows there is a statement with encoding G that says "The statement with encoding G cannot be proved" – if it is true, then it cannot be proved.

It's kind of confusing at first, but there is an easier way to get an intuition why there might be true statements that cannot be proved. Think of each statement about the natural numbers as a subset where each number in the subset makes the statement true. There are uncountably many subsets of the natural numbers (by Cantor's diagonalization argument). Proofs are finite chains of finite statements so there are only countably infinitely many of these. Therefore there must be subsets/statements that are true that do not have a matching proof.

The approach that Gödel's proof takes is not too different to the above argument – it is essentially a diagonalization argument – the complexity is in making the encoding of statements are numbers very precise.

Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Tuesday September 13, 2022 @09:46PM (#32832353)
I’ve only ever seen examples like the one you give here, which seem like trite, trivial, and uninteresting middle-school level logical gotchas. Are there actually interesting properties which are true but can’t be proven? Or is it just a statement about self-referential recursive logic being unprovable?
Re:Gödel, Escher, Bach: an in-depth explainer by memetomancer on Tuesday September 13, 2022 @11:29PM (#32833033)
Interesting take. You have casually dismissed the Goldbach Conjecture (perhaps the deepest centuries old problem in number theory) as 'trite, trivial and uninteresting'... Suggesting that you are only minimally familiar with the issue... then toss about an inapplicable phrase 'self-referential recursive logic' as if you are deeply immersed in such matters, perhaps even _much_ smarter than the thousands of mathematicians (including the likes of Euler) that have applied themselves to this problem. An odd contradiction!

I do believe this opinion places you very high on the 'confidence' axis, but not especially far along the 'competence' axis.

Re:Gödel, Escher, Bach: an in-depth explainer by wikfwikf on Wednesday September 14, 2022 @05:44AM (#32835004)
The Goldbach conjecture is of very little interest to mathematicians, unlike either Fermat's Last Theorem or the Riemann Hypothesis. Statistically it is clearly true, in the sense that there are way more prime numbers than you would need for it to be true. Finding a counterexample would be interesting in the sense that it would be very surprising (but not mathematically interesting).

It is fated to be proved as a trivial corollary to some more important mathematics; a corollary that no one would have bothered with if not for the historical importance.

The unsolved Twin Prime Conjecture, of roughly the same age, is expected to lead to much more interesting mathematics if it is proved.

Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Wednesday September 14, 2022 @01:21AM (#32833591)
I was talking about Gödel, not Goldbach:

> The proof of Gödel's result's involves very carefully formalizing what statements and proofs mean so that they can be encoded as statements about arithmetic. He then shows there is a statement with encoding G that says "The statement with encoding G cannot be proved" – if it is true, then it cannot be proved.

Sorry I meant to quote this bit at the beginning of my comment. Parent comment which I was replying to talks about both.

Re:Gödel, Escher, Bach: an in-depth explainer by dudeguy3301 on Wednesday September 14, 2022 @03:24AM (#32834245)
wait, so you are casually dismissing Gödel's work as a logical "gotcha"? don't premise opinions about complex proofs on other peoples woefully impoverished and misrepresented explanations of said proofs

that is disrespectful and very very very short sighted.

also, go read up (...on Gödel, Cantor, Turing, Tarski, etc...)

Re:Gödel, Escher, Bach: an in-depth explainer by gsinclair on Wednesday September 14, 2022 @06:53AM (#32835415)
I understand precisely what adastra22 meant from the moment I read it. Unfortunately two people now have rushed to unkind characteristics of what that (perfectly sensible) meaning was.
Re:Gödel, Escher, Bach: an in-depth explainer by dudeguy3301 on Wednesday September 14, 2022 @12:22PM (#32839426)
sure, what was written was sensible but has no bearing on the proof. speculation isn't critical thinking, as adastra22 says, be careful to what you are responding to. my point is the lack of rigor and understanding because the proof isnt being discussed, hand waving about an unread and very important mathematical work is irresponsible. thats MY point
Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Wednesday September 14, 2022 @07:56AM (#32835907)
Please try to give the people you talk to the benefit of the doubt, and read carefully what you are responding to.

My training is as an applied physicist. We physicists have an interesting relationship with math. Obviously math is essential to the work that we do, but the physical world decides whether the math is right, not the other way around. Our mathematical models technically permit things like negative mass, time flowing backwards, or magnetic monopoles. But that doesn't mean tachyons, time machines, or fundamental magnetic particles exist--they don't, so far as we know. So I'm trained to actively disregard non-physical, not relevant mathematical implications. I'm sorry if this offends a pure mathematicians sensibilities, but pragmatically it is very useful.

Or take a different field: in computational semantics, a branch of formal linguistics, there are many models for inferring a formal logical statement from an example written sentence or spoken utterance, and then determining the validity (truth) of the statement. These models get caught up on stuff like "This sentence is false." What's the truth value for that sentence? If it is true then it must be false, and if it is false then it must be true. Error, validity of this statement can't be determined! But hey, it turns out that in practice this basically never happens unless the speaker is really confused, misspeaks, or deliberately evasive. Real sentences don't have this self-referential, circular logic structure because that's not how people think or communicate.

Now "this sentence is false" goes back to the greeks, IIRC, and Gödel's theorem is slightly different. Gödel's main work is in the formalization of proofs and proof systems, and I don't want to take away from that in any way. But the incompleteness theorem always seems to be explained through these sorts of self-referential examples and I have yet to ever see it reduced to a practical problem with real-world implications. Hence my question. Does Gödel's incompleteness theorem actually constrain a real world application of proof systems, where we tend to be interested in non-cyclical logical arguments?

Re:Gödel, Escher, Bach: an in-depth explainer by thrwycct123 on Wednesday September 14, 2022 @01:53PM (#32840734)
> Obviously math is essential to the work that we do, but the physical world decides whether the math is right, not the other way arounnd

That was the belief before the 1800s. But with the discovery of non-euclidean geometry, math has been divorced from the physical world. Math is simply a system of axioms and proofs. Math is purely abstract and logical. Whatever math that physicists use just simply happens to align with the physical world.

Also, the physical world doesn't confirm whether the math is "right". Math is deductive, not inductive. As long as the math is derivable from the axioms, it is right. The physical world/experiments determine whether the mathematical model aligns with the physical world. The physical world has no say in math. Not anymore.

> So I'm trained to actively disregard non-physical, not relevant mathematical implications.

In the past, when a mathematical model predicted something ( relativity to quantum physics to elements ), experiments were conducted to determine whether the models aligned with the physical world. If the mathematical models make predictions that physicists currently can't verify with experiments, should we disregard it? Do we need technology to advance to where we can conduct experiments. Do we need physics to become more abstract? Perhaps model the physical world in the virtual world. Would experiments in the virtual world be applicable to physics? Seems like physics is both at a dead-end and on the cusp of a revolution.

Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Wednesday September 14, 2022 @05:27PM (#32843615)
The question “does this have relevant applications?” Is still well formed and answerable. That’s all I’m asking! I find it odd that so many are taking offense.
Re:Gödel, Escher, Bach: an in-depth explainer by randomswede on Friday September 16, 2022 @02:01AM (#32862621)
If your question is "does Gödel Incompleteness have practical applications", my answer is "probably". Not necessarily directly, but indirectly it has inspired much other work.

One of the things it inspired was Turing's work on uncomputable numbers. It turns out that computability and incompleteness are intertwined, which at least I find interesting. And without the "uncomputable numbers" malarkey, I wonder if the Turing Machine formalism would exist (answer, "probably, but maybe looking different and with another name"). And, well, the Halting Problem is essentially Gödel Incompleteness (imagine handwaving here).

As for proof systems, again, the answer is "probably". Knowing that there are true, unprovable, statements in a formalism is something that informs how you approach it, you need to put a limit on how far to go before you say "I don't know" and taht is in and of itself important.

Re:Gödel, Escher, Bach: an in-depth explainer by dudeguy3301 on Wednesday September 14, 2022 @12:13PM (#32839275)
still doesn't sound like you have ever read the proof, nor about it. so aren't you engaged in this discussion strictly by speculation? logical fallacy? just because you have some point to make has no bearing on the work you are adjacent to and not actually discussing. making your own points and arguments about logical gotchas is great, has nothing to do with critically understanding a work you haven't read. asking for giving the 'benefit of the doubt' to speculation informed only by a comment section is ridiculous. do your homework before asking for generous responses to your internet quibbling
Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Wednesday September 14, 2022 @12:17PM (#32839321)
And what did your post contribute?

Never mind then, I’m sorry I bothered.

Re:Gödel, Escher, Bach: an in-depth explainer by ColinWright on Friday September 16, 2022 @09:40AM (#32865918)
I'm late to the party, so I'm not sure you'll see this. Hope you do. Different people will each have their own contexts and their own concepts of "useful" or "interesting". I'm making assumptions about yours ... apologies if I misrepresent you.

The proof of Gödel's result uses the paradoxical statement "This statement is false", but that's being used to prove this very general result about all systems. So the hunt is then on to find "natural" statements that are True but Unprovable.

But the "unprovable" bit should more completely be stated as "unprovable in a specific axiomatic proof system". If we want to prove that statement S is "True but Unprovable" then we must actually prove that it's true. So if we've proved it's true, what does it mean to say it's unprovable? We just proved it! What's going on?

So let's take a specific example.

Peano Arithmetic (PA)[0] is an axiomatic proof system intended to capture Natural Numbers and their behaviour.

The "Goodstein Sequence" G(m) of a number m is a sequence of natural numbers ... you can find the definition here[1]. It's not hard, but it's longer than I want to reproduce here.

Goodstein's Theorem (GT) says that for every integer m greater than 0, G(m) is eventually zero.

It has been proven that GT cannot be proved in PA, but it can be proved in stronger systems, such as second-order arithmetic.

So the statement of GT is not self-referential, along the lines of "This Statement Is False" sort of thing. It's an actual statement about the behaviour of integers, so it's not a self-referential trick.

Your question now is: What's the point? How is this useful or relevant?

Much of modern (pure) mathematics is chasing things because the mathematicians find them interesting. The vast, vast majority will never, of themselves, be useful by (what I expect are) your standards.

But it was once thought that factoring integers was of no practical use, and only pursued or investigated by cranks. Imaginary Numbers were thought to be bizarre, useless, and dangerous. Non-Euclidean Geometry was thought to be utter nonsense, and held up as part of the "proof" that the fifth postulate was unnecessary and was deducible from the other four. All three of these now form critical components in modern technology.

Even more, to the average person on the street, anything to do with algebra is completely pointless.

For you, Gödel's theorem is completely pointless and useless and probably of no interest at all, but it helps us understand the limitations of formal systems. The techniques that have been developed in the time since it was proved have helped us understand more about what computer verification systems might or might not be able to accomplish.

Of itself, Gödel's theorem might not be of direct, immediate, and practical use, but the work it has inspired has tangentially been useful, and may yet be moreso.

But not for everyone. After all, some people don't care about the Mona Lisa, or Beethoven's Fifth Symphony, or Michaelangelo's David, or the fact that people have walked on the Moon, so why should people care about results in Pure Mathematics?

That's the thing about Pure Mathematics. Sometimes it ends up being useful in ways we never expected.

[0] https://en.wikipedia.org/wiki/Peano_axioms

[1] https://en.wikipedia.org/wiki/Goodstein's_theorem#Goodstein_...

Re:Gödel, Escher, Bach: an in-depth explainer by flebron on Tuesday September 13, 2022 @10:51PM (#32832763)
Well, most interesting properties about computer programs are, in general for all programs, undecidable (https://en.wikipedia.org/wiki/Rice%27s_theorem). Undecidability is a closely related notion to unprovability (https://en.wikipedia.org/wiki/Undecidable_problem#Relationsh....
Re:Gödel, Escher, Bach: an in-depth explainer by thayne on Tuesday September 13, 2022 @10:56PM (#32832795)
I don't know if it is quite what you are looking for, but with the normal mathematical axioms, it isn't possible to prove whether or not the there are any sets with a cardinality between the cardinality of the natural numbers and the cardinality of the real numbers.

But one of those two must be true, you just can't prove it. Of course you can add a new axiom that allows you to prove one or the other (or accept one of those statements as an axiom), but you will still have other statements that you can't prove.

Re:Gödel, Escher, Bach: an in-depth explainer by schoen on Wednesday September 14, 2022 @02:57AM (#32834079)
> But one of those two must be true, you just can't prove it.

Three alternative accounts:

* Both the CH and ¬CH mathematical universes really exist, so we just have to choose which one we're more interested in at a given time. Like one might say there are the "reall numbers" and the "realle numbers", both valid and interesting constructions which humanity was just slow to recognize the distinctions between (because they were initially less relevant to our interests and our day-to-day lives).

* We are actually ultimately thinking about one or the other of them, or are in some sense in one or the other mathematical universe, but we don't know enough about our intuition about the reals to be able to specify or explain which one. (Maybe we need other properties whose obviousness or relevance humanity is not smart enough to notice?)

* Some finitist or ultrafinitist approach is actually right: the real numbers are a formalism that, while reasonably motivated by historical attempts to "complete" mathematics in various ways, doesn't correspond to anything Platonically real or to anything intellectually relevant to humanity. (In this account, there is potentially no answer to the question because the real numbers don't exist at all. Neither CH nor ¬CH refers to a mathematical reality, just to games about formalisms.)

Re:Gödel, Escher, Bach: an in-depth explainer by thayne on Wednesday September 14, 2022 @03:20AM (#32834218)
sure, but if you ignore any connection to the real world or platonic truth and are just talking about within the ZFC formalism, then `CH ∨ ¬CH` is a true statement, even though it is impossible to prove either `CH` or `¬CH`.
Re:Gödel, Escher, Bach: an in-depth explainer by chriswarbo on Wednesday September 14, 2022 @07:52AM (#32835872)
> within the ZFC formalism, then `CH ∨ ¬CH` is a true statement

It's also a provable statement (via excluded middle)

Re:Gödel, Escher, Bach: an in-depth explainer by DontchaKnowit on Wednesday September 14, 2022 @12:00AM (#32833190)
This is super interesting. Was not aware of this. Is there a proof that this is not provable?
Re:Gödel, Escher, Bach: an in-depth explainer by thayne on Wednesday September 14, 2022 @01:42AM (#32833682)
Yes, Paul Cohen proved that the continuum hypothesis (that there is no set with cardinality between that of natural numbers and real numbers) was independent of the ZFC formulation of set theory (the most standard set of axioms used in today's set theory) in 1963.
Re:Gödel, Escher, Bach: an in-depth explainer by schoen on Wednesday September 14, 2022 @02:47AM (#32834015)
Re:Gödel, Escher, Bach: an in-depth explainer by gsinclair on Wednesday September 14, 2022 @06:58AM (#32835453)
My understanding is this: Gödel proved his earth shattering result in the 1930s. Then the dust settled and mathematicians thought it might be “academic” and that mathematics might not come tumbling down after all. Then in the 1960s Paul Cohen proves that the continuum hypothesis is undecidable. That is, we will never know whether an infinite set can have a cardinality between the natural numbers and the real numbers.

My understanding comes from Keith Devlin’s wonderful book “Mathematics: A new golden age”.

Re:Gödel, Escher, Bach: an in-depth explainer by butokai on Tuesday September 20, 2022 @10:40AM (#32912255)
Harvey Friedman, one of the most renowned contemporary logicians, has a research program devoted to finding such examples as those you seem to be looking for. This article presents his views: https://nautil.us/this-man-is-about-to-blow-up-mathematics-2...
Re:Gödel, Escher, Bach: an in-depth explainer by red_trumpet on Wednesday September 14, 2022 @05:16AM (#32834849)
Wikipedia has a list[1] of statements which are not provable in (or rather independent of) ZFC.

IMO the most weird thing is the following, intertwining consistency of ZFC with Diophantine equations[2]:

> One can write down a concrete polynomial p ∈ Z[x1, ..., x9] such that the statement "there are integers m1, ..., m9 with p(m1, ..., m9) = 0" can neither be proven nor disproven in ZFC (assuming ZFC is consistent). [...] the polynomial is constructed so that it has an integer root if and only if ZFC is inconsistent.

[1] https://en.wikipedia.org/wiki/List_of_statements_independent...

[2] https://en.wikipedia.org/wiki/List_of_statements_independent...

Re:Gödel, Escher, Bach: an in-depth explainer by Tainnor on Wednesday September 14, 2022 @04:21AM (#32834534)
There are examples of "natural" sentences which are unprovable in Peano Arithmetic (which is one of the simpler systems for which Gödel's theorems apply): https://en.m.wikipedia.org/wiki/Paris%E2%80%93Harrington_the...

But in general, Gödel applies to all formal systems that satisfy certain properties, it's just that the exact unprovable sentences will be different (since you may just add that sentence as an axiom) that's why the general example is very abstract. It shows that sufficiently rich theories are not only incomplete, but also incompletable.

Re:Gödel, Escher, Bach: an in-depth explainer by voldacar on Thursday September 15, 2022 @09:54PM (#32861093)
>Are there actually interesting properties which are true but can’t be proven?

Goodstein's theorem and the Paris-Harrington theorem are some examples of this for ZFC. There are several more, maybe a logician could chime in

Re:Gödel, Escher, Bach: an in-depth explainer by machina_ex_deus on Wednesday September 14, 2022 @04:37AM (#32834619)
The Continuum hypothesis is independent of ZFC. It is the first of Hilbert's 23 problems.
Re:Gödel, Escher, Bach: an in-depth explainer by wikfwikf on Wednesday September 14, 2022 @05:41AM (#32834992)
This is the best example - before it was shown that the Continuum Hypothesis was unprovable, many people believed, like the GP, that only uninteresting and artificial statements could be shown to be unprovable.

The CH is undoubtedly meaningful, natural, and of huge interest to (a subset of) mathematicians.

Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Wednesday September 14, 2022 @08:02AM (#32835976)
What are the practical applications of CH?
Re:Gödel, Escher, Bach: an in-depth explainer by SamBam on Friday September 16, 2022 @12:44PM (#32868752)
At this point I feel like you're going from a reasonable question about Godel's theorem to cranky person unwilling to see how any math that doesn't explain how to fly a 747 is relevant to the world.

There are huge branches of mathematics that don't find immediate practicality in physics. Often these end up being practical in cryptography or quantum mechanics, but sometimes they don't. But to dismiss the entire field that relates to the cardinality of real numbers as uninteresting if someone can't give you a practical application of it shows a simple disregard for other fields of study.

Re:Gödel, Escher, Bach: an in-depth explainer by wikfwikf on Wednesday September 14, 2022 @09:57AM (#32837270)
lol
Re:Gödel, Escher, Bach: an in-depth explainer by adastra22 on Wednesday September 14, 2022 @12:19PM (#32839347)
What was funny?
Re:Gödel, Escher, Bach: an in-depth explainer by red_trumpet on Wednesday September 14, 2022 @04:49AM (#32834694)
What do we actually mean by saying "statement S is unprovable"? Do we mean "there is no prove for S" (which includes the case that S is provably false), or do we mean "there is no proof for S and there is no proof for its converse"?

Because if you show that the converse of Goldbach's conjecture is not provable, you have actually proven Goldbach's conjecture (since you have shown that there is no counterexample!).

>Think of each statement about the natural numbers as a subset where each number in the subset makes the statement true. There are uncountably many subsets of the natural numbers (by Cantor's diagonalization argument).

Don't we only care about the countable set of statements that can written down in a given logical system? Say second order logic + ZFC.

Re:Gödel, Escher, Bach: an in-depth explainer by gsinclair on Wednesday September 14, 2022 @07:43AM (#32835804)
> What do we actually mean by saying "statement S is unprovable"? Do we mean "there is no [edited:] proof for S" (which includes the case that S is provably false), or do we mean "there is no proof for S and there is no proof for its converse"?

By “converse” I think you mean “negation”.

A statement being unprovable means we will never know whether it is this or false. > Because if you show that the converse of Goldbach's conjecture is not provable, you have actually proven Goldbach's conjecture (since you have shown that there is no counterexample!).

Nope: demonstrating that (the opposite of Goldbach’s conjecture) is unprovable is logically equivalent to demonstrating that (Goldbach’s conjecture) is unprovable. It means we’ll never know either way.

Re:Gödel, Escher, Bach: an in-depth explainer by trashtester on Wednesday September 14, 2022 @08:04AM (#32835988)
> Nope: demonstrating that (the opposite of Goldbach’s conjecture) is unprovable is logically equivalent to demonstrating that (Goldbach’s conjecture) is unprovable. It means we’ll never know either way.

I think this is false. If you find a number N that is not the sum of two primes, you did disprove Goldbach's conjecture. Any such number would be smaller than infinity, and so there would only be a finite set of primes smaller it to check for.

So basically, if Goldbach's conjecture turns out to be false it IS going to be PROVABLY false.

Only if Goldbach's conjecture is actually true will it be the case that it is impossible to prove its negation. But if it is ALSO unprovable (but STILL true) you will NOT be able to prove that the negation is unprovable, because that would mean that there doesn't exist ANY number N that disproves the conjecture, so would prove the unprovable original conjecture....

Consider the statement "All swans are white", but you live in a universe with an infinite number of swans.

Lets assume that there exists at least one black swan. Proving the statement false is trivial once you find the first black swan.

However, if all swans in the given universe ARE white, and you have no way of inspecting every one, you can never PROVE that they are all white. Also you can NOT prove that it is impossible to prove the negation.

Re:Gödel, Escher, Bach: an in-depth explainer by kubanczyk on Wednesday September 14, 2022 @09:29AM (#32836891)
> if all swans in the given universe ARE white, and you have no way of inspecting every one, you can never PROVE

Yes, you can. Math is not physics. Pythagoras was able to prove his theorem about every triangle in the universe without inspecting every triangle in the universe. The trick is that "the universe" is not the physical universe, it's just a choice of axioms.

Re:Gödel, Escher, Bach: an in-depth explainer by trashtester on Wednesday September 14, 2022 @07:06PM (#32844680)
> Pythagoras was able to prove his theorem about every triangle in the universe without inspecting every triangle in the universe.

My understanding is that statements about members of infinite sets can be decidable if there exists a method to set up use recoursion/induction to cover all of them. For the set of right triangles, this is relatively straight forward (if we ignore the complexity introduced by real numbers).

For statements on infinite sets where it is not possible to reduce a proof to such recoursion/induction, you quickly end up needing an infinite number of steps to cover all cases, meaning the problem is undeciable/uncomputable.

See the Church-Turing thesis: https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

Re:Gödel, Escher, Bach: an in-depth explainer by trashtester on Wednesday September 14, 2022 @07:52AM (#32835868)
> Because if you show that the converse of Goldbach's conjecture is not provable, you have actually proven Goldbach's conjecture (since you have shown that there is no counterexample!).

Lets hypothetize that Goldbach's conjecture is true and unprovable (let's call it S1). In that case, the following statments are both true: C1) It is impossible to prove S1. C2) It is impossible to prove the converse of S1. (since in this case S1 is true, the converse is actually false, so cannot be proven).

Now, if we go into meta-proofs, we may be able to prove C1 (whether or not S1 is true). But we will never be able to prove C2 (if S1 is true and unprovable, C2 will also be true and unprovable).

Now, if S1 is actually false, We may actually at some point find a proof of that. But that's not really so interesting.

The interesting part is that there DOES exist statements like this that ARE true AND unprovable (even if we don't know which statments), we just don't know WHAT statments those are.

Re:Gödel, Escher, Bach: an in-depth explainer by quantum_state on Tuesday September 13, 2022 @07:24PM (#32831409)
what if the proofs cannot be described as finite or countable sets that does not render a straightforward application of diagonalization? What happens to Goedel’s theorem then?
Re:Gödel, Escher, Bach: an in-depth explainer by pfortuny on Wednesday September 14, 2022 @03:03AM (#32834120)
That is not a “proof” in the statement of Gödel’s theorem.

A proof (there) is just a finite number of symbols which happens to have a specifix form (A=>B AND A), where A and B are sentences, which are finite sequences of symbols having a slecific form… Wait, I am telling you a half of what Gödel did to prove his result.

Re:Gödel, Escher, Bach: an in-depth explainer by teawrecks on Tuesday September 13, 2022 @08:28PM (#32831842)
What's an example of an uncountably infinite proof?
Re:Gödel, Escher, Bach: an in-depth explainer by didericis on Wednesday September 14, 2022 @01:05AM (#32833505)
Any visual geometric proof. You can build an uncountably infinite set of different sized variations proving the same underlying relationships like this: https://youtu.be/CAkMUdeB06o

Whether or not a visual demonstration like that is actually a “proof” is a separate question. It definitely wouldn’t satisfy Hilbert, and doesn’t meet this definition:

> A proof of a statement S is a finite sequence of assertions S(1), S(2), … S(n) such that S(n) = S and each S(i) is either an axiom or else follows from one or more of the preceding statements S(1), …, S(i-1) by a direct application of a valid rule of inference.

I also don’t know of any visual “proof” like that which can’t be explained much more rigorously and powerfully with a formal set of assertions. But pulling threads like this and really asking what makes a proof a “proof” are some of the deepest questions I think a person can ask. It’s worth doing if only to appreciate what an incredible accomplishment all of the formal set theory work is in unifying and attempting to define meta concepts like “proof” itself.

Re:Gödel, Escher, Bach: an in-depth explainer by jhanschoo on Wednesday September 14, 2022 @01:20AM (#32833584)
> You can build an uncountably infinite set of different sized variations proving the same underlying relationships like this

For such proofs to be contained in a finite space, the verifying person or machine needs to be able to distinguish between arbitrarily minute differences between proofs.

Re:Gödel, Escher, Bach: an in-depth explainer by didericis on Wednesday September 14, 2022 @01:40AM (#32833671)
You don’t need to go through every possible element in that infinite uncountable set to prove that relationship, though. You can create an arbitrary demonstration that you can then manipulate in your head. Once you see that water demonstration you can inuit how that relationship must persist at different sizes.

Again, that doesn’t really count as a “proof” by modern standards, but it’s how the ancient greeks thought (they used more than just visual intuition/they also used more rigorous and formal propositions than that water thing, but they were visual and didn’t involve finite sets)

Re:Gödel, Escher, Bach: an in-depth explainer by wikfwikf on Wednesday September 14, 2022 @05:47AM (#32835025)
But your brain is, presumably, doing finitely many cognitive steps, so it seems that a proof you can understand can also be expressed finitely?
Re:Gödel, Escher, Bach: an in-depth explainer by didericis on Wednesday September 14, 2022 @08:34AM (#32836259)
That’s a really deep question. If our brains are like digital computers, then yes, that’d be true. But they could be like analog computers, quantum computers, or something we don’t yet have the ability to describe.
Re:Gödel, Escher, Bach: an in-depth explainer by wikfwikf on Wednesday September 14, 2022 @08:50AM (#32836426)
The problem with this theory is: what is the part of a geometric proof which cannot be described or validated using a classical, discrete computer? There is no such step. All parts of mathematics which mathematicians are able to agree on can be so described. There is no scope for our brains taking in an analog measurement, doing an analog measurement step on it, and using it to confirm the truth of a mathematical statement.

Of course, this is not an argument that our brains are absolutely finite and classical. Perhaps analog computations is required for an appreciation of beauty, or quantum physics is necessary for us to fall in love. But we seem to be able to check math proofs without them.

Re:Gödel, Escher, Bach: an in-depth explainer by didericis on Wednesday September 14, 2022 @09:38AM (#32837008)
I think mathematical intuition might be some kind of weird analog calculation, but yes, I can’t think of an actual visual proof that cannot also be described in discrete formal terms and validated with a computer. There might be examples out there somewhere, but I don’t know of any.
Re:Gödel, Escher, Bach: an in-depth explainer by quantum_state on Tuesday September 13, 2022 @10:05PM (#32832462)
Not aware of how to provide one due to constraint of the discrete nature of the language would have been used to describe the example … however, imagine entities that are able to communicate via continuous means … they would be able to … but would we be able to find ways to get it?