Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Natural deduction with handy latex commands
\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}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.