Hacker News Reader

Comment by quantum_state | Hacker News Reader

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?

View on HN

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.

What's an example of an uncountably infinite proof?

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?

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.

> 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.

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)

But your brain is, presumably, doing finitely many cognitive steps, so it seems that a proof you can understand can also be expressed finitely?

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.

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.

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.

Reply on news.ycombinator.com