Probability Logic for Type Spaces

Using a formal prepositional language with operators "individual i assigns probability at least α" for countably many α, we devise an axiom system which is sound and complete with respect to the class of type spaces in the sense of Harsanyi (1967-1968, Management Science, 14, 159-182). A crucial inference rule requires that degrees of belief be compatible for any two sets of assertions which are equivalent in a suitably defined natural sense. The completeness proof relies on a theorem of the alternative from convex analysis, and uses the method of filtration by finite sub-languages.