Logic tree with tikz-tree -- placing nodes on specific places

Question

I am trying to reproduce the following with tikz:

And also:

Regarding the first image I could start with:

\documentclass{article}
\usepackage{tikz-qtree}
\usepackage{tikz-cd}

\tikzstyle{every picture}+=[remember picture]

\begin{displaymath}
((\neg Qb \wedge x (Px \rightarrow Qx)) 
\tikz[baseline]\node (n1)     {$\rightarrow$}; \neg Pb)
\end{displaymath}


\begin{displaymath}
(\neg Qb \wedge \tikz[baseline]\node (n2) {$\forall$};x 
(Px \rightarrow Qx)) \qquad \tikz[baseline]\node (n3) {$\neg Pb$};
\end{displaymath}


\begin{tikzpicture}[overlay]

\draw (n1) -- (n2); 
\draw (n1) -- (n3); 


\end{tikzpicture}

\end{document}

The result, however, is far from elegant, and I do not know how to proceed from that:

Answer 1

For the first tree, if the branches do not need to start from the main logical connectives, then the TikZ-based forest package would be a good option.

The second tree can also be drawn using forest, as if it were growing from bottom to top.

Code

\documentclass{article}
\usepackage{forest}
\renewcommand\b[1]{\textbf{#1}}

\begin{document}
\begin{forest}
  for tree={parent anchor=south,child anchor=north}
  [$((\lnot Qb \wedge \forall x(Px \to Qx)) \to \lnot Pb)$, s=1cm
    [$(\lnot Qb \wedge \forall x (Px\to Qx))$
      [$\lnot Qb$
        [$Qb$]
      ]
      [$\forall x (Px\to Qx)$
        [$(Px\to Qx)$
          [$Px$]
          [$Qx$]
        ]
      ]
    ]
    [$\lnot Pb$
      [$Pb$]
    ]
  ]
  \node[below,red]at(current bounding box.south){Figure: First Tree};
\end{forest}
%
\hskip20pt
%  
\begin{forest}
  for tree={
    child anchor=south,grow'=north,
    edge path={\noexpand\path[\forestoption{edge}](!u.parent anchor)-|(.child anchor)\forestoption{edge label};}
  },
  [\b{V}
    [\b{F}
      [\b{V}[$(C$,no edge]]
      [$\wedge$,no edge,tier=final]
      [\b{F}[$B)$,no edge]]
    ]
    [\b{V},name=n
      [$\to$,no edge,tier=final]
      [,no edge,name=nc
        [$\lnot$,no edge,tier=final]
      ]
      [\b{F}[$D$,no edge,tier=final]]
    ]
  ]
  \draw(n.north)--(nc.north);
  \node[below,red]at(current bounding box.south){Figure: Second Tree};
\end{forest}
\end{document}

Output

Answer 2

I don't know if this is any use as it does not use tikz but here is how I would typeset the first example using the qtree package:

\documentclass{article}
\usepackage{qtree}
\usepackage{amssymb}
\begin{document}
\Tree
  [.{$((\neg Qb \wedge \forall x (Px \rightarrow Qx)) \rightarrow \neg Pb)$}
    [.{$(\neg Qb \wedge \forall x (Px \rightarrow Qx))$}
      [.{$\neg Qb$}
        [.{$Qb$}
        ]
      ]
      [.{$\forall x (Px \rightarrow Qx)$}
        [.{$(Px \rightarrow Qx)$}
          [.{$Px$}
          ]
          [.{$Qx$}
          ]
        ]
      ]
    ]
    [.{$\neg Pb$}
      [.{$Pb$}
      ]
    ]
  ]
\end{document}

Warning: This is NOT correct logically but is, in fact, full of errors. Do not use this if you are learning logic just because it happens to be on a website!

Note that older versions of qtree apparently had issues with pdflatex but the current version is compatible (and I've always used it with pdflatex).