# How to get monospace logic formulas?

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.

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.

-

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:

-
I tried this on my system (MikTeX 2.8 on Windows XP, numerous special fonts installed): The \land and the \neg come out fine, but the quantifiers are missing in the PDF. I assume this is a font problem? –  Hans Adler Feb 2 '11 at 11:52
@Hans: Yes, you need to make sure that the monospace font selected via \setmonofont contains the characters in question. I chose DejaVu Sans Mono for my example because I know it contains them. –  Philipp Feb 2 '11 at 12:00
@Philipp: I looked at my type 1 DejaVu Sans Mono font in a font viewer, and it turns out the quantifiers are present in it but wider than the other characters. Very odd. Perhaps that's why they don't appear in the PDF? –  Hans Adler Feb 2 '11 at 12:21
Actually, my font viewer displays the quantifiers in all my fonts, even the most exotic ones, and they tend to not fit into a font's general style. So I guess the font viewer takes them from fall-back fonts without telling me, and they are not actually present in my version of DejaVu Sans Mono. This page confirms that the quantifiers are not present in the font: xahlee.org/emacs/emacs_unicode_fonts.html Still looking for one that works, preferably with serifs. –  Hans Adler Feb 2 '11 at 12:31
DejaVu Sans Mono does contain ∀ and ∃, see the coverage table (page 24) or this page. I've added a screenshot of the result. –  Philipp Feb 2 '11 at 13:29

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

-
Thanks! I completely forgot about \mathtt. I am not completely happy with this because it's not fixed-width: In particular the parentheses are too narrow and the \land is even spaced as an operator. But I guess I can combine this with \texttt and create special commands for the operators to get the spacing approximately right. –  Hans Adler Feb 2 '11 at 11:09