\begin{tikzpicture}[>=stealth,minimum size = 0.3cm,scale = 0.8]
[level distance=40mm]
\tikzstyle{level 1}=[sibling distance=5cm]
\node{$x: M \sqcap \forall b.K \sqcap (\neg M \sqcup \exists b.(\neg H \sqcap \neg K))  \checkmark$ }
child{node(nodem){$x: M$}
 child{node{$x: \forall b.K$}
  child{node{$x: \neg M \sqcup \exists b. \neg H \sqcap \neg K \checkmark$}
   child{
   node(nodenotm){$x: \neg M$}
   child [level distance=.5cm]{
   node{$\Box$} edge from parent [draw=none]}}
   child{node{$x: \exists b. \neg H \sqcap \neg K \checkmark$}
    child{node{$y:\neg H \sqcap \neg K \checkmark$}
     child{node{$(x,y) \in b$}
      child{node{$y: \neg H$}
       child{node(nodek){$y: \neg K$}
        child{node(nodenotk){$y: K$}
           child [level distance=.5cm]{node{$\Box$} edge from parent [draw=none]}}
        }}}}}}}};
\path[<->,dashed](nodem) edge[bend right] node[left] {$\lightning$} (nodenotm);
\path[<->,dashed](nodek) edge[bend left] node[right] {$\lightning$} (nodenotk);
\end{tikzpicture}