Lastly, for statements that are unprovable, we have to assign a probability of ½.
You can’t do that. Let φ and ψ be sentences such that φ, ψ, and (φ ^ ψ) are all neither provable nor disprovable. If all of these sentences are given probability 1⁄2, then since φ and (φ ^ ψ) have the same probability, (φ ^ ~ψ) must have probability 0. That is, φ implies ψ with probability 1. By symmetry, ψ implies φ with probability 1, so φ and ψ are equivalent with probability 1. But there exist such pairs of sentences that are not equivalent.
Edit: Actually it looks like my argument doesn’t apply in your system because it does not satisfy the axioms of a probability measure. For instance, if φ has a short proof that does not meantion ψ anywhere, and ψ does not have a short proof, then (φ v ψ) will be provable, with its shortest proof being the proof of φ with the rule of inference φ |- (φ v ψ) appended to the end, a longer proof, and thus P(φ v ψ) < P(φ), which is ridiculous. Another reason I don’t like the idea of assigning probabilities based on proof length is that in order to compute the probability, you have to find a proof, and by that time, you may as well give probability 1 to the statement. The only reason I would want to assign a probability other than 1 to a provable statement is if I didn’t already know that it was provable.
You can’t do that. Let φ and ψ be sentences such that φ, ψ, and (φ ^ ψ) are all neither provable nor disprovable. If all of these sentences are given probability 1⁄2, then since φ and (φ ^ ψ) have the same probability, (φ ^ ~ψ) must have probability 0. That is, φ implies ψ with probability 1. By symmetry, ψ implies φ with probability 1, so φ and ψ are equivalent with probability 1. But there exist such pairs of sentences that are not equivalent.
Edit: Actually it looks like my argument doesn’t apply in your system because it does not satisfy the axioms of a probability measure. For instance, if φ has a short proof that does not meantion ψ anywhere, and ψ does not have a short proof, then (φ v ψ) will be provable, with its shortest proof being the proof of φ with the rule of inference φ |- (φ v ψ) appended to the end, a longer proof, and thus P(φ v ψ) < P(φ), which is ridiculous. Another reason I don’t like the idea of assigning probabilities based on proof length is that in order to compute the probability, you have to find a proof, and by that time, you may as well give probability 1 to the statement. The only reason I would want to assign a probability other than 1 to a provable statement is if I didn’t already know that it was provable.