You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

Sewing-Machine comments on Syntacticism - Less Wrong Discussion

-3 Post author: ec429 23 September 2011 06:49AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (62)

You are viewing a single comment's thread. Show more comments above.

Comment author: [deleted] 24 September 2011 05:41:37AM 0 points [-]

If something is provable in principle, then (with a certain, admittedly contrived and inefficient search algorithm) the proof can be found in finite time with probability 1. No?

Finite amount of time, yes. Feasible amount of time, no, unless P = NP. When I said that you were considering agents with unlimited resources, this is what I meant--agents for whom "in principle" is not different from "in practice." There are no such agents under the sun.

Comment author: ec429 24 September 2011 06:51:21AM *  0 points [-]

But you don't have to have unlimited resources, you just have to have X large but finite amount of resources, and you don't know how big X is.

Of course, in order to prove that your resources are sufficient to find the proof, without simply going ahead and trying to find the proof, you would need those resources to be unlimited - because you don't know how big X is. But you still know it's finite. "Feasibly computable" is not the same thing as "computable". "In principle" is, in principle, well defined. "In practice" is not well-defined, because as soon as you have X resources, it becomes possible "in practice" for you to find the proof.

I say again that I do not need to postulate infinities in order to postulate an agent which can find a given proof. For any provable theorem, a sufficiently (finitely) powerful agent can find it (by the above diagonal algorithm); equivalently, an agent of fixed power can find it given sufficient (finite) time. So, while such might be "unfeasible" (whatever that might mean), I can still use it as a step in a justification for the existence of infinities.