\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
\Tree
 [.$\lor $
    [.$\forall x$
        [.$P$ $x$ $x$ ]
    ]
    [.$\forall y$
        [.$Q$ $x$ $y$ ]
    ]
 ]
\end{tikzpicture}

The $x$ in the right subformula is a free variable.


\begin{multicols}{2}
An example for a \emph{satisfying} model $\Model_{SAT}$:
\begin{itemize}
\item  $\mathcal{A} = \{a, b\} $
\item  $P^{\Model_{SAT}} = \{(a,a), (b,b)\}$
\item  $Q^{\Model_{SAT}} = \{(a,a), (a,b)\}$
\end{itemize}
\columnbreak
An example for an \emph{unsatisfying} model $\Model_{UNSAT}$:
\begin{itemize}
\item  $\mathcal{A} = \{a, b\} $
\item  $P^{\Model_{UNSAT}} = \{(a,a)\}$
\item  $Q^{\Model_{UNSAT}} = \{(a,a)\}$
\end{itemize}
\end{multicols}


\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
\Tree
[.$\lnot$
  [.$\forall x$
    [.$\land$
      [.$\imp$
        [.$Q$
          [.$f$ $x$ ]
        ]
        [.$P$
          [.$f$
            [.$f$ $x$ ]
          ]
        ]
      ]
      [.$\lnot$
        [.$Q$ $x$ ]
      ]
    ]
  ]
]


\end{tikzpicture}
\begin{multicols}{2}
An example for a \emph{satisfying} model $\Model_{SAT}$:
\begin{itemize}
\item $\mathcal{A} = \{a, b\} $
\item $f^{\Model_{SAT}} = \{ x \rightarrow x \}$
\item $P^{\Model_{SAT}} = \true$
\item $Q^{\Model_{SAT}} = \false$
\end{itemize}
\columnbreak
An example for an \emph{unsatisfying} model $\Model_{UNSAT}$:
\begin{itemize}
\item  $\mathcal{A} = \{a, b\} $
\item  $f^{\Model_{UNSAT}} = \{ x \rightarrow x \}$
\item  $P^{\Model_{UNSAT}} = \true$
\item  $Q^{\Model_{UNSAT}} = \false$
\end{itemize}
\end{multicols}