I'm working through Computability and Logic and need to construct proofs the same way they do in the book. However, I can't find anything about how to give inference justifications that are on the same lines as premises in the sequent-style proof. What I can do is this :
2 Answers
Not exactly clear what you want. How about
\documentclass{article}
\usepackage{amsmath}
\usepackage{amssymb}
\begin{document}
\begin{align}
\{A\} & \implies \{A\} \tag{R0} \\
\{A,{\sim}A\} & \implies \varnothing \tag{R2a} \\
\Gamma & \implies \varnothing \tag{R1}.
\end{align}
\end{document}
Seeing bussproofs
in your question now, perhaps you want to use a proofs package, and I think the prooftrees
package does what you want except the nice alignment of the implications. But the package is suitable to write proofs.
\documentclass{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{prooftrees}
\forestset{line numbering=false}
\begin{document}
\begin{prooftree}
{
to prove={}
}
[
\{ A \} \Rightarrow \{ A \}, just=(R0)
[
{\{A, \neg A\} \Rightarrow \varnothing}, just=(R2a)
[
\Gamma \Rightarrow \varnothing, just=(R1)
]]]
\end{prooftree}
\end{document}