= 27d567bc2d48d9f40e9ccc20ea370b15)
Sewing-Machine comments on Syntacticism - Less Wrong
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)
This is because you have misconstrued my view. My philosophy of syntacticism is not formalism, nor is it a straight rejection of Platonism. Instead it is a Platonic formalism, in which the Platonic ideals are of the form "thus-and-such is derivable from these axioms with these deduction rules", except that any attempt to talk directly and formally about those Platonic ideals fails (because that involves application of a formal system to a formal system).
The point of my post is that 'implemented PA' in fact implements "PA", and there can be no rigorous proof that the referent of "PA" is PA (because such a rigorous proof in fact ends with ""PA" is PA", and how do we know that this new system's "PA" is PA?)
But how do we prove that (ZFC proves statement about PA) ⇔ (statement about PA)? Only by appealing to a higher-order theory. After all, I can define a theory T by the axioms "1. PA is consistent. 2. PA proves PA is consistent.", where (if necessary) PA is defined by listing PA's axioms, and yet if I were to conclude from this that PA proves PA's consistency without thereby becoming inconsistent, you would scream blue Gödelian murder, because you have a proof in ZFC that if PA proves PA is consistent then PA is not consistent. But I have a proof in T that PA is consistent and proves PA consistent (a trivial one, in fact). So how can you justify privileging ZFC's referent of "PA" over T's referent of "PA"? Only by appeal to some meta-theory - or by informal justification.
It is a fact that agents implementing the same deduction rules and starting from the same axioms tend to converge on the same set of theorems. Therefore there is some sense in which the theorems are inherent in the (axioms + deduction rules): there is a truth about what those (axioms + deduction rules) lead to, and that truth exists outside of any implementation. But that truth is not like a rock, it is not a physical object - so it must be a metaphysical one. Thus, Platonism.
But then why privilege any particular set of rules as having Platonic existence? Thus, all possible formal systems have Platonic existence.
The "magical spirit realm" does not say that "2+2=4". But it does say that "If you apply the rules of PA to evaluate the expression 2+2, a failure to converge on 4 implies a failure to follow the rules of PA" (which failure might, for instance, be a cosmic ray hitting a neuron).
Do I make sense now?
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!)