2

I am using the Clea F. Rees' prooftrees package in order to typeset tableau proofs in LaTeX. Things are working just fine, but there are two caveats I do not know how to deal with. Firstly, the "to prove" line you can specify in a tableau's preamble is left-aligned instead of centered. Secondly. I have not found a way yet to center the "q. e. d." below the last line of a tableau; it is alway misaligned.

How it should look like:

enter image description here

How it looks like at the moment:

enter image description here

Here is my MWE:

\documentclass[leqno,hyperref={pdfpagemode=FullScreen},aspectratio=169]{beamer}
%%% Font %%%

\usepackage[math-style=upright]{unicode-math} % Mathe-Font gerade
\setmathfont{latinmodern-math.otf}            % Latin Modern Math Font

\usepackage{amssymb}
\usepackage[greek, main=ngerman, germanb]{babel}

\usepackage{bussproofs} % für Gentzen-Bäume
\usepackage{tikz} % für Diagramme
\usepackage{forest} % nötig für prooftrees
\usepackage{prooftrees} % für Tableaux

%%%%% Definition der Standardpräambel für Tableaux %%%%%
\forestset{% Hiermit legen wir den Font im Tableaux fest: sans serif ohne italics!
mathsf content/.style={content
format={\noexpand\ensuremath{\noexpand\mathsf{\forestoption{content}}}}}}

\forestset{
default preamble=
{% Beginn der Standardpräambel 
line no sep=5mm, % Abstand Baum - Nummerierung
single branches=true, % auch vertikale Striche werden angezeigt
for tree={mathsf content, s sep'=10mm}, % Wie weit gehen die Striche zur Seite?
close with={$\bigtimes$} % Mit Kreuz schließen
}, %Ende der Standardpräambel 
}

%%% Nummerierung der Tableaux in Klammern  %%%
\renewcommand*\linenumberstyle[1]{(#1)}

\newcommand*{\til}{\ensuremath{\mathbin{{\sim}}}} %  Tilde
\usepackage{turnstile}
\usepackage{adjustbox}
\begin{document}
\begin{frame}{Exercixe 9 -- Solution}
\centerline{zz: $\sststile {PL}{} \forall x Fx \to \exists x Fx$}
\smallskip
\begin{adjustbox}{max totalsize={.9\textwidth}{.7\textheight},center}
\begin{tableau}
{
to prove={\text{zz: }\sststile {PL}{} \forall x Fx \to \exists x Fx}
}
[\til (\forall x Fx \to \exists x Fx), just=reductio-Hypothese
[\forall x Fx,  just=(1) ($\til \text{,}\to$)
[\til \exists x Fx, just=(1) ($\til \text{,}\to$) % Komma muss als Text ausgegeben werden, weil prooftree sonst denkt, es käme ein weiteres Argument!
[\forall x \til Fx,               just=(3) DT
[Fa,               just=(2) \text{US: a/x}
[\til Fa,               just=(4) \text{US: a/x}, , close={(5),(6)}
]
]
]
]
]
]
\end{tableau}
\end{adjustbox}
\centerline{\textit{q. e. d.}}
\end{frame}
\end{document}

I am new to LaTeX. Is there anyone out there willing to help?

1 Answer 1

3

I think the easiest way to do this is just to use tikz to add a node after the tableau is drawn. However, there doesn't seem to be room on the slide. I made room by removing the repetition of the statement to be proved, but you obviously might prefer to make space using some other method (e.g. reducing distances between lines or reducing the font size or using plain or whatever).

\documentclass[leqno,hyperref={pdfpagemode=FullScreen},aspectratio=169]{beamer}
%%% Font %%%

\usepackage[math-style=upright]{unicode-math} % Mathe-Font gerade
\setmathfont{latinmodern-math.otf}            % Latin Modern Math Font

\usepackage{amssymb}
\usepackage[greek, main=ngerman, germanb]{babel}

\usepackage{bussproofs} % für Gentzen-Bäume
\usepackage{prooftrees} % für Tableaux

%%%%% Definition der Standardpräambel für Tableaux %%%%%
\forestset{% Hiermit legen wir den Font im Tableaux fest: sans serif ohne italics!
  mathsf content/.style={content
    format={\noexpand\ensuremath{\noexpand\mathsf{\forestoption{content}}}}}}

\forestset{
  default preamble=
  {% Beginn der Standardpräambel 
    line no sep'=5mm, % Abstand Baum - Nummerierung
    single branches=true, % auch vertikale Striche werden angezeigt
    for tree={mathsf content, s sep'=10mm}, % Wie weit gehen die Striche zur Seite?
    close with={$\bigtimes$} % Mit Kreuz schließen
  }, %Ende der Standardpräambel 
}

%%% Nummerierung der Tableaux in Klammern  %%%
\renewcommand*\linenumberstyle[1]{(#1)}
\newcommand*{\til}{\ensuremath{\mathbin{{\sim}}}} %  Tilde
\usepackage{turnstile}
\begin{document}
\begin{frame}{Exercixe 9 -- Solution}
  \centering
%   \centerline{zz: $\sststile {PL}{} \forall x Fx \to \exists x Fx$}
%   \smallskip\par
  \begin{tableau}
    {
      to prove={\text{zz: }\sststile {PL}{} \forall x Fx \to \exists x Fx}
    }
    [\til (\forall x Fx \to \exists x Fx), just=reductio-Hypothese
    [\forall x Fx,  just=(1) ($\til \text{,}\to$)
    [\til \exists x Fx, just=(1) ($\til \text{,}\to$) % Komma muss als Text ausgegeben werden, weil prooftree sonst denkt, es käme ein weiteres Argument!
    [\forall x \til Fx,               just=(3) DT
    [Fa,               just=(2) \text{US: a/x}
    [\til Fa,               just=(4) \text{US: a/x}, , close={(5),(6)}, name=qedhere, tikz+={\node [anchor=base] at ([yshift=-.5\baselineskip]current bounding box.south -| qedhere.center) {q.\ e.\ d.};}
    ]
    ]
    ]
    ]
    ]
    ]
  \end{tableau}
\end{frame}
\end{document}

tableau with q.e.d. aligned with final wff

3
  • 2
    Lucky me you're reading this! Thank you so much for your solution. Is there a way to do something similar for the to-prove-line, taking the first formula node this time? I also have some beginner's questions, if I may: Could you explain the name=qedhere and tikz+= commands in more detail, please? What exactly is the forest node named "qedhere"? Is there a specific reason you use baselineskip and not vskip? What does the -| do? Commented Apr 3, 2022 at 23:46
  • name is just names the TikZ node. For tikz+ see forest's docs. For -| see TikZ's documentation. You can use something other than \baselineskip, but you couldn't use \vskip because \vskip isn't a length but a command. But you could use 5cm or something. Using \baselineskip means if you change font or font size, the spacing will automatically adjust. In general, it's better to ask a new question if it's substantive as things don't get seen in comments (like this). You can do just the same for the first formula node (or any node) and add arbitrary TikZ stuff with tikz+.
    – cfr
    Commented Jun 18, 2023 at 3:00
  • @VitusSchäfftlein ^^
    – cfr
    Commented Jun 18, 2023 at 3:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .