How to typeset the "freshness quantifier"
The freshness quantifier is the reflected "N" symbol first
introduced in the paper
M. J. Gabbay and A.M. Pitts, A
New Approach to Abstract Syntax with Variable
Aspects of Computing 13(2002)341-363.
So long as you are prepared to convert your DVI output to
Postscript, the simplest way to typeset this symbol using LaTeX
is to use the
\reflectbox command from the graphics package:
The "weight" of this character is heavier than those used for the
conventional quantifiers \forall and
\exists. Keith Wansbrough has designed a font using
METAFONT that gives a freshness quantifer of the correct weight
(and also a special version of the freshness relation symbol,