Distinguish math symbols in the language and the meta-language

Question

I'm writing some notes on logic and formal languages, and I would like to provide some visual cues to distinguish symbols in the formal language (e.g. predicate and logic symbols), from symbols in the meta-language.

For example, something like:

where the proposition p, the brackets, and the implication arrows are all part of the formal language; while F1 is more like a placeholder saying (in the meta-language) that you can insert there any formula from the language.

Now, I can achieve this effect with the following code:

\documentclass{article}
\usepackage{xcolor}

\definecolor{string}{Hsb}{330,0.8,1}
\definecolor{meta-string}{Hsb}{330,0.8,0.6}
\newcommand\lthen{\rightarrow}

\begin{document}

$\textcolor{string}{\mathsf{p} \lthen (\textcolor{meta-string}{F_1} \lthen \mathsf{p})}$

\end{document}

But, of course, it will soon get tedious to write all of that code all the time, so I need to write some macros. And this is where I'm struggling to find the “best” abstraction and more convenient interface to simplify the typing of the code.

One possibility is to define some marcos so that I can type something like:

\formal{\symb{p} \lthen (\meta{F_1} \lthen \symb{p})}

This is straightforward to implement, but I still think this is too much to type since I have to explicitly assign a “type/class” to each symbol in the string.

Another possibility would be to define some macros so that I can type something like:

\formal{p \lthen (\meta{F_1} \lthen p)}

to get the desired effect. Semantically this also feels very right, but I have no idea how to implement it. (In particular if I make \formal select \mathsf for the whole formula, I don't know how to “reset-it” to normal math fonts in \meta, \mathit doesn't work because it also applies the format to the subscript 1.)

Finally the ideal would be to set things up so that \formal auto-magically determines the right font and color for each symbol, so that I can just type

\formal{p \lthen (F_1 \lthen p)}

and get the desired result. It could assume, for example, that lowercase letters are symbols in the language, while uppercase are in the meta-language. Or maybe I just have to explicitly specify which symbols have which type once and the beginning of the document, either way would be fantastic.

So my question is, how can implement one of these interfaces? Or is there another option, perhaps easier to implement, which I haven't thought of?

Answer 1

It might not be quite the official interface but you can reset to the normal font regime with fam=-1

\documentclass{article}
\usepackage{xcolor}

\definecolor{string}{Hsb}{330,0.8,1}
\definecolor{meta-string}{Hsb}{330,0.8,0.6}
\def\formal#1{\mathsf{\color{string}#1}}
\def\meta#1{\begingroup\fam-1 \color{meta-string}#1\endgroup}

\newcommand\lthen{\rightarrow}

\begin{document}

$\textcolor{string}{\mathsf{p} \lthen (\textcolor{meta-string}{F_1} \lthen \mathsf{p})}$

$\formal{p \lthen (\meta{F_1} \lthen p)}$
\end{document}

Answer 2

This is a rather slow (but not so much it becomes really noticeable) implementation of your last idea:

\documentclass{article}
\usepackage{amsmath,sansmath,xcolor}
\definecolor{string}{Hsb}{330,0.8,1}
\definecolor{meta-string}{Hsb}{330,0.8,0.6}
\newcommand\lthen{\rightarrow}

\makeatletter
\def\change@code@lc#1\relax{%
  \mathcode#1=\string"8000
  \begingroup\lccode`~=#1
  \lowercase{\endgroup\def~}{\text{\normalfont\sffamily\char#1}}%
}
\def\change@code@uc#1\relax{%
  \mathcode#1=\string"8000
  \begingroup\lccode`~=#1
  \lowercase{\endgroup\def~}{%
    \text{\normalfont\sffamily\slshape\color{meta-string}\char#1}%
    \@ifnextchar_\@uc@subscript{}}%
}
\def\@uc@subscript_#1{_\text{\color{meta-string}$#1$}}

\protected\def\formal{%
  \hbox\bgroup
  \count@=\numexpr`a-1\relax
  \loop\ifnum`z>\count@
  \advance\count@\@ne
  \expandafter\change@code@lc\number\count@\relax
  \repeat
  \count@=\numexpr`A-1\relax
  \loop\ifnum`Z>\count@
  \advance\count@\@ne
  \expandafter\change@code@uc\number\count@\relax
  \repeat
  \@formal
}
\def\@formal#1{\sansmath\color{string}$#1$\egroup}
\makeatother

\begin{document}
\formal{p \lthen (F_1 \lthen p)}

\begin{align}
&\formal{A\lthen b}\\
&\formal{C\lthen D}
\end{align}
\end{document}

The align is just to show that it works (to a limited extent) also in alignments: the argument to \formal cannot contain a & for the alignment.

Answer 3

Regarding your last idea:

It is not very difficult to use for certain symbols/letter another font. E.g. here for the p:

\documentclass{article}
\usepackage{xcolor}
\newcommand\lthen{\rightarrow}
\DeclareSymbolFont{formalletters}{OT1}{cmss}{m}{n}
\DeclareMathSymbol{p}\mathalpha{formalletters}{"70}
\begin{document}
$p \lthen (F_1 \lthen p)$
\end{document}

But it is difficult to add colors in this case.

This is easier with xelatex/lualatex as there you can add color directly to the font:

\documentclass{article}
\usepackage{xcolor}
\usepackage{unicode-math}
\setmathfont[Color=00FF00]{lmodern-math.otf}
\ExplSyntaxOn
%\bool_set_true:N  \g_um_uplatin_bool %for upright p
\ExplSyntaxOff
\setmathfont[range={"61-"7A, %a-z
                    "02192, %\rightarrow
                    "00028-"00029% parentesis
                    },
             Color=FF0000]{lmodern-math.otf}
\newcommand\lthen{\rightarrow}
\begin{document}
$p  \lthen (F_1 \lthen p)$

\end{document}

(The name for the lm modern math font can differ on your system). If you need beside your "formal math" also normal math you can (probably as I didn't test) set up a \mathversion for the "formal math".