 In addition to standard modal models, logic also has a straightforward analogue to probabilistic type spaces: logical type spaces. In a formal framework first introduced by Fagin, Geanakoplos et al. (1999), an n-type is a sequence \(\mathfrak{f}_n=\langle f_0,f_1\ldots,f_{n}\rangle\) where \(f_0\) specifies the state of nature, i.e., a valuation recording which atomic propositions are true or false, and \(f_1\) lists for all players the states of nature they consider possible. \(f_m\) for \(m\geq 0\) then specifies for all players which \((m-1)\)-types, i.e., sequences \(\langle g_0,\ldots,g_{m-1}\rangle\) they consider possible. In this way, an n-type fixes the player’s higher-order beliefs up to level n. These types are, of course, subject to coherence conditions: the agents’ k-types for different k must fit together. For instance, whenever some agent considers a k-type \(\mathfrak{f}_k\) possible, she must also consider any initial segment \(\mathfrak{f}_{k'}\) for \(k'&lt;k\) possible. Conversely, any \(k'\) type the agent considers must be the initial segment of some k type the agent holds possible. Type spaces offer a semantics for the epistemic language: Inductively, for a formula \(\varphi\) of modal depth m, \(K_i\varphi\) is true at a type \(\mathfrak{f}_n\) if all \(g_{m}\in f_{m+1}(i)\) satisfy \(\varphi\) or if \(m&gt;n\).