Probabilistic semantics for intuitionistic logic.
Hugues Leblanc, C. G. Morgan · Notre Dame Journal of Formal Logic · 1983
Venturing into technically virgin territory, we isolate probability functions that: (i) stand to intuitionistic logic as Popper's functions do to classical logic, 1 and hence (ii) rate (we believe) the appellation "intuitionistic probability functions".We then define in terms of these functions a notion of logical truth and a notion of entailment (or, if preferred, logical consequence) such that, where IL is a first-order language, A is a statement of IL, and S is a set of statements of IL, (a) A is logically true if provable by intuitionistic means (T2.8), and only ifso(T3.6)(b) A is entailed by S if provable from S by intuitionistic means (T2.10), and only if so (T3.8).Our definitions and theorems constitute-in current parlance-a probabilistic semantics for intuitionistic logic, i.e., an adaptation to intuitionistic logic of the semantics that Popper and various writers in Popper's debt have devised for classical logic. 2 We concentrate in this article on the semantics that thus issues from our probability theory.In a sequel to it we shall discuss the interpretation of Pr which dictated the ten constraints placed in Section 1 on that function.