It seems to me that “high-level” sentences let us reason about “low-level” sentences faster, so dropping them isn’t a good idea. But maybe we could have a performance guarantee in terms of “low-level” sentences only, like “this program prints X in the first N steps”. That sounds interesting, do you have any thoughts?
Are you making the point that we often reason about how likely a sentence is to be true and then use our conclusion as evidence about how likely it is to have a proof of reasonable length? I think this is a good point. One possible response is that if we’re doing something like logical induction in that it listens to many heuristics and pays more attention to the ones that have been reliable, then some of those heuristics can involve performing computations that look like trying to estimate how likely a sentence is to be true, in the process of estimating how likely it is to have a short proof, and then we can just pay attention to the probabilities suggested for existence of a short proof. A possible counterobjection is that if you want to know how to be such a successful heuristic, rather than just how to aggregate successful heuristics, you might want to reason about probabilities of mathematical truth yourself. A possible response to this counterobjection is that yes, maybe you should think about how likely a mathematical claim is to be true, but it is not necessary for your beliefs about it to be expressed as a probability, since it is impossible to resolve bets made about the truth of a mathematical sentence, absent a procedure for checking it.
Hmm, I was thinking about something simpler. Take for example the fact that for any n there are n! permutations of n objects. That’s not in your class of sentences which come with an “obvious” decision procedure. Yet it’s pretty useful: if you have a program that counts permutations of 100 objects one by one, you can replace it with a program that calculates 100! which is much faster. If you had uncertainty about the first decimal digit of the result (a “low-level” fact), using the “high-level” fact has just helped you resolve it faster. So “high-level” facts are useful even if you’re only interested in “low-level” facts. You’re right that using probabilities for “high-level” facts might not work, but we need to reason about them somehow, or we’ll be outplayed by those who can.
Oh, I see. But for any particular value of n, the claim that there are n! permutations of n objects is something we can know in advance is resolvable (even if we haven’t noticed why this is always true), because we can count the permutations and check.
It seems to me that “high-level” sentences let us reason about “low-level” sentences faster, so dropping them isn’t a good idea. But maybe we could have a performance guarantee in terms of “low-level” sentences only, like “this program prints X in the first N steps”. That sounds interesting, do you have any thoughts?
Are you making the point that we often reason about how likely a sentence is to be true and then use our conclusion as evidence about how likely it is to have a proof of reasonable length? I think this is a good point. One possible response is that if we’re doing something like logical induction in that it listens to many heuristics and pays more attention to the ones that have been reliable, then some of those heuristics can involve performing computations that look like trying to estimate how likely a sentence is to be true, in the process of estimating how likely it is to have a short proof, and then we can just pay attention to the probabilities suggested for existence of a short proof. A possible counterobjection is that if you want to know how to be such a successful heuristic, rather than just how to aggregate successful heuristics, you might want to reason about probabilities of mathematical truth yourself. A possible response to this counterobjection is that yes, maybe you should think about how likely a mathematical claim is to be true, but it is not necessary for your beliefs about it to be expressed as a probability, since it is impossible to resolve bets made about the truth of a mathematical sentence, absent a procedure for checking it.
Hmm, I was thinking about something simpler. Take for example the fact that for any n there are n! permutations of n objects. That’s not in your class of sentences which come with an “obvious” decision procedure. Yet it’s pretty useful: if you have a program that counts permutations of 100 objects one by one, you can replace it with a program that calculates 100! which is much faster. If you had uncertainty about the first decimal digit of the result (a “low-level” fact), using the “high-level” fact has just helped you resolve it faster. So “high-level” facts are useful even if you’re only interested in “low-level” facts. You’re right that using probabilities for “high-level” facts might not work, but we need to reason about them somehow, or we’ll be outplayed by those who can.
Oh, I see. But for any particular value of n, the claim that there are n! permutations of n objects is something we can know in advance is resolvable (even if we haven’t noticed why this is always true), because we can count the permutations and check.