Probability Logic for Type Spaces

Using a formal propositional language with operators "individual i assigns probability at least a" for countable many a, we devise an axiom system which is sound and complete with respect to the class of type spaces in the sense of Harsanyi (1967-68). A crucial axiom 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.