= 27d567bc2d48d9f40e9ccc20ea370b15)
Sewing-Machine comments on Syntacticism - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (62)
Not so! From most interesting formal systems there are exponentially many possible deductions that can be made. All known agents can only make a bounded number of possible deductions. A widely believed conjecture implies that longer-lived agents could only make a polynomial number of possible deductions.
Um, that's not quite what I meant... if I prove a theorem you're unlikely to prove its negation, and if I tell you I have a proof of a theorem you're likely to be able to find one. Moreover, in the latter case, if you're not able to find a proof, then either I am mistaken in my belief that I have a proof, or you haven't looked hard enough (and in principle could find a proof if you did). That doesn't mean that every agent with "I think therefore I am" will deduce the existence of rice pudding and income tax, it only means that if one agent can deduce it, the others in principle can do the same. For any formal system T, the set {X : T proves X} is recursively enumerable, no? (assuming 'proves' is defined by 'a proof of finite length exists', as happens in Gödel-numbering / PA "box")
As you know, I am outside of mainstream opinion on this. But this:
is flatly wrong if P <> NP and not controversially so. If I reach a point in a large search space there is no guarantee that you can reach the same point in a feasible amount of time.
Recursively enumerable sure. Not feasibly enumerable.
But why should feasibility matter? Sure, the more steps it takes to prove a proposition, the less likely you are to be able to find a proof. But saying that things are true only by virtue of their proof being feasible... is disturbing, to say the least. If we build a faster computer, do some propositions suddenly become true, because we now have the computing power to prove them?
Me saying I have a proof of a theorem should cause you to update P(you can find a proof) upwards. (If it doesn't, I'd be very surprised.) Consequently, there is something common.
Similarly, no matter how low your prior probability for "PA is consistent", so long as that probability is not 0, learning that I have proved a theorem should cause you to decrease your estimate of the probability that you will prove its negation.
Incidentally but importantly, lengthiness is not expected to be the only obstacle to finding a proof. Cryptography depends on this.
As to why feasibility matters: it's because we have limited resources. You are trying to reason about reality from the point of view of a hypothetical entity that has infinite resources. If you wish to convince people to be less skeptical of infinity (your stated intention), you will have to take feasibility into account or else make a circular argument.
I am certainly not saying that feasible proofs cause things to be true. Our previous slow computer and our new fast computer cause exactly the same number of important things to be true: none at all. That is the formalist position, anyway.
Not so. If I have P(PA will be shown inconsistent in fewer than m minutes) = p, then I also have P(I will prove the negation of your theorem in fewer than m+1 minutes) = p. Your ability to prove things doesn't enter into it.
True; stick a ceteris paribus in there somewhere.
Not so; I am reasoning about reality in terms of what it is theoretically possible we might conclude with finite resources. It is just that enumerating the collection of things it is theoretically possible we might conclude with finite resources requires infinite resources (and may not be possible even then). Fortunately I do not require an enumeration of this collection.
So either things that are unfeasible to prove can nonetheless be true, or nothing is true. So why does feasibility matter again?
No, it is > p. P(I will prove 1=0 in fewer than m+1 minutes) = p + epsilon. P(I will prove 1+1=2 in fewer than m+1 minues) = nearly 1. This is because you don't know whether my proof was correct.
A positive but minuscule amount. This is how cryptography works! In less than a minute (aided by my very old laptop), I gave a proof of the following theorem: the second digit of each of each of the prime factors of n is 6, where
n = 44289087508518650246893852937476857335929624072788480361
It would take you much longer to find a proof (even though the proof is very short!).
Update!
About feasibility, I might say more later.
Right - but if there were no 'fact-of-the-matter' as to whether a proof exists, why should it be non-zero at all?
But that isn't what either of us said. You mentioned P(you can find a proof). I am telling you (telling you, modulo standard open problems) that this can be very small even after another agent has found a proof. This is a standard family of topics in computer science.
I am aware it can be very small. The only sense in which I claimed otherwise was by a poor choice of wording. The use I made of the claim that "Agents implementing the same deduction rules and starting from the same axioms tend to converge on the same set of theorems" was to argue for the proposition that there is a fact-of-the-matter about which theorems are provable in a given system. You accept that my finding a proof causes you to update P(you can find a proof) upwards by a strictly positive amount - from which I infer that you accept that there is a fact-of-the-matter as to whether a proof exists. In which case, you are not arguing with my conclusion, merely with a step I used in deriving it - a step I have replaced - so does that not screen off my conclusion from that step - so why are you still arguing with me?
I am still arguing with you because I think your misstep poisons more than you have yet realized, not to get on your nerves.
No. "I can find a proof in time t" is a definite event whose probability maybe can be measured (with difficulty!). "A proof exists" is a much murkier statement and it is much more difficult to discuss its probability. (For instance it is not possible to have a consistent probability distribution over assertions like this without assigning P(proof exists) = 0 or P(proof exists) = 1. Such a consistent prior is an oracle!)
I wasn't suggesting you were trying to get on my nerves. I just think we're talking past each other.
As a first approximation, what's wrong with "\lim_{t -> \infty} P(I can find a proof in time t)"?
Also, I don't see why the prior has to be oracular; what's wrong with, say, P(the 3^^^3th decimal digit of pi is even)=½? But then if the digit is X, then surely a proof exists that it is X (because, in principle, the digit can be computed in finitely many steps); it must be some X in [[:digit:]], so if it is even a proof exists that it is even; otherwise (sharp swerve) one does not, and P=½. Not sure about that sharp swerve; if I condition all my probabilities on |arithmetic is consistent) then it's ok. But then, assuming I actually need to do so, the probabilities would be different if conditioned on |arithmetic is inconsistent), and thus by finding a proof, you find evidence for or against the assertion that arithmetic is consistent. But things you can find evidence on, exist! (They are the sheep that determine your pebbles.) So where did I go wrong? (Did I slip a meta-level somewhere? It's possible; I was juggling them a bit.)
Suggestions of dire wrongness? Bah. Now I'm all tempted to read through the context. But so far I've failed to see the point!
Wait. "A proof exists" is murky? What sort of bizarre twisted mathematical reasoning is behind that? (Not that I'm saying mathematics doesn't say equally bizarre and twisted things!)
In the set of all mathematical things you can say either there is one that constitutes a proof or there isn't. That doesn't mean it is possible to establish whether such a proof exists by using all the computing power in the universe but it still exists. Not a big deal.
Counter assertion: Yes there is. It's just mundane logical uncertainty. But even if you decide you're not allowed to assign probabilities to logical unknowns (making the whole exercise tautologically pointless) that doesn't make "a proof exists" murky. If anything it makes it arbitrarily more clear cut. It means you're allowed to say 'a proof exists' or the reverse claim but have forbidden yourself the chance to assign probabilities to the possibility. And not allowing yourself to think about it doesn't do anything to change whether the thing exists or not.