\documentclass{article}

\input{prooftree}

\newcommand{\arr}{{\rightarrow}}
\newcommand{\imp}{{\rightarrow}}
\newcommand{\oftype}{{:}}
\newcommand{\FV}{\mbox{FV}}

\begin{document}

Derivation rules for minimal prpositional logic, $\sigma$ and $\tau$ are propositions.

$$\begin{array}{ccc}
\begin{prooftree}
\sigma\arr\tau\:\:\:\: \sigma
\justifies
\tau
\using{\arr\mbox{-E}} 
\end{prooftree}
&\:&
\begin{prooftree}
\begin{array}{c}
[\sigma]^j\\ 
\vdots\\
 \tau
\end{array}
\justifies
\sigma\arr\tau 
\using{^{[j]} \arr\mbox{-I}} 
\end{prooftree}
\end{array}$$



An example derivation with nested prooftrees.
$$
\begin{prooftree}
{
\begin{prooftree}
[\alpha\arr\beta\arr\gamma]^3\:\: [\alpha]^1
\justifies
\beta\arr\gamma
\end{prooftree}
\:\:
\begin{prooftree}
[\alpha\arr\beta]^2\:\: [\alpha]^1
\justifies
\beta
\end{prooftree}
}
\justifies
\begin{prooftree}
\begin{prooftree}
\begin{prooftree}
\gamma
\justifies 
\alpha\arr\gamma
\using 1
\end{prooftree}
\justifies 
(\alpha\arr\beta)\arr \alpha\arr\gamma
\using 2
\end{prooftree}
\justifies
(\alpha\arr\beta\arr\gamma)\arr (\alpha\arr\beta)\arr \alpha\arr\gamma
\using 3
\end{prooftree}
\end{prooftree}
$$

A definition of a set of derivation rules.

$$\begin{array}{lll} 
%\hoog{1.5em}
(\mbox{axiom}) 
& 
%\prooftree
%\justifies
\Delta \vdash \phi
%\endprooftree 
& \mbox{if }\phi\in\Delta\\
&&\\
\vspace{-.2cm}
(\imp\mbox{-introduction})
& 
\prooftree
\Delta \cup{\phi} \vdash \psi
\justifies
\Delta \vdash \phi\imp \psi
\endprooftree&\\
&&\\
\vspace{-.2cm}
(\imp\mbox{-elimination})
& 
\prooftree
\Delta\vdash \phi\imp\psi\;\;\Delta \vdash \phi
\justifies
\Delta \vdash\psi
\endprooftree &\\
&&\\
\vspace{-.2cm}
(\forall\mbox{-introduction})
&
\prooftree
\Delta \vdash \phi
\justifies
\Delta \vdash \forall x\oftype {\sigma}.\phi
\endprooftree & \mbox{if }x\oftype {\sigma} \notin \FV(\Delta)\\
&&\\
\vspace{-.2cm}
(\forall \mbox{-elimination})
& 
\prooftree
\Delta \vdash \forall x\oftype {\sigma}. \phi
\justifies
\Delta \vdash \phi[t/x]
\endprooftree & \mbox{if }t:\sigma\\
&&\\
\vspace{-.2cm}
(\mbox{conversion})
& 
\prooftree
\Delta \vdash \phi
\justifies
\Delta \vdash\psi
\endprooftree & \mbox{if }\phi =_{\beta} \psi\\[1em]
\end{array}$$

\end{document}