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?