Ah, well, if you’re only closing under propositional tautologies, then you’re not doing anything interesting. OLC(X) is for practical purposes the same as X (not just because it’s decidable, as you say, but more importantly because it’s so weak). So your suggestions boils down to assigning P=1 to axioms, P=0 to their negations, and trying to figure out non-trivial probabilities for everything else by constraining on propositional consistency. But propositional consistency is merely a very thin veneer over X.
Because propositional inference isn’t going to be able to break down quantifiers and “peer” inside their clauses, any quantified statement that’s not already related to X [in the sense of participating in X either as a member or as a clause of a Boolean member] is opaque to X. So if I write A = (exists Y)(Y=2) and B = (exists Z)(Z=2 and Z=3), you’ll be forced to deduce P(A)=P(B) under your axioms, or pre-commit to include in your axioms A, not(B) and everything else in a smoothly growing (complexity-wise) list of arithmetical truths I can come up with. That doesn’t seem very useful.
But propositional consistency is merely a very thin veneer over X.
That was my goal—to come up with a minimum necessary for consistency, but still sufficient to prove the 1⁄2 probability for digits of PI :) If you wish to make OLC stronger, you’re free to do so, as long as it remains decidable. For example, you can define OLC(X) to be {everything provable from X by at most 10 steps of PA-power reasoning, followed by propositional calculus closure}.
In your scheme you have P=1/2 for anything nontrivial and its negation that’s not already in X. It just so happens that this looks reasonable in case of the oddity of a digit of pi, but that’s merely a coincidence (e.g. take A=”a millionth digit of pi is 3″ rather than ”...odd”).
No, a statement and its negation are distinguishable, unless indeed you maliciously hide them under quantifiers and throw away the intermediate proof steps.
Ah, well, if you’re only closing under propositional tautologies, then you’re not doing anything interesting. OLC(X) is for practical purposes the same as X (not just because it’s decidable, as you say, but more importantly because it’s so weak). So your suggestions boils down to assigning P=1 to axioms, P=0 to their negations, and trying to figure out non-trivial probabilities for everything else by constraining on propositional consistency. But propositional consistency is merely a very thin veneer over X.
Because propositional inference isn’t going to be able to break down quantifiers and “peer” inside their clauses, any quantified statement that’s not already related to X [in the sense of participating in X either as a member or as a clause of a Boolean member] is opaque to X. So if I write A = (exists Y)(Y=2) and B = (exists Z)(Z=2 and Z=3), you’ll be forced to deduce P(A)=P(B) under your axioms, or pre-commit to include in your axioms A, not(B) and everything else in a smoothly growing (complexity-wise) list of arithmetical truths I can come up with. That doesn’t seem very useful.
That was my goal—to come up with a minimum necessary for consistency, but still sufficient to prove the 1⁄2 probability for digits of PI :) If you wish to make OLC stronger, you’re free to do so, as long as it remains decidable. For example, you can define OLC(X) to be {everything provable from X by at most 10 steps of PA-power reasoning, followed by propositional calculus closure}.
In your scheme you have P=1/2 for anything nontrivial and its negation that’s not already in X. It just so happens that this looks reasonable in case of the oddity of a digit of pi, but that’s merely a coincidence (e.g. take A=”a millionth digit of pi is 3″ rather than ”...odd”).
No, a statement and its negation are distinguishable, unless indeed you maliciously hide them under quantifiers and throw away the intermediate proof steps.