2

I have a problem with

\infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

I have looked at this answer but couldn't find it helpful

3
  • 3
    \infer already switches to math mode, you need no $ : \documentclass{article} \usepackage{amsmath} \usepackage{proof} \begin{document} \infer{\forall x\in A. P(x)}{\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)} \end{document} works out of the box.
    – user194703
    Jan 3, 2020 at 16:53
  • Thank you, it worked!
    – brj
    Jan 3, 2020 at 18:40
  • Welcome to TeX.SE! Jan 3, 2020 at 20:25

2 Answers 2

3

Answer:

  • In this case, \infer (from the proof package) expects its arguments to be formulas, so it already surrounds its arguments with dollar signs. You should remove the extra ones you added.

  • General tip: Always interpret “Missing $ inserted” as “TeX encountered the following math-mode thing when it was not in math mode”, and first try to figure out why TeX was not in math mode. (Sometimes it's really a missing dollar sign, but in this case, it's because it had just exited math mode, because of the “extra” dollar sign.)


More detailed answer on TeX error messages and debugging:

Although the error message looks very weird at first glance, in principle everything makes sense from the error output, especially if you add \tracingall and know what to look for.

\documentclass{article}
\usepackage{amsmath} 
\usepackage{proof} 
\begin{document} 

\tracingall
\infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

In your input above you have \infer followed by two things in braces: the first is

{$\forall x\in A. P(x)$}

and the second is

{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

The output with \tracingall reveals that this \infer results, after enough steps, in TeX trying to expand an internal command \@infer [#1]#2#3 in which

#1<-\@empty 
#2<-$\forall x\in A. P(x)$
#3<-$\forall x\in A.(\forall y\in A.x\xrightarrow {+}y\implies P(y))\implies P(x)$

This is a bit higher up than the final error message, which is:

! Missing $ inserted.
<inserted text> 
                $
<to be read again> 
                   \forall 
<argument> $\forall 
                    x\in A. P(x)$
\@infer [#1]#2#3->\relax \if@ReturnLeftOffset \else \@SavedLeftOffset =\@LeftOffset \fi \setbox \@LabelPart =\hbox {$#1$}\relax \setbox \@LowerPart =\hbox {$#2
                                                                                                                                                               $}\relax \global \@LeftOffset =0pt \setbox \@UpperPart =\vbox {\tabskip =0pt \halign {\relax...
l.7 \infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

? 

This shows that the definition of this \@infer is:

\@infer [#1]#2#3->\relax \if@ReturnLeftOffset \else \@SavedLeftOffset =\@LeftOffset \fi \setbox \@LabelPart =\hbox {$#1$}\relax \setbox \@LowerPart =\hbox {$#2
                                                                                                                                                              $}\relax \global \@LeftOffset =0pt \setbox \@UpperPart =\vbox {\tabskip =0pt \halign {\relax...

(the ... at the end of the last line above means the definition is not yet complete!) in which, while carrying out the command \hbox {$#2$} (where #2 will be substituted when encountered), what happens is:

  • First, TeX sees \hbox and enters restricted horizontal mode.

  • Then it sees $ (which came from the definition of \@infer) and enters math mode (and does some stuff, like changing font family and executing whatever is in \everymath).

  • Then it sees #2 and substitutes its definition $\forall x\in A. P(x)$.

  • So when it sees the first character $, it leaves math mode.

  • Then it sees \forall, which at this point has the definition \mathchar"238.

  • This \forall (\mathchar"238) can only be in math mode, so TeX "helpfully" inserts a $ sign before reading it (to enter math mode), but only tentatively: it also “helpfully” lets you know (before going ahead to act on this $ that it inserted) what it's about to do, in case you want to change what's going to happen.

This explains the error message, which consists of a message followed by pairs of lines denoting the input stack:

! Missing $ inserted.

^ The error message.

<inserted text> 
                $

^ First level of the input stack: TeX is about to read a $ that it inserted, and is letting you know.

<to be read again> 
                   \forall 

^ Second level of the input stack: There's a \forall that TeX had read earlier and has put back (when it encountered the error), which it will read again next (if you allow it to).

<argument> $\forall 
                    x\in A. P(x)$

^ Third level of the input stack: While reading an argument $\forall x\in A. P(x)$ (this is an argument of a macro that will be shown next), TeX has finished reading up to the $\forall, and is yet to read x\in A. P(x)$.

\@infer [#1]#2#3->\relax \if@ReturnLeftOffset \else \@SavedLeftOffset =\@LeftOffset \fi \setbox \@LabelPart =\hbox {$#1$}\relax \setbox \@LowerPart =\hbox {$#2
                                                                                                                                                               $}\relax \global \@LeftOffset =0pt \setbox \@UpperPart =\vbox {\tabskip =0pt \halign {\relax...

^ Fourth level of the input stack: The macro that TeX was expanding, when it encountered the argument. Note that here you can see that it has just read \hbox{$#2 and this is the clue to what's going on.

l.7 \infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

^ Fifth level of the input stack: The line 7 from your source file, that TeX had read.

? 

^ Prompt, asking you how to proceed. If you hit Enter, it will read $ then \forall then x\in A. P(x)$ (from the first three levels of the stack) then continue reading the fourth level of the stack starting at $ (which will cause another error).


As an aside, it is interesting (as an idle exercise of imagination) to speculate what sort of design or user conventions would have prevented such unhelpful (at least at first glance) error messages, for a more pleasant user experience. My flippant answer would be to not use too many macros. :) But more seriously, perhaps some sort of way for packages to specify that a certain argument of a macro is supposed to be a formula or not, and for that to be checked first (before being fed into the innards of TeX) would help. Not sure if expl3 provides this. Another thing that may help is some sort of interactive/slow-motion display of what TeX is doing (something better than \tracingall which takes some experience to understand), so that you could have seen that TeX has entered math mode because of \infer, and has left math mode because of your $, before encountering the \forall.

1

As pointed out by @Schrödinger's cat in the comments, the fix is to not use $..$ when already inside \infer as it switches to math mode

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .