I'm working through Fagin et al.'s Reasoning About Knowledge and got stuck in their proof of the decidability of the epistemic logic $K_n$ (characterized by the class of all Kripke frames for $n$ agents $(W, R_1, \ldots, R_n)$, where every $R_i$ is a 2-place relation on $W$).
As usual in their presentation Fagin et al. derive decidability from the fact that $K_n$ has the finite model property, which they express in their theorem 3.2.2 (p. 64f.) (here $M^n$ denotes the class of all Kripke models for $n$ agents, $|\varphi|$ is the length of formula $\varphi$):
If $\varphi$ is satisfiable in some model from $M^n$, then $\varphi$ is satisfiable in some finite model from $M^n$ whose carrier contains at most $2^{|\varphi|}$ points.
The proof is straightforward with the exception of a single step. Let $con(\varphi)$ be the set of all maximally consistent subsets of $sub(\varphi) \cup \lbrace \neg \psi:\psi \in sub(\varphi)\rbrace$, where $sub(\varphi)$ is the set of subformulas of $\varphi$. The problematic step goes as follows:
Clearly, every member of $con(\varphi)$ contains exactly one of $\psi, \neg \psi$ for every $\psi \in sub(\varphi)$. From this the authors conclude that the cardinality of $con(\varphi)$ is at most $2^{|sub(\varphi)|}$, where $|sub(\varphi)|$ is the cardinality of $sub(\varphi)$.
I cannot see how the reasoning goes here. Obviously the way to go is to find an injection from $con(\varphi)$ to $sub(\varphi)$'s power set. But several attempts of mine to construct one lead nowhere. So how is the required injective function to be constructed? Any help would be appreciated.
As Fabio has pointed out, an element of $con(\varphi)$ can either contain $\psi$ or $\lnot \psi$, where $\psi \in Sub(\varphi)$. Hence there may be up to $2^{|Sub(\varphi)|}$ ways to pick a set of $\psi$'s from $Sub(\varphi)$.