# 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, ...) – J Fabian Meier Nov 26 '15 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. – Florian Nov 26 '15 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. – crocket Nov 26 '15 at 9:26
• Of course it's possible. The only question is: which way is the most appropriate? – Alenanno Nov 26 '15 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. – Florian Nov 26 '15 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? – crocket Nov 26 '15 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. – egreg Nov 26 '15 at 11:15