With these macros, one can typeset natural deduction proofs in Fitch style, as in the following example:
\begin{nd} \hypo {1} {\forall y \neg P(y)} \open \hypo {2} {\exists x P(x)} \open[u] \hypo {3} {P(u)} \have {4} {\forall y \neg P(y)} \r{1} \have {5} {\neg P(u)} \Ae{4} \have {6} {\bot} \ne{3,5} \close \have {6a}{\bot} \Ee{2,3-6} \close \have {7} {\neg \exists x P(x)} \ni{2-6a} \end{nd} |
This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.