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