To assign 0.99999 to a judgement that a : T is to assign 0.99999 probability to “a proves T”, which also states that “T is inhabited”, which then means “we believe T”.
Okay, let’s say the probability you assign is called ‘alpha’ and you don’t call it a probability, you call it alpha, for the sake of clarity. So you assign alpha of 0.999999 to “a proves T”. Does that, in any practical sense, imply that in some situations we don’t have to worry too much about some statement being false (e.g. don’t have to worry that adding a proves T as an axiom would result in an internal contradiction), and if so, why?
Does that, in any practical sense, imply that in some situations we don’t have to worry too much about some statement being false (e.g. don’t have to worry that adding a proves T as an axiom would result in an internal contradiction), and if so, why?
The whole approach here is to generalize the proof-theoretic (and thus computational) treatment of logic to Bayesian reasoning over classical propositions. The degree of belief assigned is thus the degree of belief assigned by a specific set of premises (those we fed into the logic with some arbitrary probabilities) (keep in mind that in proof theory (sequent calculi, natural deduction, lambda calculi), the axioms of the logic are not treated as logical premises but instead as computational operations performed on logical premises) to the theorem T via proof a.
To assign 0.99999 to a judgement that
a : T
is to assign 0.99999 probability to “a proves T”, which also states that “T is inhabited”, which then means “we believe T”.Okay, let’s say the probability you assign is called ‘alpha’ and you don’t call it a probability, you call it alpha, for the sake of clarity. So you assign alpha of 0.999999 to “a proves T”. Does that, in any practical sense, imply that in some situations we don’t have to worry too much about some statement being false (e.g. don’t have to worry that adding a proves T as an axiom would result in an internal contradiction), and if so, why?
The whole approach here is to generalize the proof-theoretic (and thus computational) treatment of logic to Bayesian reasoning over classical propositions. The degree of belief assigned is thus the degree of belief assigned by a specific set of premises (those we fed into the logic with some arbitrary probabilities) (keep in mind that in proof theory (sequent calculi, natural deduction, lambda calculi), the axioms of the logic are not treated as logical premises but instead as computational operations performed on logical premises) to the theorem
T
via proofa
.