1

Using prooftrees.sty (https://ctan.org/pkg/prooftrees), is there an option or hack to obtain a line numbering scheme different from the default one?

I would like to format truth trees that match the output of https://www.umsu.de/logik/trees/ (direct link to an example: https://www.umsu.de/logik/trees/?f=(p\lor%20(q\land%20r))\to%20((p\lor%20q)\land%20(p\lor%20r))).

The only relevant difference is that in prooftrees, any two new expressions resulting from a branching rule are labelled with the same line number, whereas umsu.de, in line with certain logic textbooks, assigns two different “line” numbers (or, rather, “expression” numbers). In addition, it should be possible to assign checkmarks to individual expressions rather that wholesale to lines (which might contain any number of different expressions only one of which is usually supposed to be marked).

I do realize that line numbering can be influenced by inserting move by=1, but then the expressions resulting from a branching rule are no longer in the same horizontal position.

  • Welcome! Please do not rely on external links. Instead, post the code for a small document demonstrating the issue here. If prooftrees is assigning checkmarks to lines rather than wffs, that's a bug. It makes no sense to assign them to lines (in any system I'm aware of - maybe there's one out there). So it should not do that. However, there is no option to assign multiple numbers to the same line. If you want different numbers, you need to put the wffs on different lines and then they'll get different numbers, of course. O/w you need to change prooftrees code to do what you want. – cfr Jan 28 '18 at 4:27
  • Trees of the kind shown in the link can be drawn with regular forest. There is no problem here of the kind prooftrees is designed to solve. Basically, everything can go in nodes with the wffs. So just don't use prooftrees would be my advice, since, by using it, you are requesting that stuff get handled separately and moved around - which is explicitly want you don't want. – cfr Jan 28 '18 at 4:38
1

It would indeed be bad if prooftrees added checks to lines rather than wffs. However, it does not do that. Checks are added with either

content+'={\ \forestregister{check with}#1},

or

+content'={\forestregister{check with}#1\ },

depending on whether the checks are to go left or right. Either way, this is manipulating the content of the node containing the wff. The only case in which this constitutes an entire line is one in which that wff constitutes the entire line.

While I can't rule out having done something bizarre, I cannot currently see how I can have introduced a bug of the kind described: this part of the code is very simple. All it does is manipulate the node content i.e. appends or prepends to the particular wff. Until I see an example to the contrary, therefore, as far as I know, prooftrees is guilty of no such indiscretions.

I'm sure there are plenty of other bugs, so if you'd like to report one of those, please do so. I'm just sceptical about the existence of this particular one.

prooftrees provides no option to draw tableaux of the kind shown in the link. These trees do not present the problems prooftrees was designed to solve, so the package has nothing to do here. Basically, they are structured just like linguists' trees: everything goes with the wff - number, wff, justification, checks etc. All you need here is one of the linguists' tree-drawing packages and just put everything in the node.

For example, you could use forest, which is the base for prooftrees, directly. That way, you aren't using something which will be trying to solve a problem you don't have.

You could use prooftrees in the same way and just switch off numbering and justifications. However, this just really adds another layer of code and will only slow compilation down to no useful purpose.

So I would just use forest here.

For example, a couple of custom toks and styles are all you really need here.

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    for tree={math content},
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad ##1\quad ##3} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

produces a linguist-friendly tableau:

linguist-friendly tableau

The only disadvantage, really, is the loss of the cross-referencing for justifications. If you need that, you could borrow the code from prooftrees. However, there is less reason to use that here, because things don't need to get moved around, so there are fewer advantages to automating it. There are still some, but they may not be worth the trouble.

  • prooftrees provides no option to draw tableaux of the kind shown in the link.” – Many thanks, that’s all I wanted to know. I’ll try forest then. – Nick Bart Jan 28 '18 at 9:54
  • @NickBart Does it really add checks to lines for you? Can you give me an example? It really shouldn't and I can't see how it can, so it is hard to fix if it is really a bug. – cfr Jan 28 '18 at 21:17
  • @NickBart Please see example above. You just need a simple style, I think, and you can get what you need pretty easily. Also, this will compile much faster than if you use prooftrees. forest is slow, but prooftrees is far slower. – cfr Jan 28 '18 at 22:32
  • Many thanks for your example; that’s precisely what I was looking for. Also, I never wanted to claim there’s a bug in prooftrees, I just wished to clarify the exact layout I had in mind. – Nick Bart Jan 30 '18 at 12:50
  • @NickBart But the behaviour you described is a bug if prooftrees really does it. It should not be putting checks on lines rather than with individual wffs at all. Could you clarify whether you actually have an example where it applies it to a whole line rather than a particular wff? I'm glad the example helped, in any case. – cfr Jan 30 '18 at 23:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.