09:34
@shredalert: What do you think I should do if I spot (minor) errors? Should I keep trashing the old write-up and pinning the new one?
> The above proof does not assume that T is classical, but note that classicality and soundness implies consistency, because if T is inconsistent then T proves (by classical explosion) every sentence about programs.
But more precisely it should have been:
> The above proof does not assume that T is classical, but note that classicality and soundness implies consistency, because if T is classical and inconsistent then T proves (by classical explosion) every sentence about programs.
