Logic of Probability and Conjecture

I introduce a formalization of probability in intensional Martin-Löf type theory (MLTT) and homotopy type theory (HoTT) which takes the concept of ‘evidence’ as primitive in judgments about probability. In parallel to the intuition- istic conception of truth, in which ‘proof’ is primitive and an assertion A is judged to be true just in case there is a proof witnessing it, here ‘evidence’ is primitive and A is judged to be probable just in case there is evidence supporting it. To formalize this approach, we regard propositions as types in MLTT and define for any proposi- tion A a corresponding probability type Prob(A) whose inhabitants represent pieces of evidence in favor of A. Among several practical motivations for this approach, I focus here on its potential for extending meta-mathematics to include conjecture, in addition to rigorous proof, by regarding a ‘conjecture in A’ as a judgment that ‘A is probable’ on the basis of evidence. I show that the Giry monad provides a formal semantics for this system.