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

191–196 of 196 posts

Re: What does “Undecidable” mean, anyway

#191

Post by Tainnor »

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.

First of all, I should have written "recursively enumerable theory" or "theory with decidable axioms". But I think it's clear that I'm referring to things like ZFC, first-order PA or any other similar system.

With that out of the way, it's pretty easy to write a general theorem prover for such theories if you can solve the halting problem.

First define a TM G that takes as input 1. the description of another TM A that decides whether a particular sentence is an axiom of some theory T and 2. a sentence P. We enumerate all syntactically valid proofs with P as the conclusion and check whether all axioms are valid according to A and all inferences are sound. If we find a valid proof, we stop. (G can obviously be built.)

Then define H such that it takes the same inputs as G, and then (using the halting oracle) determines whether G would halt given A and P. If yes, return true, otherwise false.

Then H would be a decider for the language consisting of all pairs T |= P, where T is some recursively enumerable theory.

Re: What does “Undecidable” mean, anyway

#193

Post by Tainnor »

bubblyworld wrote: post #189
Maxatar wrote: post #187

Earlier quoted context omitted.

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?

> By the compactness theorem this is guaranteed to work.

I think you mean completeness, but essentially yes.

Re: What does “Undecidable” mean, anyway

#194

Post by bubblyworld »

Tainnor wrote: post #193
bubblyworld wrote: post #189

Earlier quoted context omitted.

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?

> By the compactness theorem this is guaranteed to work. I think you mean completeness, but essentially yes.

In this case I meant compactness - if a statement follows from your (possibly infinite set of) axioms then it follows from a finite subset of them. But you can skin the cat in many ways, yeah (proof theory vs model theory way of looking at it I guess).

Re: What does “Undecidable” mean, anyway

#195

Post by tel »

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

Earlier quoted context omitted.

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.

The quantification over T is still kind of weird, though. In a formulation like `for all T, (T and P consistent and T and neg P consistent)` is trivially false, just take `T = {neg P}` and now `{P, neg P}` is inconsistent.

We're never trying to show P is independent of all theories, just some specific one.

Re: What does “Undecidable” mean, anyway

#196

Post by DonaldPShimoda »

andoando wrote: post #179
DonaldPShimoda wrote: post #175

Earlier quoted context omitted.

> If you were say, writing a programming language, it would be nice to understand the fundamentals. I work in programming languages research. Nobody uses Turing machines for anything. We do talk about decidability when it comes to certain things (type-checking, for instance), but that doesn't use Turing machines directly. The lambda calculus comes up frequently, on the other hand, but it's used as a base from which w…

Considering we can implement and simulate a Turing machine and get actual calculations, how do you consider them to be completely abstract/theoretical?

A Turing machine is not a real device; I suggest reading the Wikipedia article on abstract machines [0], which says verbatim: "Turing machines, for example, are some of the most fundamental abstract machines in computer science."

Abstract/theoretical doesn't mean "doesn't do anything practical". Labeling gravity as a "theory" doesn't mean that it doesn't hold things to the surface of the Earth. The Turing machine is a model of computation that is so simple (so abstract) that we can implement it with a pencil and paper very easily, and it can be used for actual calculation, but it is not — and never was — a literal device that existed physically.

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

Post reply on HN