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 Binding, Formal Aspects of Computing 13(2002)341-363.
See Andy Pitts' FreshML pages for more information.
I designed a font (in METAFONT) which provides this quantifier in a weight which matches that of the conventional quantifiers \forall and \exists. It also has the freshness relation symbol "#".
The font files and sample document are now available on github as a ZIP file or git repo.
Please contact me on keithw AT lochan DOT org or via github if you have any questions.
Keith Wansbrough, 2014-05-08.