Hacker News Reader

There's one thing worth mentioning here. There's an algorithm that checks if a graph has given minor. If you fix a minor once and for all, the algorithm that checks if graph contains a fixed minor has polynomial complexity. Together with Robertson-Seymour theorem, it implies that for any family closed upon taking minors, the problem of determining whether given graph belongs to it, is solvable in polynomial time: just check if it contains forbidden minors. Each minor can be tested in polynomial time, and there are finitely of them, so the whole algorithm works in polynomial time.

Now, the thing is: since we don't know the minors, we don't know the algorithm. In other words, we just non-constructively proved that some problem can be solved in polynomial time. We only proved that algorithm exists, we just don't know what it is.

This is closely related to proof by the probabilistic method, which shows up quite often in pattern recognition literature and combinatorics (Erdös was fond of it). This method says that instead of even proving the exact existence of something (despite missing any examples) you simply prove that the probability of its existence is positive (and thus cannot be zero).

At some level these are just proofs that lower-bound the size of the set of instances, and it may be possible to convert any such argument in to one that is more directly measuring the count of instances. In practice however they tend to go through using bounds which are derived from measurable to arguments on random variables, so the conversion is less obvious to me.

I wish my copy of DGL wasn't 2 hours away or I'd dig up one.

(Edit: Wikipedia to the rescue! The "second example" on this page goes through using Markov's Bound on distributions http://en.wikipedia.org/wiki/Probabilistic_method)

Forgive my mathematical ignorance, but you've piqued my curiosity and I haven't had any luck in searching - what is DGL?

I think he means this textbook: http://www.szit.bme.hu/~gyorfi/pbook.pdf

Yep, sorry! (Also, did not know that was online. It is totally going on my ipad now)

Thanks! I was going bonkers trying to find that with only the acronym.

They aren't necessarily unfindable, there just isn't a generic method of obtaining them.

For example, we do know the minors for 'graph is planar'. We somehow found it and verified it to be correct. So, we know that some of them, at least, exist. The others, I think, would be in "The Book" (https://en.wikipedia.org/wiki/Paul_Erd%C5%91s#Personality) until they are found. So, those answers do exist in the same sense that The Book exists.

And after they are found, they definitley exist and of course will be called trivial :-)

> Now for the philosophy question: in what sense do those unfindable, unverifiable answers actually exist?

I don't really see anything philosophically interesting here. Such a feeling probably arises from a misinterpretation of the halting problem here:

> it would let us do interesting things like solve the Halting problem! That is, of course, an impossible thing to do. This proves that there is, in fact, no such procedure.

No such procedure to do it generally.

If you're familiar with the history of constructivism and the corresponding foundational debates (never truly resolved) of the early 20th century, then it is clear what I am referring to.

If you're not familiar with that, Constance Reid's Hilbert! contains a surprisingly readable history of this debate for non-mathematicians, disguised as a biography. For another accessible popular reference, The Mathematical Experience walks through this in a variety of levels of detail (you get out of it what you have the background to get out of it, but it is enjoyable anyways).

> My answer would be that there are existence proofs for things that we cannot produce examples of.

> Let me give a concrete example.

Please don't think I'm trivializing your point. I agree that it's deep and thought provoking.

But I hope that you don't mind me pointing out that your wording gave me a smile.

> Now for the philosophy question: in what sense do those unfindable, unverifiable answers actually exist?

Well, you can't calculate BusyBeaver(n), but they've found the first few Busy Beaver numbers anyway.

As one more simple example of non-constructive proof consider this theorem: "not rational number raised to not rational number is not rational".

We know it's not true because: http://www.math.hmc.edu/funfacts/ffiles/30002.3-5.shtml

Constructivist answer: they don't.