%---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|----8

%% natded package version 0.1
%% Copyright 2014 Mohammad M. Ajallooeian
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
% 
% The Current Maintainer of this work is Mohammad M. Ajallooeian, m.ajallooeian@gmail.com.
%
% This work consists of the files natded.sty, natded.tex and extended_doc.tex
% and complied files natded.pdf and extended_doc.pdf.

\documentclass{article}
\usepackage{natded}
\usepackage{fullpage}
\usepackage{listings}
\usepackage{paralist}
\usepackage[normalem]{ulem}
\usepackage{color}
\usepackage{graphicx}


\lstset
{
    language=[LaTeX]TeX,
    breaklines=true,
    basicstyle=\tt\scriptsize,
}

\usepackage{url}
\newcommand{\Jas}{Ja\'skowski }
\newcommand{\JasA}{Ja\'skowski}
\newcommand{\KM}{Kalish-Montague }
\newcommand{\KMa}{Kalish-Montague}


\title{A \LaTeX\, Package for Natural Deduction Proofs in the \\ Ja\'skowski and Kalish--Montague Styles}
\author{Mohammad M. Ajallooeian \and Francis Jeffry Pelletier}
\date{}

\begin{document}

\maketitle

\section{Description}

This package provides a \LaTeX\, environment to typeset natural deduction proofs in format used by Ja\'skowski (1934, footnote 3) or the format used by Kalish and Montague (1964) and Kalish, Montague, Mar (1980).  This format differs from both the tree format initiated by Gerhard Gentzen (1934) and available in \LaTeX\, with Sam Buss's bussproofs.sty and from the more common Frederic Fitch style also available in \LaTeX\, by either Johan Kl\"user's fitch.sty or Peter Selinger's fitch.sty (and more recently, from Richard Zach's lplfitch.sty).  A major point of difference between the various fitch-styles and the \Jas and \KM proofs is that these latter styles  draw entire boxes or rectangles around subproofs, and these boxes can be embedded inside one another.  Further details on both the logic and the history can be accessed from \cite{ext14}.

\section{Downloads}

Download the natded.sty and install in your \LaTeX\ path.

\section{Usage}

After instructing the \LaTeX\, compiler by using this package (by issuing a \verb+\usepackage{natded}+ at the beginning of the file, you can typeset natural deduction proofs in two major formats: Ja\'skowski-style proofs are specified by \verb+\Jproof{+\emph{proof contents}\verb+}+ command while Kalish--Montague-style proofs are specified by \verb+\KMproof{+\emph{proof contents}\verb+}+ command. Note that both of these commands \textbf{should be used in math mode}. There are two major components for a proof: 

\medskip

\begin{compactenum}
\item Simple proof lines are specified by a \verb+\proofline{+\emph{formula}\verb+}{+\emph{annotation}\verb+}+ command, 
\item Block commands, which initiate subproofs.  These blocks (which normally contain lines and/or other blocks as \emph{block contents}) come in two flavours: 
\begin{compactenum}[(i)]
\item A Kalish-Montague block, where  the conclusion comes before the block body: \\ \verb+\cbblk[+\emph{guard symbol}\verb+]{+\emph{conclusion}\verb+}{+\emph{block contents}\verb+}+, 
\item A \Jas block, where the conclusion comes after the block body: \\ \verb+\cablk[+\emph{guard symbol}\verb+]{+\emph{block contents}\verb+}{+\emph{conclusion}\verb+}+. 
\item (In both of these commands, the block guard is optional as indicated by the brackets around the argument.  The various roler of the guards are described in \cite{ext14}.
\end{compactenum}
\end{compactenum}

\section{Comments on Usage}
There are two distinct proof types -- the \JasA-proof, started by the \verb+\Jproof+ command, and the \KMa-proof, started by the \verb+\KMproof+ command.  These overall proof commands require the remaining \emph{proof contents} to be inside a set of braces.  Each of these two proof-types require a single line as a conclusion, and can have many lines and many subproofs as \emph{block contents}, and subproofs inside of them, and so forth.

The \JasA-proofs have the conclusion come after the end of its justifying subproof block, whereas the \KMa-proofs have the conclusion before the start of its justifying subproof.  Thus there are two separate commands that are in use: \verb+\cablk+ and \verb+\cbblk+, standing for \uline{c}onclusion \uline{a}fter and \uline{c}onclusion \uline{b}efore, respectively.  Obviously the \verb+\cablk+ is for use with the \verb+\Jproof+ while the \verb+\cablk+ is for use with the \verb+\KMproof+.

The two arguments to each of the proof-styles are the conclusion and the block contents, each surrounded by a set of braces.  Since the conclusions are always single formulas (possibly with a null annotation string), they are generated by indicating a formula: \verb+\proofline{+\emph{formula}\verb+}{+\emph{annotation}\verb+}+, which is also the way to put a single formula on a line anywhere within a subproof.  Note that \verb+\proofline+ requires each of its two arguments to be inside braces, but the line itself will not be within braces unless this is called for by some other feature (such as being the conclusion of one of block commands).

Note also that while the \emph{formula} of a \verb+\proofline+ is automatically in math mode, the \emph{annotation} is not.  So, if reference to a logical symbol is required for the annotation, it must explicitly employ \$s.

\section{Some Examples}
For example, Figure~\ref{fig:KM} is generated by Listing~\ref{lst:KM}, while Figure~\ref{fig:J} is generated by Listing~\ref{lst:J}.  Further examples, including their input listings, are in \cite{ext14}.

\begin{lstlisting}[caption={\LaTeX\, code for Kalish--Montague-style proof},label={lst:KM},numbers=left,escapeinside={@}{@}]
\[
\KMproof{
  \cbblk{  
  	\proofline{(((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))\rightarrow(P\rightarrow R))}{2--13 Conditionalization}
  }{
    \proofline{((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))}{Supposition}   
    \cbblk{
      \proofline{(P\rightarrow R)}{4--13 Conditionalization}
    }{
      \proofline{P}{Supposition}
      \proofline{((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))}{2 Repeat}
      \proofline{(P\rightarrow Q)}{5 Simplification}
      \proofline{Q}{4, 6 Modus Ponens}
      \proofline{(\neg R\rightarrow\neg Q)}{5 Simplification}
      \cbblk{
        \proofline{R}{10--13 Reductio ad Absurdum}
      }{   
        \proofline{\neg R}{Supposition}    
        \proofline{(\neg R\rightarrow\neg Q)}{8 Repeat}
        \proofline{\neg Q}{10, 11 Modus Ponens}
        \proofline{Q}{7 Repeat}
      }
    }
  }
}
\]
\end{lstlisting}


\begin{figure}
\caption{A Kalish--Montague-style proof\label{fig:KM}}
\[
\KMproof{
  \cbblk{  
  	\proofline{(((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))\rightarrow(P\rightarrow R))}{2--13 Conditionalization}
  }{
    \proofline{((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))}{Supposition}   
    \cbblk{
      \proofline{(P\rightarrow R)}{4--13 Conditionalization}
    }{
      \proofline{P}{Supposition}
      \proofline{((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))}{2 Repeat}
      \proofline{(P\rightarrow Q)}{5 Simplification}
      \proofline{Q}{4, 6 Modus Ponens}
      \proofline{(\neg R\rightarrow\neg Q)}{5 Simplification}
      \cbblk{
        \proofline{R}{10--13 Reductio ad Absurdum}
      }{   
        \proofline{\neg R}{Supposition}    
        \proofline{(\neg R\rightarrow\neg Q)}{8 Repeat}
        \proofline{\neg Q}{10, 11 Modus Ponens}
        \proofline{Q}{7 Repeat}
      }
    }
  }
}
\]
\end{figure}

\begin{figure}
\caption{A Ja\'skowski-style proof\label{fig:J}}
\[
\Jproof{
  \cablk{
    \proofline{((P\rightarrow Q)\land (\neg R \rightarrow\neg Q))}{Supposition}
    \cablk{
      \proofline{P}{Supposition}
      \proofline{((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))}{1 Repeat}
      \proofline{(P\rightarrow Q)}{3 Simplification}
      \proofline{Q}{2, 4 Modus Ponens}
      \proofline{(\neg R\rightarrow\neg Q)}{3 Simplification}
      \cablk{
        \proofline{\neg R}{Supposition}
        \proofline{(\neg R\rightarrow\neg Q)}{6 Repeat}
        \proofline{\neg Q}{7, 8 Modus Ponens}
        \proofline{Q}{5 Repeat}
      }{
        \proofline{R}{7--10 Reductio ad Absurdum}  
      }
    }{
      \proofline{(P\rightarrow R)}{2-11 Conditionalization}
    }
  }{
    \proofline{(((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))\rightarrow(P\rightarrow R))}{1--12 Conditionalization}
  }
}
\]
\end{figure}

\begin{lstlisting}[caption={\LaTeX\, code for Ja\'skowski-style proof},label={lst:J},numbers=left,escapeinside={@}{@}]
\[
\Jproof{
  \cablk{
    \proofline{((P\rightarrow Q)\land (\neg R \rightarrow\neg Q))}{Supposition}
    \cablk{
      \proofline{P}{Supposition}
      \proofline{((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))}{1 Repeat}
      \proofline{(P\rightarrow Q)}{3 Simplification}
      \proofline{Q}{2, 4 Modus Ponens}
      \proofline{(\neg R\rightarrow\neg Q)}{3 Simplification}
      \cablk{
        \proofline{\neg R}{Supposition}
        \proofline{(\neg R\rightarrow\neg Q)}{6 Repeat}
        \proofline{\neg Q}{7, 8 Modus Ponens}
        \proofline{Q}{5 Repeat}
      }{
        \proofline{R}{7--10 Reductio ad Absurdum}  
      }
    }{
      \proofline{(P\rightarrow R)}{2-11 Conditionalization}
    }
  }{
    \proofline{(((P\rightarrow Q)\land (\neg R\rightarrow\neg Q))\rightarrow(P\rightarrow R))}{1--12 Conditionalization}
  }
}
\]
\end{lstlisting}

\begin{thebibliography}{9}

\bibitem{ext14}
  Mohammad M. Ajallooeian and Francis Jeffry Pelletier.
  \emph{Kalish/Montague and Ja\'skowski Natural Deduction}.
  \LaTeX\ Package Manual on CTAN.
  2014.

\end{thebibliography}

\end{document}