How to get monospace logic formulas?

Question

The following does not work in LaTeX because logic symbols can only be used in maths mode:

\texttt{\forall x(\exists y((f(x)=y)\land(\neg(g(y)=y))))}

I want to do this to stress the nature of such formulas as strings (mathematical objects). The logic symbols should look more similar to the other fixed-width symbols than to normal maths mode symbols. I would then also be able to write the following:

If $\phi$ is a formula of first-order logic and $x$ is a variable, then
\texttt{\forall$x$($\phi$)} is again a formula of first-order logic.

What's the best way to do this? Obviously, using different commands instead of \forall, \land etc. is fine. Directly entering unicode maths characters would be even better:

\texttt{∀x(∃y((f(x)=y)∧(¬(g(y)=y))))}

If $\phi$ is a formula of first-order logic and $x$ is a variable, then
\texttt{∀$x$($\phi$)} is again a formula of first-order logic.

I tried XeTeX with \usepackage{utf8x} and it doesn't work. The negation symbol gives "Character172appearedalone", and the other characters are simply not printed.

[Added after first response]

The following is so far the best approximation:

\newcommand{\Forall}{$\mathtt\forall$}
\newcommand{\Exists}{$\mathtt\exists$}
\newcommand{\Neg}{$\mathtt\neg$}
\newcommand{\Land}{$\mathtt\land$}
\newcommand{\Lor}{$\mathtt\lor$}

\noindent\texttt{\Forall x\Exists y(x\Land y)}\\
\texttt{abcde\Forall x\Exists y(x\Land y)}

The usage example demonstrates that the logic symbols do not have precisely the right width. But it's sufficient for my needs, at least initially. I guess for the final solution I will look up how to make these symbols use width zero and print them over a monotype space character.

Answer 1

This is no problem with XeTeX if you load a font that contains these characters:

\documentclass{minimal}

\usepackage{fontspec}

\setmainfont{DejaVu Serif}
\setsansfont{DejaVu Sans}
\setmonofont{DejaVu Sans Mono}

\begin{document}

\texttt{∀x(∃y((f(x)=y)∧(¬(g(y)=y))))}

If $\phi$ is a formula of first-order logic and $x$ is a variable, then
\texttt{∀$x$($\phi$)} is again a formula of first-order logic.

\end{document}

Note: Never load the inputenc package when compiling with XeTeX.

• Results using DejaVu Sans Mono:

• Results using FreeMono:

Answer 2

can't you use $\mathtt{\forall x(\exists y((f(x)=y)\land(\neg(g(y)=y))))}$ ?