\arg in \spfjust problem on newsproof branch

[kohlhase]

In MathHub/MiKoMH/GenCS/source/pl0/mod/HilbertCalc-deduction-thm.en.tex, I have

      \spfstep{
        $\livar\bC{i}$ is inferred by $\MPRule$ from $\livar\bC{j}$ and
         $\livar\bC{k}=\limpl{\livar\bC{j}}{\livar\bC{i}}$
         \spfjust[method=MPrule]{$\MPRule$ from
           \arg{$\livar\bC{j}$} and
           \arg{$\livar\bC{k}=\limpl{\livar\bC{j}}{\livar\bC{i}}$}
         } for
         $\natlessthan{j,k}i$.
      }

and that gives me brackets errors.

./HilbertCalc-deduction-thm.en.tex:68: Missing $ inserted.
<inserted text> 
                $
l.68       }

./HilbertCalc-deduction-thm.en.tex:68: Missing } inserted.
<inserted text> 
                }
l.68       }

./HilbertCalc-deduction-thm.en.tex:68: LaTeX Error: \mathbf allowed only in math mode.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
 ...                                              

l.68       }

./HilbertCalc-deduction-thm.en.tex:68: Extra }, or forgotten $.
<recently read> }

l.68       }

./HilbertCalc-deduction-thm.en.tex:68: Extra }, or forgotten $.
<argument> ...$ from \arg {$\livar \bC {j}$} and }
                                                   for $\natlessthan {j,k}i$. 
l.68       }

./HilbertCalc-deduction-thm.en.tex:68: Missing $ inserted.
<inserted text> 
                $
l.68       }

./HilbertCalc-deduction-thm.en.tex:68: Missing } inserted.
<inserted text> 
                }
l.68       }

The problem seems to the be two \arg, when I comment them out, things run through.

[Jazzpirate]

\spfjust[method=MPrule]{$\MPRule$ from
           \arg{$\livar\bC{j}$} and

Yes, this is wrong syntax. \arg is only allowed in the argument of a semantic macro that takes arguments. What you probably meant was something like \spfjust{\MPRule{\comp{Modus Ponens} from \arg{$\livar...$} and \arg{...} ...}} (assuming \MPRule takes two arguments).

...note, that $\MPRule$ is also an error then (missing arguments). If \MPRule does not take arguments, \arg makes little sense...