[Tex/LaTex] How to typeset this parsing tree for propositional logic formula with forest or something else

Question

The following parsing tree is from Mathematical Logic published in 2007 and written by Ian Chiswell & Wilfrid Hodges. It looks like a forest tree, but I guess it could be typeset better by another package. How shall I typeset this?

Answer 1

Using more-or-less the formulae kindly transcribed from the do-it-for-me image by egreg when the OP failed to provide any help whatsoever, together with a tweaked version of the tableaux style I developed for this answer, I drew a version of the tree using Forest as follows. For the record, I think I ought not answer this question but I'm giving in to my fascination with trees.

\documentclass[border=5pt,tikz,multi]{standalone}
\usepackage{forest}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\forestset{%
  declare toks={wff}{},
  declare toks={cyswllt}{},
  declare toks register={nod safonol},
  nod safonol=\circ,
  dosbarthu/.style={%
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
      inner sep=0pt,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      delay={%
        content'/.register=nod safonol,
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{wff()},
        if={strequal(cyswllt(),"")}{cyswllt/.option=wff}{},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{cyswllt()},
      },
      if={n_children("!parent")==1}{%
        before packing={calign with current edge},
      }{%
        if n=1{%
          before packing={%
            !parent.calign primary child/.process args={O}{n},
          },
        }{%
          before packing={%
            !parent.calign secondary child/.process args={O}{n},
          },
       }
      }
    },
  }
}
\begin{document}
\begin{forest}
  dosbarthu
  [
    [, wff=((\lnot(p_1\lif(\lnot p_0)))\lif p_0), cyswllt=\lif
      [, wff=(\lnot(p_1\lif(\lnot p_0))), cyswllt=\lnot
        [, wff=(p_1\lif(\lnot p_0)), cyswllt=\lif
          [, wff=p_1]
          [, wff=(\lnot p_0), cyswllt=\lnot
            [, wff=p_0]
          ]
        ]
      ]
      [, wff=p_0]
    ]
  ]
\end{forest}
\end{document}