# Can I typeset a proof tree in exercise 2.4.3(c) from mathematical logic by ian chiswell and wilfrid hodges(2007) with tex?

The picture below is exercise 2.4.3(c).

• You should add what you have looked up and tried so far (pstricks, tikz, ...) Commented Nov 26, 2015 at 9:14
• by the looks of the picture, the book actually is typeset with TeX. People here are very helpful, but even more so when they get the impression that you've already put some effort in solving the problem yourselv, e.g. by showing your (unsuccessful) attempts. Commented Nov 26, 2015 at 9:17
• I haven't learned Tex or LaTex yet. But, I want to know if it's "possible" to typeset the above picture with Tex/LaTex.
– user82730
Commented Nov 26, 2015 at 9:26
• Of course it's possible. The only question is: which way is the most appropriate? Commented Nov 26, 2015 at 9:36
• It is possible but a bit advanced. If you don't know any LaTeX yet, it is definitely not worth learning it, just for the sake of one tree. But if you are planning to work extensively in this or similar fields, it's probably a really good idea to get going with a good LaTeX-introduction and get back to trees after a while. Commented Nov 26, 2015 at 9:48

There are several packages to draw proof trees in LaTeX, e.g., bussproofs, ebproof,prftrees. Here is a solution using bussproofs to draw the proof tree and cancel to slash one of the assumption.

\documentclass[11pt]{article}
\usepackage{bussproofs}
\usepackage{cancel}
\begin{document}
\begin{prooftree}
\noLine
\UnaryInfC{$\cancel\psi$}
\AxiomC{$\phi\wedge\psi$}
\RightLabel{($\wedge$E)}
\UnaryInfC{$\phi$}
\RightLabel{($\wedge$I).}
\insertBetweenHyps{\hskip2cm}
\BinaryInfC{$(\psi\wedge\phi)$}
\LeftLabel{\textcircled{\scriptsize 1}}
\RightLabel{($\rightarrow$I)}
\UnaryInfC{$(\psi\rightarrow(\psi\wedge\phi))$}
\end{prooftree}
\end{document}


Resulting in

With ebproof the same proof tree can be achieved with the following code

\documentclass[11pt]{article}

\usepackage{ebproof}
\usepackage{cancel}

\begin{document}
\begin{prooftree}[template=$\inserttext$]
\Infer[no rule]1{\cancel\psi}
\Hypo{(\phi\wedge\psi)}
\Infer1[($\wedge$E)]{\phi}
\Infer[separation=2cm]2[($\wedge$I)]{(\psi\wedge\phi)}
\Infer[left label=\textcircled{\scriptsize 1},
right label=($\rightarrow$I)]1{(\psi\rightarrow(\psi\wedge\phi))}
\end{prooftree}

\end{document}


With the help of bussproofs and cancel:

\documentclass{article}
\usepackage[T1]{fontenc}
\usepackage{bussproofs}
\usepackage{cancel}

\newcommand{\lto}{\mathbin{\to}}

\begin{document}

\begin{prooftree}
\renewcommand{\defaultHypSeparation}{\hspace{4em}}
\AxiomC{${\cancel{\psi}}^{\,\raisebox{\depth}{\textcircled{\footnotesize 1}}}$}
\AxiomC{$(\phi\land\psi)$}
\RightLabel{($\land\mathrm{E}$)}
\UnaryInfC{$\phi$}
\RightLabel{($\land\mathrm{I}$)}
\BinaryInfC{$(\psi\land\phi)$}
\LeftLabel{\textcircled{\footnotesize 1}}
\RightLabel{($\lto\mathrm{I}$)}
\UnaryInfC{$(\psi\lto(\psi\land\phi))$}
\end{prooftree}

\end{document}


• Did you type the tex code by hand? or did you use a GUI frontend?
– user82730
Commented Nov 26, 2015 at 11:10
• @crocket Just some lookup in the manual of bussproofs. No, there's no front-end for this, as far as I know. But, as you see, the syntax is not bad. Commented Nov 26, 2015 at 11:15