\documentclass[a4paper,10pt]{article}
\usepackage[utf8]{inputenc}
\usepackage{pdfpages}
\usepackage{latexsym}
\usepackage{amssymb,amsthm,amsmath}
\usepackage{amsthm}

\begin{document}
 \newcommand{\nxt}{{\ensuremath\raisebox{0.25ex}{\text{\scriptsize$\bigcirc$}}}}
\newcommand{\Rdiamond}{\Diamond_{\!F}}
\newcommand{\Rbox}{\Box_{\!F}}
\newcommand{\Rnext}{\nxt_{\!F}}
\newcommand{\Ldiamond}{\Diamond_{\!P}}
\newcommand{\Lbox}{\Box_{\!P}}
\newcommand{\Lnext}{\nxt_{\!P}}
\newcommand{\SVdiamond}{\mathop{\ooalign{$\Diamond$ \cr \kern0.5ex
    \raisebox{0.35ex}{\scalebox{0.7}{$*$}}} \kern-0.9ex}}
\newcommand{\SVbox}{\mathop{\ooalign{$\Box$ \cr \kern0.42ex
    \raisebox{0.3ex}{\scalebox{0.7}{$*$}}} \kern-0.9ex}}


$ \forall X. ((E1NameInv(X) \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1NameInv(X)) \land $ \\ 
 $ (String(X) \rightarrow  \lnot Person(X)) \land $ \\ 
 $ (E1Name(X) \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name(X)) \land $ \\ 
 $ (E1NameInv(X) \rightarrow String(X)) \land $ \\ 
 $ (E2Name(X) \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name(X)) \land $ \\ 
 $ (Person(X) \rightarrow E1Name(X)) \land $ \\ 
 $ (E2Name(X) \rightarrow E1Name(X)) \land $ \\ 
 $ (Person(X) \rightarrow  \lnot E2Name(X)) \land $ \\ 
 $ (E1NameInv(X) \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv(dNameInv)) \land $ \\ 
 $ (PinvName \rightarrow E1Name(dName)) \land $ \\ 
 $ (E1Name(X) \rightarrow  \SVbox PName))$ 
\end{document}