Analytic Tableaux Smullyan's Style

2,338

Solution 1

Here's a forest style, smullyan tableaux. The key closed can be used when the style is active to close the current branch.

One advantage of forest is the concise bracket syntax used to specify trees.

\documentclass[tikz,border=10pt]{standalone}
\newcommand*\lif{\mathbin{\to}}% added thanks to egreg's suggestion
\usepackage{forest}
\forestset{
  smullyan tableaux/.style={
    for tree={
      math content
    },
    where n children=1{
      !1.before computing xy={l=\baselineskip},
      !1.no edge
    }{},
    closed/.style={
      label=below:$\times$
    },
  },
}
\begin{document}
\begin{forest}
  smullyan tableaux
  [\lnot(\lnot(A \land B) \lif (\lnot A \lor \lnot B))
    [\lnot(A \land B)
      [\lnot(\lnot A \lor \lnot B)
        [\lnot\lnot A
          [\lnot\lnot B
            [A
              [B
                [\lnot A, closed]
                [\lnot B, closed]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

Smullyan tableaux

Note that it is more usual in logic, as far as I know, to draw trees so that branches start from a common point:

common branch point

This can be achieved, if necessary, by adding

      parent anchor=south,
      child anchor=north,

to the style.

Solution 2

Here is a simple code with pstricks, and more specifically with pst-tree:

\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{mathtools}
\usepackage{pst-node, pst-tree, auto-pst-pdf}
\def\noedge{\ncline[linestyle = none]}
\renewcommand\psedge{\ncline[arrows =-]}

\begin{document}

\centering
\[ \psset{levelsep=1.2cm, treesep=2cm, nodesepA=10pt, nodesepB=2pt}
    \pstree%
    {\TR[vref =-1.25]{%
        \makebox[0pt]{$ \begin{matrix}\neg(\neg(A\wedge B)\to(\neg A\vee\neg B))\\
            \neg(A\wedge B)\\
            \neg(\neg A\vee\neg B) \\
            \neg\neg A\\
            \neg\neg B\\
            A\\B\end{matrix} $}}}%
    {%
        \TR[vref=1, href=2]{$ \begin{matrix} \neg A\\ \times\end{matrix}$}
        \TR[vref=1, href=-2]{$ \begin{matrix} \neg B\\ \times \end{matrix}$}
        } \]
\end{document} 

enter image description here

Share:
2,338

Related videos on Youtube

Matteo
Author by

Matteo

Updated on August 01, 2022

Comments

  • Matteo
    Matteo over 1 year

    Is there a simple and intuitive way to drawn with latex this kind of tree?

    I tried to check in the site "LATEX for LOGICIANS", but I can't find this kind of tree, with this kind of layout. Thank you

    • Thruston
      Thruston almost 8 years
      Section 4 of the LaTeX for Logicians site appears to have exactly this type of tree.
    • Matteo
      Matteo almost 8 years
      I saw it, but I would like to find the latex code of that kind of type...
    • cfr
      cfr almost 8 years
      Well, if you look at the packages listed on that page, you will find plenty of examples. There are also examples on this site. This is just standard. You don't even need numbers or labelling, which is where the complications begin.
  • Bernard
    Bernard almost 8 years
    You're welcome. Always glad to help!
  • egreg
    egreg almost 8 years
    I usually define \newcommand{\lto}{\mathbin{\to}} so the arrow is treated as a binary operation (which it is, in this case).
  • cfr
    cfr almost 8 years
    @egreg I don't think it is really the correct arrow. When I had to draw these, I was using the horseshoe so it wasn't a problem.
  • cfr
    cfr almost 8 years
    @egreg Is that better? I think \lif is better than \lto because it can be redefined to \supset if necessary. (I know \lto could be also, but \lif is semantic whereas \lto is format.)