\documentclass[a4paper]{article} \usepackage{bussproofs} \usepackage{savetrees} \usepackage{amsmath} \newcommand{\using}[2]{\AxiomC{}\RightLabel{#1}\UnaryInfC{#2}} \newcommand{\assume}[1]{\AxiomC{#1}} \newcommand{\closed}[2]{\AxiomC{$\left[\text{#2}\right]^\text{#1}$}} \newcommand{\impli}[2]{\RightLabel{$\rightarrow$I,#1}\UnaryInfC{#2}} \newcommand{\imple}[1]{\RightLabel{$\rightarrow$E}\BinaryInfC{#1}} \newcommand{\disji}[1]{\RightLabel{$\lor$I}\UnaryInfC{#1}} \newcommand{\disje}[2]{\RightLabel{$\lor$E,#1}\TrinaryInfC{#2}} \newcommand{\conji}[1]{\RightLabel{$\land$I}\BinaryInfC{#1}} \newcommand{\conje}[2]{\RightLabel{$\land$E,#1}\BinaryInfC{#2}} \newcommand{\univi}[1]{\RightLabel{$\forall$I}\UnaryInfC{#1}} \newcommand{\unive}[1]{\RightLabel{$\forall$E}\UnaryInfC{#1}} \newcommand{\exisi}[1]{\RightLabel{$\exists$I}\UnaryInfC{#1}} \newcommand{\exise}[2]{\RightLabel{$\exists$E,#1}\BinaryInfC{#2}} \begin{document} \begin{prooftree} \closed{1}{$Px \rightarrow Qs$} \assume{$Px$} \imple{$Qs$} \impli{1}{$(Px \rightarrow Qs) \rightarrow Qs$} \end{prooftree} \begin{prooftree} \using{LEM}{$P \lor \lnot P$} \closed{1}{$P$} \disji{$P \lor Q$} \closed{1}{$\lnot P$} \UnaryInfC{$\vdots$} \UnaryInfC{$P \lor Q$} \disje{1}{$P \lor Q$} \end{prooftree} \begin{prooftree} \assume{$A$} \assume{$B$} \conji{$A \land B$} \assume{$A \rightarrow B \rightarrow C$} \closed{1}{$A$} \imple{$B \rightarrow C$} \closed{1}{$B$} \imple{$C$} \conje{1}{$C$} \end{prooftree} \begin{prooftree} \assume{$\exists x Px$} \using{Lemma}{$\forall x (Px \rightarrow Qx)$} \unive{$Px \rightarrow Qx$} \closed{1}{$Px$} \imple{$Qx$} \exisi{$\exists x Qx$} \exise{1}{$\exists x Qx$} \univi{$\forall y \exists x Qx$} \end{prooftree} \end{document}