[Tex/LaTex] Enderton’s tautologically equivalent symbol

Question

How does not get the $\vDash$ flipped to obtain Enderton's tautologically equivalent symbol?

Answer 1

Here is a picture (courtesy of Google Books)

The code might be

\documentclass{article}
\usepackage{amsmath,amssymb}
\usepackage{graphicx}

\newcommand{\tautimplies}{\vDash}
\newcommand{\tautimplied}{\mathrel{\text{\reflectbox{$\vDash$}}}}
\newcommand{\tauteq}{%
  \tautimplies
  \mathrel{\mspace{1mu}}%
  \tautimplied
}

\begin{document}

If \(\Sigma\) is singleton \(\{\sigma\}\), then we write
``\(\sigma \tautimplies \tau\)'' in place of 
``\(\{\sigma\} \tautimplies \tau\).'' If both \(\sigma \tautimplies \tau\) and
\(\tau \tautimplies \sigma\), then \(\sigma\)  and \(\tau\) are said to be 
\emph{tautologically equivalent} (written \(\sigma \tauteq \tau\)).
For example, in Section 1.0 we encountered the wffs
\( (\lnot(\mathbf{C} \lor \mathbf{K})) \) and
\( ((\lnot\mathbf{C}) \land (\lnot\mathbf{K})) \)
as alternative translations of an English sentence.  We can now assert that
they are tautologically equivalent.

\end{document}