I provide the following MWE regarding the construction of a semantic tableaux for modal logic.
\documentclass[a4paper,twoside,10pt]{memoir}
\usepackage{alphabeta}
\usepackage {tikz}
\usepackage {forest}
\usetikzlibrary {positioning,graphs}
\usepackage{graphicx}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{mathtools}
\begin{document}
\begin{forest}
[$F(\Box A\wedge\Box B)\rightarrow\Box(A\wedge B)$, name=root, tikz={\node [draw,red,fit=(!1)(!ll)] {};}
[ $T(\Box A\wedge\Box B)$, name=nodeA [ $F\:\Box(A\wedge B)$, name=nodeB, tikz={\node [draw,red,fit=(!1)(!ll)] {};}
[ $T\Box A$, name=nodeC [ $T\:\Box B$, name=nodeD [ $F(A\wedge B)$, name=nodeE
[ $FA$, rectangle, draw [ $TA$, rectangle, draw, name=nodeF [ $\otimes$ ] ] ]
[ $FB$, rectangle, draw [ $TB$, rectangle, draw, name=nodeG [ $\otimes$ ] ] ] ] ] ] ] ] ]
\draw[->] (nodeA) to [out=west, in=west] (nodeC);
\draw[->] (nodeB) to [out=east, in=east] (nodeE);
\end{forest}
\end{document}
I need to improve the drawing of the arrows .. the main issue, is to use the nodes enclosed in the second rectangle as a single (virtual) node, and draw the tip (namely, the end) of the left arrow (starting from the second node), in the middle of the left vertical side of the second rectangle ... it would also be great, if the arrows did not intersect the borders of the rectangles (but this is a secondary and not so important issue)..