Ah. I didn’t quite understand what you were trying to do there.
In general in this theory, I don’t think we have (p(phi) < 1 → p(phi) =1) → p(phi) = 1. The theory only reflects on itself to within epsilon, so what the theory would conclude if it were certain about p(phi) being less than 1 can’t be taken as the premise of a proof-by-contradiction in the same way that ~phi can be taken as a premise… ergh, I’m trying to figure out a more helpful way to state this than “I don’t think you can derive that kind of probabilistic proof by contradiction from the stated properties of the theory because the system is never supposed to know the exact probabilities it assigns”.
Stuart’s proof by contradiction goes through, as far as I can see. (The speculation in the last paragraph doesn’t, as Paul notes, and I don’t know what “Hence P(‘G’)=1” is supposed to mean, but the proof by contradiction part does work.)
ETA: I now think that “Hence P(‘G’) = 1” is supposed to mean that this statement is implied by the first-order theory (T + the reflection axioms).
I think this should be “Then P(G) ⇐ 1”.
No, that’s correct. P(G)<1 is the premise of a proof by contradiction.
Ah. I didn’t quite understand what you were trying to do there.
In general in this theory, I don’t think we have (p(phi) < 1 → p(phi) =1) → p(phi) = 1. The theory only reflects on itself to within epsilon, so what the theory would conclude if it were certain about p(phi) being less than 1 can’t be taken as the premise of a proof-by-contradiction in the same way that ~phi can be taken as a premise… ergh, I’m trying to figure out a more helpful way to state this than “I don’t think you can derive that kind of probabilistic proof by contradiction from the stated properties of the theory because the system is never supposed to know the exact probabilities it assigns”.
EDIT: Retracted pending further cogitation.
Stuart’s proof by contradiction goes through, as far as I can see. (The speculation in the last paragraph doesn’t, as Paul notes, and I don’t know what “Hence P(‘G’)=1” is supposed to mean, but the proof by contradiction part does work.)
ETA: I now think that “Hence P(‘G’) = 1” is supposed to mean that this statement is implied by the first-order theory (T + the reflection axioms).
I used the axioms as stated, and any non-intuitionist logic. If we want to capture your intuition, I think we’ll have to tweak the definitions...