1. The problem
It is standard to use corner quotes in denoting Gödel numbers. The simple way of setting corner quotes in LaTeX is as follows:
| $\ulcorner\phi\urcorner$ is the G\”odel number of $\phi$. |
 |
This usually works just fine. But suppose (to follow another standard convention) that we also use corner quotes round a (metalinguistic) designator for n to signify the Gödel number for the standard formal numeral for the number n. So …
| $\ulcorner 2^2 \urcorner = \ulcorner \mathsf{SSSS0} \urcorner$ |
 |
The setting of the corner quotes on the left of the equation is ugly. We’d like to raise them to the height of the exponent.
And if we need to set a lot of corner-quoted expressions, we’d also like to define a snappier command to cut down keystrokes. So, we’d like to be able to type something like below to get the result displayed.
| $\Godelnum{2^2} = \Godelnum{\mathsf{SSSS0}}$ |
 |
2. One solution
Use Sam Buss’s nice macro. Simply paste into your document preamble the following:
\newbox\gnBoxA
\newdimen\gnCornerHgt
\setbox\gnBoxA=\hbox{$\ulcorner$}
\global\gnCornerHgt=\ht\gnBoxA
\newdimen\gnArgHgt
\def\Godelnum #1{%
\setbox\gnBoxA=\hbox{$#1$}%
\gnArgHgt=\ht\gnBoxA%
\ifnum \gnArgHgt<\gnCornerHgt \gnArgHgt=0pt%
\else \advance \gnArgHgt by -\gnCornerHgt%
\fi \raise\gnArgHgt\hbox{$\ulcorner$} \box\gnBoxA %
\raise\gnArgHgt\hbox{$\urcorner$}}
Exactly as we wanted, in math mode,
\Godelnum{…}
sets the contents of the brackets between corner quotes (positioned so their top edges are level with the top of the box containing the contents).
When single letters or symbols are to be set in corner quotes, you can of course drop the brackets, thus
\Godelnum A, \Godelnum \phi, …
3. Another solution
An alternative solution is proposed here by Heiko Oberdiek, and has been recommended as giving preferable spacing. Putting it together with a check whether MnSymbol is already loaded and adding a different definition of the command \Godelnum (thanks to Peter Gerdes) we get:
\makeatletter
\RequirePackage{ltxcmds}
\ltx@ifpackageloaded{MnSymbol}{}{
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{MnLargeSymbols}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{MnLargeSymbols}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
<-6> MnSymbolE5
<6-7> MnSymbolE6
<7-8> MnSymbolE7
<8-9> MnSymbolE8
<9-10> MnSymbolE9
<10-12> MnSymbolE10
<12-> MnSymbolE12
}{}
\DeclareFontShape{OMX}{MnSymbolE}{b}{n}{
<-6> MnSymbolE-Bold5
<6-7> MnSymbolE-Bold6
<7-8> MnSymbolE-Bold7
<8-9> MnSymbolE-Bold8
<9-10> MnSymbolE-Bold9
<10-12> MnSymbolE-Bold10
<12-> MnSymbolE-Bold12
}{}
\DeclareMathDelimiter{\ulcorner}
{\mathopen}{MnLargeSymbols}{‘036}{MnLargeSymbols}{‘036}
\DeclareMathDelimiter{\urcorner}
{\mathclose}{MnLargeSymbols}{‘043}{MnLargeSymbols}{‘043}
}
\newcommand*{\Godelnum}[1]{\left\ulcorner #1 \right\urcorner}
\makeatother