Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What does “Undecidable” mean, anyway

buttondown.com

Post reply on HN
Print view View original

181–190 of 196 posts

Re: What does “Undecidable” mean, anyway

#181

Post by Dylan16807 »

jonahx wrote: post #178
Dylan16807 wrote: post #101

Earlier quoted context omitted.

The problem is the author's giving a misleading picture of the problem space with those examples. Tasks like optimizing whole programs or running a theorem prover are difficult/impossible tasks to do perfectly. We don't have a solution verifier that we can plug into the "free" brute force framework. With theorem provers, even when restricted to fixed finite (non-trivial) lengths, I don't think we have one that always…

> The intuition that such a thing is "too powerful" is actually a pretty bad intuition here. I still disagree. Just focus on theorem proving and not the examples that are too simple. If the halting problem could be solved, we'd be able to magically solve all these "impossible" problems. But our intuition is that just doesn't make sense, it's "too good to be true", "the universe is just more complex than that", etc. T…

The examples matter for the correctness.

This example is a little flawed, but go with me. Imagine someone was making an argument that an algorithm is too powerful because it can solve really hard problems, then list a bunch of problems that need ridiculous amounts of compute time to solve, but half their examples are NP-hard and half their examples are P.

The intuition that says "wow, that problem is very difficult to solve, so I'm very skeptical of a solution" is wrong. Because that intuition applies to both the NP examples and the P examples. That intuition is too simplistic and overgeneral.

You need an intuition that is right with both classes of problem. It has to say "no" to one class and "yes" to another. Ignoring the wrong examples is not how you evaluate an intuition.

Re: What does “Undecidable” mean, anyway

#182

Post by alok-g »

tel wrote: post #137
alok-g wrote: post #89

Earlier quoted context omitted.

Could I say that 'P is Undecidable' is defined as: It is False that {There exists T such that [(T and P) and (T and not P) are both consistent]}?

Quantifying over T is probably not going to work. In informal terms that reads like "No logic exists where P is independent", which probably wasn't quite what you wanted, but also we can trivially disprove that with T = {}. As long as P is self-consistent, then "not P" should be too. We're interested in a proposition's status with respect to some theory that we enjoy (i.e. Zermelo–Fraenkel set theory).

I intended to say the opposite, i.e., for all T (not equal to P or not-P), P is independent, but perhaps that is wrong too.

Re: What does “Undecidable” mean, anyway

#183

Post by bubblyworld »

Maxatar wrote: post #180
bubblyworld wrote: post #174

Earlier quoted context omitted.

Look, I have a masters in mathematical logic (but bailed from my PhD, to my discredit). I know what I'm talking about. You are the one who started all this bickering about what counts as a theorem prover - personally I don't really care what you call it! As for the stuff about CH, yes, there's nothing we disagree about there. And on non-recursive theories and logics without a sound/complete/effective proof theory, su…

No one is asking you to spell out the edge cases, but when you claim that a halting oracle can be used as a general-purpose theorem prover and I point out the edge cases where that won't work, it's pretty egregious to then say that I'm mixing things up, I am misusing standard terminology, etc... If you claimed every prime number is odd, and I point out that 2 is an even prime number, you don't get to turn around, pul…

[flagged]

Re: What does “Undecidable” mean, anyway

#184

Post by gnulinux »

LPisGood wrote: post #136
gnulinux wrote: post #3

The reason decidability makes no or very little sense to tons of CS or Math majors is because the logical basis of decidability is almost never explained in school. Even if you're in a logic/computability class you likely won't get a very concrete explanation, unless you're in a Philosophy of Math class. The problem that's usually not told to kids is that decidability has different sort of implications to classical m…

I was with you until here: > which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd ... Why did you randomly shoehorn in homotopy type theory? Maybe I’m overreacting to this, but the only person I’ve ever known to shoehorn homotopy type theory into largely unrelated discussion has left quite a poor impression for me.

Why not? Why do you think it's irrelevant? The reason why I included that is very simple: it models the situation I want to express exceptionally well. In "mathematics" we learn in school none of the discussion relevant to the "Halting Problem" really is relevant, which is very confusing to students who even paid attention in school. To make the situation even relevant, we need to start assuming (or realizing, accepting, whichever one you want) that there are relations in mathematics that are undecidable. If you have a model of computation, which will internally be constructive, in order to freely apply our knowledge of mathematics onto this model, we need to go back to grade school and replace every instance of "is true" with "is constructible in your model of computation/programming language" (or more traditionally "is provable"). Which means you need an entirely different reasoning framework. So, to "go back" to classical math from having understood the existence of undecidability as "home", we need to unassume this, which will be identical to assuming all relations are "decidable" within your computational model. It's not like they actually are (at least not to the extent you can compute within). Homotopy theory is the exact thing that's developed to explain situations such as this one. Why not just use it? I apologize if anything I say is wrong or misleading, I'd be happy if you can clarify.

Re: What does “Undecidable” mean, anyway

#185

Post by Tainnor »

Maxatar wrote: post #173
bubblyworld wrote: post #171

Earlier quoted context omitted.

Tainnor has basically already said what I would have (independence phenomena is an orthogonal concern, general purpose theorem prover does not mean "can prove X or not-X for any first-order sentence X"). > if you're dealing with a proposition that either has a proof or a proof of its negation, you don't need a solution to the halting problem to find it, you are guaranteed to find it eventually by definition. You don'…

Terminology isn't the most important detail here and there's no real point dwelling on it, what's important are the actual fundamental concepts at play. An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independen…

> but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC).

huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms, there's nothing specific to ZFC to it.

Re: What does “Undecidable” mean, anyway

#186

Post by lo0dot0 »

rstuart4133 wrote: post #166
mreid wrote: post #65

This is a really nice explanation of decidability. One extra thing it might be worth mentioning is that there are many more functions `f : string -> boolean` then there are programs that implement those functions. When I first encountered this topic I had trouble intuitively understanding how there could not exist an `IS_HALTING` function when it is also just a function that takes in a string (representing a program…

> This is a really nice explanation of decidability. I'm not an enthused about it as you. It doesn't mention that every undecidabilty involves an infinity. What makes a problem undecidable is not that you can't write an algorithm for it, it's that you can't guarantee the spits out an answer in a finite number of steps. Take the halting problem. He defines it as "does [the Turning] machine M halt on input i?". The ans…

Even if you can not compute the result in a finite number of steps through the naive approach there could still be a better approach, let me call it shortcut, for determining the value that can be computed. E.g. the geometric series result is known (a/(1-r)) but not computable through evaluating the series itself. A problem is undecidable if you can prove that the shortcut can not exist, it is decidable if you know a shortcut exists (knowing the formula is not required), and potentially either decidable or undecidable if a proof in either direction is unknown.

Re: What does “Undecidable” mean, anyway

#187

Post by Maxatar »

Tainnor wrote: post #185
Maxatar wrote: post #173

Earlier quoted context omitted.

Terminology isn't the most important detail here and there's no real point dwelling on it, what's important are the actual fundamental concepts at play. An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independen…

> but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC). huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms, there's nothing specific to ZFC to it.

No it won't. You must first fix a specific theory to apply your solver to. It won't work for every arbitrary choice of theory even with recursively enumerable axioms.

Re: What does “Undecidable” mean, anyway

#188

Post by bubblyworld »

Tainnor wrote: post #185
Maxatar wrote: post #173

Earlier quoted context omitted.

Terminology isn't the most important detail here and there's no real point dwelling on it, what's important are the actual fundamental concepts at play. An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independen…

> but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC). huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms, there's nothing specific to ZFC to it.

And even works for some non-recursive theories like the first-order theory of true arithmetic.

The basic idea is that you can determine whether a sentence X is in the theory or not by searching every natural number for counter-examples, and then using your halting oracle to check whether that search terminates or not.

Re: What does “Undecidable” mean, anyway

#189

Post by bubblyworld »

Maxatar wrote: post #187
Tainnor wrote: post #185

Earlier quoted context omitted.

> but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC). huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms, there's nothing specific to ZFC to it.

No it won't. You must first fix a specific theory to apply your solver to. It won't work for every arbitrary choice of theory even with recursively enumerable axioms.

Yes it will? This works for any first-order theory with a recursive set of axioms. You are simply searching for proofs of implications from the axioms and using the halting oracle to tell if the search terminates or not. By the compactness theorem this is guaranteed to work.

Of course you have to input the axioms, how would a theorem prover work otherwise?

Re: What does “Undecidable” mean, anyway

#190

Post by Maxatar »

bubblyworld wrote: post #183
Maxatar wrote: post #180

Earlier quoted context omitted.

No one is asking you to spell out the edge cases, but when you claim that a halting oracle can be used as a general-purpose theorem prover and I point out the edge cases where that won't work, it's pretty egregious to then say that I'm mixing things up, I am misusing standard terminology, etc... If you claimed every prime number is odd, and I point out that 2 is an even prime number, you don't get to turn around, pul…

[flagged]

[flagged]
Post reply on HN