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.
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.