summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/natded
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/natded
Initial commit
Diffstat (limited to 'macros/latex/contrib/natded')
l---------macros/latex/contrib/natded/README1
-rw-r--r--macros/latex/contrib/natded/README.md6
-rw-r--r--macros/latex/contrib/natded/extended_doc.pdfbin0 -> 189072 bytes
-rw-r--r--macros/latex/contrib/natded/extended_doc.tex399
-rw-r--r--macros/latex/contrib/natded/natded.pdfbin0 -> 143885 bytes
-rw-r--r--macros/latex/contrib/natded/natded.sty540
-rw-r--r--macros/latex/contrib/natded/natded.tex218
7 files changed, 1164 insertions, 0 deletions
diff --git a/macros/latex/contrib/natded/README b/macros/latex/contrib/natded/README
new file mode 120000
index 0000000000..42061c01a1
--- /dev/null
+++ b/macros/latex/contrib/natded/README
@@ -0,0 +1 @@
+README.md \ No newline at end of file
diff --git a/macros/latex/contrib/natded/README.md b/macros/latex/contrib/natded/README.md
new file mode 100644
index 0000000000..bf8801aa1d
--- /dev/null
+++ b/macros/latex/contrib/natded/README.md
@@ -0,0 +1,6 @@
+natded
+======
+
+A LaTeX package for natural deduction proofs in styles used by Jaśkowski and Kalish and Montague.
+
+Package version: 0.1 \ No newline at end of file
diff --git a/macros/latex/contrib/natded/extended_doc.pdf b/macros/latex/contrib/natded/extended_doc.pdf
new file mode 100644
index 0000000000..1c56b520a0
--- /dev/null
+++ b/macros/latex/contrib/natded/extended_doc.pdf
Binary files differ
diff --git a/macros/latex/contrib/natded/extended_doc.tex b/macros/latex/contrib/natded/extended_doc.tex
new file mode 100644
index 0000000000..ef3dd29af4
--- /dev/null
+++ b/macros/latex/contrib/natded/extended_doc.tex
@@ -0,0 +1,399 @@
+
+%% 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[11pt]{article}
+
+\usepackage{latexsym, amssymb,amsmath,amsthm,wasysym}
+\usepackage{bm} % Define \bm{} to use bold math fonts
+\usepackage[normalem]{ulem}
+\usepackage{listings}
+\usepackage{paralist}
+
+\usepackage{bussproofs} %Sam Buss's package for making Gentzen-like proof trees
+\usepackage{fitch} % johan KlŸwer's sty file for making Fitch proofs
+\usepackage{natded} %Mohammad Ajallooeian's sty file for making \Jas and \KM proofs.
+
+\newcommand{\Jas}{Ja\'skowski }
+\newcommand{\JasA}{Ja\'skowski}
+\newcommand{\Jass}{Ja\'skowski's }
+\newcommand{\JassA}{Ja\'skowski's}
+\newcommand{\Gen}{Gentzen }
+\newcommand{\GenA}{Gentzen}
+\newcommand{\GensA}{Gentzen's}
+\newcommand{\Gens}{Gentzen's }
+\newcommand{\ND}{natural deduction }
+\newcommand{\NDA}{natural deduction}
+\newcommand{\KM}{Kalish-Montague }
+\newcommand{\KMA}{Kalish-Montague}
+
+\newcommand{\bx}{\square}
+\newcommand{\dia}{\diamondsuit}
+
+\title{Kalish/Montague and Ja{\'s}kowski Natural Deduction}
+\author{Mohammad M. Ajallooeian\\ University of Alberta \and Francis Jeffry Pelletier \\
+University of Alberta}
+
+\date{}
+
+\begin{document}
+\maketitle
+
+
+\noindent The Latex style file natded.sty will produce representations of natural deduction proofs in either \Jass original style or the modification of that style by \KMA. But before describing some of the details of the use of the natded.sty (including the use of ``guards''), we pause for some relevant historical information.
+
+The history of the formal approach to natural deduction dates from 1934, when two papers appeared simultaneously in different journals written by authors who had no interaction of any type with one another. Stanis{\l}aw Ja{\'s}kowski (``On the Rules of Suppositions in Formal Logic'', \emph{Studia Logica}, v. 1) and Gerhard Gentzen (``Untersuchungen \"uber das logische Schlie\ss en'' [``Investigations into Logical Deduction''], \emph{Mathematische Zeitschrift} v. 39) worked on the same problem -- of trying to formally mimic the reasoning of ``ordinary mathematicians'' who would ``make assumptions and see where they lead'' and only later conclude with something that was not dependent on those assumptions.
+
+Although they had essentially the same motivation, and arrived at similar but not quite identical conclusions, their methods of representing this sort of reasoning were quite different. Gentzen used a tree format, which can be mimicked using Sam Buss's bussproofs.sty. For example, the proof of the propositional logic theorem $\vdash(((p\rightarrow q)\land(\neg r\rightarrow\neg q))\rightarrow(p\rightarrow r))$ takes this form:
+
+
+\begin{prooftree}
+ \AxiomC{\sout{ 3 } }
+ \noLine
+ \UnaryInfC{$\neg r$}
+ \AxiomC{\sout{ 1 } }
+ \noLine
+ \UnaryInfC{$((p\rightarrow q) \wedge (\neg r\rightarrow \neg q))$}
+ \LeftLabel{} \RightLabel{\scriptsize $\wedge$-E}
+ \UnaryInfC{$(\neg r\rightarrow \neg q)$}
+ \LeftLabel{} \RightLabel{\scriptsize $\rightarrow$-E}
+ \BinaryInfC{$\neg q$}
+ \AxiomC{\sout{ 1 } }
+ \noLine
+ \UnaryInfC{$((p\rightarrow q) \wedge (\neg r\rightarrow \neg q))$}
+ \LeftLabel{} \RightLabel{\scriptsize $\wedge$-E}
+ \UnaryInfC{$(p\rightarrow q)$}
+ \AxiomC{\sout{ 2 } }
+ \noLine
+ \UnaryInfC{$p$}
+ \LeftLabel{} \RightLabel{\scriptsize $\rightarrow$-E}
+ \BinaryInfC{$ q$}
+ \LeftLabel{} \RightLabel{\scriptsize $\bot$-I}
+ \BinaryInfC{$\bot$}
+ \LeftLabel{} \RightLabel{\scriptsize $\bot$-E (3)}
+ \UnaryInfC{$r$}
+ \LeftLabel{} \RightLabel{\scriptsize $\rightarrow$-I (2)}
+ \UnaryInfC{$(p\rightarrow r)$}
+ \LeftLabel{} \RightLabel{\scriptsize $\rightarrow$-I (1)}
+ \UnaryInfC{$(((p\rightarrow q) \wedge (\neg r\rightarrow \neg q))\rightarrow(p\rightarrow r))$}
+
+\end{prooftree}
+
+\medskip
+
+A perhaps more familiar style of natural deduction proofs, especially among those who learned their elementary logic in philosophy departments, are the ones usually called ``Fitch'' representations. For this type of proof representation, there are two Latex packages in common use: Johan Kl\"uwer's fitch.sty and Peter Selinger's fitch.sty. Minor variants of these style packages are available, such as Richard Zach's lplfitch.sty. Here's that same proof using Kl\"uwer's fitch.sty:
+
+\begin{equation*}
+ \begin{fitch}
+ \fa \fh ((p\rightarrow q) \wedge(\neg r\rightarrow\neg q)) \\
+ \fa \fa \fh p \\
+ \fa \fa \fa ((p\rightarrow q) \wedge(\neg r\rightarrow\neg q)) & 1, Reiteration \\
+ \fa \fa \fa (p\rightarrow q) & 3,$\wedge$E \\
+ \fa \fa \fa q & 2,4 $\rightarrow$E \\
+ \fa \fa \fa (\neg r\rightarrow\neg q) & 3,$\wedge$E \\
+ \fa \fa \fa \fh \neg r \\
+ \fa \fa \fa \fa (\neg r\rightarrow\neg q) & 6,Reiteration \\
+ \fa \fa \fa \fa \neg q & 7,8 $\rightarrow$E \\
+ \fa \fa \fa \fa q & 5,Reiteration \\
+ \fa \fa \fa r & 7--10, $\neg$E \\
+ \fa \fa (p\rightarrow r) & 2--11, $\rightarrow$I \\
+ \fa (((p\rightarrow q) \wedge(\neg r\rightarrow\neg q))) & 1--12,$\rightarrow$I
+ \end{fitch}
+\end{equation*}
+
+\noindent This method is derived from one (of two) methods for natural deduction proof representation described by \Jas (1934). However, this fitch method (from Fredric Fitch (1952) \emph{Symbolic Logic}) is not exactly the way \Jas did his proofs. Here's that same proof in this one of his methods:
+
+\[
+\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\supset r}{2-11 Conditionalization}
+ }
+ }{
+ \proofline {(((p\rightarrow q)\land(\neg r\rightarrow\neg q)) \rightarrow(p \rightarrow r))}{1--12 Conditionalization}
+ }
+}
+\]
+
+
+\noindent It can be seen that what Fitch did was to remove all but the left-side of the boxes (rectangles) that \Jas employed to indicate the new ``world of the supposition''. And Fitch underlined the assumption or hypothesis or supposition of each such world, which is the first line inside one of \Jass boxes. Although the difficulty of typesetting these boxes caused Fitch's method to became more common, at least one textbook employed a variant on this method of \JassA, namely D. Kalish \& R. Montague's (1964) \emph{Logic} and the expanded D. Kalish, R. Montague \& G. Mar (1980) \emph{Logic}. One noticeable difference is that the \KM method placed the conclusion of each one of the boxes at the \emph{beginning} of the subproof, just before the assumption. This was indicated by the word {\sc show}, so that when engaged in a (sub)proof, one starts by writing the desired conclusion of that (sub)proof, prefixed by this {\sc show}. And when one legitimately completes that subproof, one ``cancels'' the {\sc show} by drawing a line through it, which indicates that the conclusion can become a part of the next-outer (sub)proof. Here is that same theorem proved in the \KM system.
+
+The codes for producing the \Jas and \KM proofs are in Listings~\ref{basicJproof} and \ref{basicKMproof}, respectively.
+
+\scriptsize
+\[
+\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}
+ }
+ }
+ }
+}
+\]
+
+
+\begin{lstlisting}[caption={\LaTeX\, code for Ja\'skowski-style proof},label={basicJproof},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\supset r}{2-11 Conditionalization}
+ }
+ }{
+ \proofline {(((p\rightarrow q)\land(\neg r\rightarrow\neg q)) \rightarrow(p \rightarrow r))}{1--12 Conditionalization}
+ }
+}
+\]
+\end{lstlisting}
+
+\begin{lstlisting}[caption={\LaTeX\, code for Kalish-Montague-style proof},label={basicKMproof},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}
+
+\normalsize
+\medskip
+
+\noindent Within the code to produce the \Jas and the Kalish-Montague proofs we see two differences: First, the \Jas proofs use the main control \verb+\Jproof+, while the Kalish-Montague proofs employ \verb+\KMproof+. Secondly, within each of these different proof controls are the commands for typesetting the conclusion: in the \verb+\Jproof+, conclusions go \emph{after} the supporting subproof, so we use \verb+\cablk+ for \uline{c}onclusion \uline{a}fter block; in the \verb+\KMproof+ the conclusions come before the subproof so we use \verb+\cbblk+ for \uline{c}onclusion \uline{b}efore block. And we have written the block structure before the conclusion in the \Jas proof, while it is written after the conclusion in the Kalish-Montague proof.
+
+\medskip
+
+On Kl\"uwer's and Selinger's pages describing their two fitch.sty files, the following argument is displayed:
+
+\begin{equation*}
+ \begin{fitch}
+ \fh \exists x\forall y P(x,y) \\
+ \fa \fitchmodal{v} \fitchmodalh{u} \forall y P(u,y) \\
+ \fa \fa \fa P(u,v) & $\forall${\bf E}, 2 \\
+ \fa \fa \fa \exists x P(x,v) & $\exists${\bf i}, 3 \\
+ \fa \fa \exists x P(x,v) & $\exists${\bf E}, 1, 2--4 \\
+ \fa \forall y\exists x P(x,y) & $\forall${\bf I}, 2--5 \\
+ \end{fitch}
+\end{equation*}
+
+\noindent The idea is that $u$ and $v$ are \emph{guards}, whose role is to prevent certain variables being imported into or exported out of the relevant subproof that they are guarding. A \Jas style proof of this theorem is given in Figure~\ref{fig:JasVarGuard} and is generated by Listing~\ref{lst:JasVarGuard}.
+
+\scriptsize
+
+\begin{figure}[h!]
+\caption{A Ja\'skowski-style proof with guarded variables\label{fig:JasVarGuard}}
+\scriptsize
+\[
+\Jproof
+ {\proofline{\exists x\forall yP(x,y)}{Premise}
+ \cablk[v]{
+ \cablk[u]{
+ \proofline{\forall yP(u,y)}{Supposition}
+ \proofline{P(u,v)}{2, $\forall\bm{E}$}
+ \proofline{\exists xP(x,v)}{3, $\exists\bm{I}$}
+ }
+ {\proofline{\exists xP(x,v)}{1,2--4, $\exists\bm{E}$} }
+ }
+ {\proofline{\forall y\exists xP(x,y)}{2--5, $\forall\bm{I}$}
+ }
+ }
+\]
+\end{figure}
+
+\begin{lstlisting}[caption={\LaTeX\, code for \JasA-style proof with guarded variables},label={lst:JasVarGuard},numbers=left,escapeinside={@}{@}]
+\[
+\Jproof
+ {\proofline{\exists x\forall yP(x,y)}{Premise}
+ \cablk[v]{
+ \cablk[u]{
+ \proofline{\forall yP(u,y)}{Supposition}
+ \proofline{P(u,v)}{2, $\forall\bm{E}$}
+ \proofline{\exists xP(x,v)}{3, $\exists\bm{I}$}
+ }
+ {\proofline{\exists xP(x,v)}{1,2--4, $\exists\bm{E}$} }
+ }
+ {\proofline{\forall y\exists xP(x,y)}{2--5, $\forall\bm{I}$}
+ }
+ }
+\]
+\end{lstlisting}
+
+\normalsize
+
+\medskip
+Kalish-Montague's strategy of putting {\sc show} lines at the beginning of a subproof and of counting the (free) variables in that formula as if they actually occurred in the proof at the time one wishes to reiterate into the area beneath such an uncancelled {\sc show} (or to do $\exists\bm{E}$ by instantiating to variables that occur in the {\sc show} formula), makes it unnecessary to have explicit guards to protect $\forall\bm{I}$ and $\exists\bm{E}$, since these are the only reasons to have guards for variables -- although one could indicate them using the present \verb+\KMproof+, if one wished. (Another peculiarity of the Kalish-Montague system is that their $\exists$-elimination rule does not employ a subproof, but directly introduces a (completely) new variable into the proof, including being completely distinct from variables in {\sc show} lines -- even uncancelled ones.) For these reasons we do not display the use of guards for variables in the Kalish-Montague system. But such guards are more logically useful in a \JasA-style proof.
+
+
+ Another use of guards is in modal logic, where -- depending on the particular modal system that we are providing a proof system for -- certain formulas cannot be reiterated into a guarded-with-a-$\bx$ scope line. Here is an example in modal system S$_4$ (or any stronger one). A \Jas style proof of the valid argument $\bx p\land\bx q\vdash\bx(p\land q)$ is given in Figure~\ref{fig:JmodalGuard} and is generated by Listing~\ref{lst:JmodalGuard}. It is followed by a \KM style proof of the same argument in Figure~\ref{fig:KMmodalGuard} together with its code in Listing~\ref{lst:KMmodalGuard}.
+
+\scriptsize
+
+\begin{figure}[h!]
+\caption{A \JasA-style proof with modal guards\label{fig:JmodalGuard}}
+\scriptsize
+\[
+\Jproof{
+ \proofline{\bx p\land\bx q}{premise}
+ \proofline{\bx p}{1,$\land\bm{E}$}
+ \proofline{\bx q}{1,$\land\bm{E}$}
+ \cablk[\bx]
+ {\proofline{\bx p}{2, Reiterate}
+ \proofline{\bx q}{3, Reiterate}
+ \proofline{p}{4, $\bx\bm{E}$}
+ \proofline{q}{5, $\bx\bm{E}$}
+ \proofline{p\land q}{6,7, $\land\bm{I}$}
+ }
+ {\proofline{\bx(p\land q)}{4--8, $\bx\bm{I}$} }
+ }
+\]
+\end{figure}
+
+\begin{lstlisting}[caption={\LaTeX\, code for \JasA-style proof with modal guards},label={lst:JmodalGuard},numbers=left,escapeinside={@}{@}]
+\[
+\Jproof{
+ \proofline{\bx p\land\bx q}{premise}
+ \proofline{\bx p}{1,$\land\bm{E}$}
+ \proofline{\bx q}{1,$\land\bm{E}$}
+ \cablk[\bx]
+ {\proofline{\bx p}{2, Reiterate}
+ \proofline{\bx q}{3, Reiterate}
+ \proofline{p}{4, $\bx\bm{E}$}
+ \proofline{q}{5, $\bx\bm{E}$}
+ \proofline{p\land q}{6,7, $\land\bm{I}$}
+ }
+ {\proofline{\bx(p\land q)}{4--8, $\bx\bm{I}$} }
+ }
+\]
+\end{lstlisting}
+
+\begin{figure}[h!]
+\caption{A Kalish/Montague-style proof with modal guards\label{fig:KMmodalGuard}}
+\[
+\KMproof{
+ \cbblk
+ {\proofline{\bx (p \land q)}{5, Direct Proof} }
+ {\proofline{\bx p \land \bx q}{Premise}
+ \proofline{\bx p}{2, $\land\bm{E}$ }
+ \proofline{\bx q}{2, $\land\bm{E}$ }
+ \cbblk[\bx]
+ { \proofline{\bx (p \land q)}{6--10, $\bx\bm{I}$} }
+ { \proofline{\bx p}{3, Reiterate}
+ \proofline{\bx q}{4, Reiterate}
+ \proofline{p}{6, $\bx\bm{E}$}
+ \proofline{q}{7, $\bx\bm{E}$}
+ \proofline{(p\land q)}{8,9 $\land\bm{I}$} }
+ }
+ }
+\]
+\end{figure}
+
+\begin{lstlisting}[caption={\LaTeX\, code for \KMA-style proof with modal guards},label={lst:KMmodalGuard},numbers=left,escapeinside={@}{@}]
+\[
+\KMproof{
+ \cbblk
+ {\proofline{\bx (p \land q)}{5, Direct Proof} }
+ {\proofline{\bx p \land \bx q}{Premise}
+ \proofline{\bx p}{2, $\land\bm{E}$ }
+ \proofline{\bx q}{2, $\land\bm{E}$ }
+ \cbblk[\bx]
+ { \proofline{\bx (p \land q)}{6--10, $\bx\bm{I}$} }
+ { \proofline{\bx p}{3, Reiterate}
+ \proofline{\bx q}{4, Reiterate}
+ \proofline{p}{6, $\bx\bm{E}$}
+ \proofline{q}{7, $\bx\bm{E}$}
+ \proofline{(p\land q)}{8,9 $\land\bm{I}$} }
+ }
+ }
+\]
+
+\end{lstlisting}
+
+
+\normalsize
+
+\bigskip
+
+For further details on the history of natural deduction, including how it became the standard method in elementary logic textbooks, especially in the years 1950-1990 and beyond, see F.J. Pelletier (1999) ``A Brief History of Natural Deduction'' \emph{History and Philosophy of Logic}, v. 20, pp. 1--31. Also discussed are the four main styles of representing natural deduction proofs: the Gentzen trees, the \JasA-Fitch graphical (boxes) method, the \JasA-Quine (1950) bookkeeping method, and the Suppes (1957) sequent natural deduction method. A discussion of how comparatively wide-spread these four methods have become is also indicated by a survey of many elementary natural deduction textbooks.
+
+\end{document}
diff --git a/macros/latex/contrib/natded/natded.pdf b/macros/latex/contrib/natded/natded.pdf
new file mode 100644
index 0000000000..2da27b30b2
--- /dev/null
+++ b/macros/latex/contrib/natded/natded.pdf
Binary files differ
diff --git a/macros/latex/contrib/natded/natded.sty b/macros/latex/contrib/natded/natded.sty
new file mode 100644
index 0000000000..abbd8314da
--- /dev/null
+++ b/macros/latex/contrib/natded/natded.sty
@@ -0,0 +1,540 @@
+%---|----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.
+
+\makeatletter
+
+%%%%% LEVEL A
+
+\usepackage{calc}
+
+% lengths
+
+\newlength{\negdepth@jaska} % negative depth
+\newlength{\posdepth@jaska} % positive depth
+\newlength{\lineheight@jaska} % line height
+\newlength{\hmargin@jaska} % horizontal margin
+\newlength{\vmargin@jaska} % vertical margin
+\newlength{\vextra@jaska} % line extra height
+\newlength{\cmargin@jaska} % comments margin
+\newlength{\borderwidth@jaska} % border width
+\newlength{\nowidth@jaska} % no border width
+\newlength{\hhrulebase@jaska} % half of horizontal rule base length
+\newlength{\stdepth@jaska} % depth of strikethrough mark
+\newlength{\stwidth@jaska} % width of strikethrough mark
+\newlength{\arrayrowheight@jaska} % array environment row height
+\newlength{\guardspace@jaska} % length of guards
+\newlength{\jguard@jaska} % length of guards - Jáskowski style
+\newlength{\kmguard@jaska} % length of guards - Kalish and Montague style
+
+\newlength{\templength@jaska} % temporary length variable
+
+% initialization
+
+%%% independent
+\setlength{\hmargin@jaska} { 10pt}
+\setlength{\vmargin@jaska} { 5pt}
+\setlength{\vextra@jaska} { 0pt}
+\setlength{\cmargin@jaska} { 20pt}
+\setlength{\borderwidth@jaska} { 1pt}
+\setlength{\nowidth@jaska} { 0pt}
+
+
+%%% dependent
+\setlength{\hhrulebase@jaska}{\hmargin@jaska} %
+\addtolength{\hhrulebase@jaska}{\borderwidth@jaska}
+
+%%% boxes
+
+\newsavebox\tempbox@jaska
+
+% utilities
+
+\newcommand\hcancel@jaska[2][0.5pt]{
+ \ifmmode
+ \sbox\tempbox@jaska{$#2$}
+ \else
+ \sbox\tempbox@jaska{#2}
+ \fi
+ \makebox[0pt][l]{\usebox\tempbox@jaska}
+ \rule[0.5\ht\tempbox@jaska-#1/2]{\wd\tempbox@jaska}{#1}
+}
+
+\newcommand{\showmark@jaska}{
+ \hcancel@jaska{Show}\;
+}
+
+% context dependent initializations
+
+\sbox\tempbox@jaska{$\showmark@jaska$}
+\setlength{\kmguard@jaska}{\wd\tempbox@jaska}
+\setlength{\jguard@jaska}{\vmargin@jaska}
+
+\setlength{\guardspace@jaska}{\jguard@jaska}
+
+%low-level commands
+
+\newcommand{\frml@jaska}[1]{
+ \sbox\tempbox@jaska{$#1$, \the\ht\tempbox@jaska, \the\dp\tempbox@jaska}
+
+ \setlength{\lineheight@jaska}{\ht\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{2\vmargin@jaska}
+ \addtolength{\lineheight@jaska}{\vextra@jaska}
+
+ \begin{minipage}[c][\lineheight@jaska][c]{\wd\tempbox@jaska}
+ $#1$
+ \end{minipage}
+}
+
+\newcommand{\boxtop@jaska}[3][\,]{
+ \makebox[\guardspace@jaska][r]{$#1$}
+
+ \sbox\tempbox@jaska{$#2$}
+
+ \setlength{\templength@jaska}{#3}
+ \addtolength{\templength@jaska}{2\hhrulebase@jaska}
+
+ \setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
+
+ \setlength{\lineheight@jaska}{\ht\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\vextra@jaska}
+ \addtolength{\lineheight@jaska}{-0.25\vmargin@jaska}
+
+
+ \setlength{\posdepth@jaska}{\lineheight@jaska}
+ \addtolength{\posdepth@jaska}{\negdepth@jaska}
+
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \hspace{-\borderwidth@jaska}
+ \rule[\posdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
+ \hspace{-\borderwidth@jaska}
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \setlength{\templength@jaska}{-#3}
+ \addtolength{\templength@jaska}{-\hhrulebase@jaska}
+ \hspace{\templength@jaska}
+ \addtolength{\lineheight@jaska}{0.25\vmargin@jaska}
+ \raisebox{0pt}[\lineheight@jaska][0pt]{$#2$}
+ \hspace{\cmargin@jaska}
+}
+
+\newcommand{\boxmid@jaska}[3][\,]{
+ \makebox[\guardspace@jaska][r]{$#1$}
+
+ \sbox\tempbox@jaska{$#2$}
+
+ \setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
+
+ \setlength{\lineheight@jaska}{\ht\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\vextra@jaska}
+
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \hspace{\hmargin@jaska}
+ \hspace{#3}
+ \hspace{\hmargin@jaska}
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \setlength{\templength@jaska}{-#3}
+ \addtolength{\templength@jaska}{-\hhrulebase@jaska}
+ \hspace{\templength@jaska}
+ \makebox[#3][l]{$#2$}
+ \hspace{\cmargin@jaska}
+}
+
+\newcommand{\boxbot@jaska}[3][\,]{
+ \makebox[\guardspace@jaska][r]{$#1$}
+
+ \sbox\tempbox@jaska{$#2$}
+
+ \setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
+ \addtolength{\negdepth@jaska}{0.25\vmargin@jaska}
+
+ \setlength{\lineheight@jaska}{\ht\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\vextra@jaska}
+ \addtolength{\lineheight@jaska}{-0.25\vmargin@jaska}
+
+ \setlength{\templength@jaska}{#3}
+ \addtolength{\templength@jaska}{2\hhrulebase@jaska}
+
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \hspace{-\borderwidth@jaska}
+ \rule[\negdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
+ \hspace{-\borderwidth@jaska}
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \setlength{\templength@jaska}{-#3}
+ \addtolength{\templength@jaska}{-\hhrulebase@jaska}
+ \hspace{\templength@jaska}
+ \addtolength{\lineheight@jaska}{0.0\vmargin@jaska}
+ \raisebox{0pt}[0pt][\lineheight@jaska]{$#2$}
+ \hspace{\cmargin@jaska}
+}
+
+\newcommand{\boxdbl@jaska}[3][\,]{
+ \makebox[\guardspace@jaska][r]{$#1$}
+
+ \sbox\tempbox@jaska{$#2$}
+
+ \setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
+ \addtolength{\negdepth@jaska}{0.25\vmargin@jaska}
+
+ \setlength{\lineheight@jaska}{\ht\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\vextra@jaska}
+ \addtolength{\lineheight@jaska}{-0.5\vmargin@jaska}
+
+ \setlength{\posdepth@jaska}{\lineheight@jaska}
+ \addtolength{\posdepth@jaska}{\negdepth@jaska}
+
+ \setlength{\templength@jaska}{#3}
+ \addtolength{\templength@jaska}{2\hhrulebase@jaska}
+
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \hspace{-\borderwidth@jaska}
+ \rule[\negdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
+ \hspace{-\templength@jaska}
+ \rule[\posdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
+ \hspace{-\borderwidth@jaska}
+ \rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
+ \setlength{\templength@jaska}{-#3}
+ \addtolength{\templength@jaska}{-\hhrulebase@jaska}
+ \hspace{\templength@jaska}
+ \addtolength{\lineheight@jaska}{0.0\vmargin@jaska}
+ \raisebox{0pt}[0pt][\lineheight@jaska]{$#2$}
+ \hspace{\cmargin@jaska}
+}
+
+
+\newcommand{\boxnot@jaska}[3][\,]{
+ \hspace{-\guardspace@jaska}
+ \hspace{-\hmargin@jaska}
+ \hspace{-\borderwidth@jaska}
+ \makebox[\guardspace@jaska][r]{$#1$}
+
+ \sbox\tempbox@jaska{$#2$}
+
+ \setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
+
+ \setlength{\lineheight@jaska}{\ht\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
+ \addtolength{\lineheight@jaska}{\vextra@jaska}
+
+ \setlength{\posdepth@jaska}{\lineheight@jaska}
+ \addtolength{\posdepth@jaska}{\negdepth@jaska}
+
+ \rule[\negdepth@jaska]{0pt}{\lineheight@jaska}
+ \hspace{\borderwidth@jaska}
+ \hspace{\hmargin@jaska}
+ \hspace{#3}
+ \hspace{\hmargin@jaska}
+ \rule[\negdepth@jaska]{0pt}{\lineheight@jaska}
+ \hspace{\borderwidth@jaska}
+ \setlength{\templength@jaska}{-#3}
+ \addtolength{\templength@jaska}{-\hhrulebase@jaska}
+ \hspace{\templength@jaska}
+ \makebox[#3][l]{$#2$}
+ \hspace{\cmargin@jaska}
+}
+
+\newcommand{\setstylej@jaska}{
+ \setlength{\guardspace@jaska}{\jguard@jaska}
+}
+
+\newcommand{\setstylekm@jaska}{
+ \setlength{\guardspace@jaska}{\kmguard@jaska}
+}
+
+%%%%% LEVEL B
+
+\newcounter{depth@jaskb}
+\newcounter{jdepth@jaskb}
+\newcounter{linecount@jaskb}
+
+\newlength{\templength@jaskb}
+\newlength{\extrawin@jaskb}
+\newlength{\extrawout@jaskb}
+
+\setlength{\extrawin@jaskb}{2pt}
+\setlength{\extrawout@jaskb}{\dimexpr\guardspace@jaska+\hmargin@jaska+25pt+\hmargin@jaska\relax}
+
+\newsavebox\tempbox@jaskb
+
+\def\makcl@jaskb#1#2{%
+ \ifcsname #1#2@jaskb\endcsname%
+ \else%
+ \ifnum#2>0\relax%
+ \makcl@jaskb{#1}{\number\numexpr#2-1\relax}%
+ \fi%
+ \global\expandafter\newcount\csname #1#2@jaskb\endcsname%
+ \fi%
+}
+
+\def\setcl@jaskb#1#2#3{%
+ \global\expandafter\csname #1#2@jaskb\endcsname #3\relax%
+}
+
+\def\inccl@jaskb#1#2{%
+ \global\expandafter\advance\csname #1#2@jaskb\endcsname by 1\relax%
+}%
+
+\def\stpcl@jaskb#1#2{%
+ \ifnum#2>0\relax%
+ \stpcl@jaskb{#1}{\number\numexpr#2-1\relax}%
+ \fi%
+ \inccl@jaskb{#1}{#2}%
+}%
+
+\def\getcl@jaskb#1#2{%
+ \the\expandafter\csname #1#2@jaskb\endcsname%
+}%
+
+\def\makdl@jaskb#1#2{%
+ \ifcsname #1#2@jaskb\endcsname%
+ \else%
+ \ifnum#2>0\relax%
+ \makdl@jaskb{#1}{\number\numexpr#2-1\relax}%
+ \fi%
+ \global\expandafter\newdimen\csname #1#2@jaskb\endcsname%
+ \fi%
+}
+
+\def\setdl@jaskb#1#2#3{%
+ \global\expandafter\csname #1#2@jaskb\endcsname=\dimexpr#3\relax%
+}
+
+\def\adddl@jaskb#1#2#3{%
+ \global\expandafter\advance\csname #1#2@jaskb\endcsname \dimexpr#3\relax%
+}%
+
+\def\getdl@jaskb#1#2{%
+ \the\expandafter\csname #1#2@jaskb\endcsname%
+}%
+
+\def\upddl@jaskb#1#2#3{%
+ \ifdim#3>\expandafter\csname #1#2@jaskb\endcsname\relax%
+ \setdl@jaskb{#1}{#2}{#3}%
+ \fi%
+}%
+
+\def\ruddl@jaskb#1#2#3#4{%
+ \upddl@jaskb{#1}{#2}{#3}%
+ \ifnum#2>0\relax%
+ \ruddl@jaskb{#1}{\number\numexpr#2-1\relax}{\dimexpr#3+#4\relax}{#4}%
+ \fi%
+}%
+
+\def\pshlsymb@jaskb#1#2#3{%
+ \global\expandafter\def\csname #1#2@jaskb\endcsname{#3}%
+}%
+
+\def\poplsymb@jaskb#1#2{%
+ \csname #1#2@jaskb\endcsname%
+% \texttt{G}#2
+% \pshlsymb@jaskb{#1}{#2}{}%
+}%
+
+
+\def\measurewidth@jaskb#1{%
+ \inccl@jaskb{mlevel}{\thedepth@jaskb}
+ \sbox\tempbox@jaskb{$#1$}%
+ \makdl@jaskb{blockwidth}{\thedepth@jaskb}
+ \ruddl@jaskb{blockwidth}{\thedepth@jaskb}{\dimexpr\wd\tempbox@jaskb+\extrawin@jaskb\relax}{\extrawout@jaskb}
+}
+
+\def\jmeasurewidth@jaskb#1{%
+ \inccl@jaskb{mlevel}{\thedepth@jaskb}
+ \sbox\tempbox@jaskb{$#1$}%
+ \makdl@jaskb{blockwidth}{\thejdepth@jaskb}
+ \ruddl@jaskb{blockwidth}{\thejdepth@jaskb}{\dimexpr\wd\tempbox@jaskb+\extrawin@jaskb\relax}{\extrawout@jaskb}
+}
+
+\def\setle@jaskb#1#2#3{%
+ \global\expandafter\def\csname #1#2@jaskb\endcsname{#3}%
+}
+
+\def\getle@jaskb#1#2{%
+ \csname #1#2@jaskb\endcsname%
+}
+
+\def\genlevexpr@jaskb#1#2{%
+ \ifnum\getcl@jaskb{plevel}{#1}=1\relax%
+ \ifnum\getcl@jaskb{plevel}{#1}=\getcl@jaskb{mlevel}{#1}\relax%
+ \setle@jaskb{levexpr}{#1}{\boxdbl@jaska[#2\poplsymb@jaskb{guardsym}{#1}]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
+ \else%
+ \setle@jaskb{levexpr}{#1}{\boxtop@jaska[#2\poplsymb@jaskb{guardsym}{#1}]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
+ \fi%
+ \else%
+ \ifnum\getcl@jaskb{plevel}{#1}=\getcl@jaskb{mlevel}{#1}\relax%
+ \setle@jaskb{levexpr}{#1}{\boxbot@jaska[#2]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
+ \else%
+ \setle@jaskb{levexpr}{#1}{\boxmid@jaska[#2]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
+ \fi%
+ \fi%
+ \ifnum#1>1\relax%
+ \genlevexpr@jaskb{\number\numexpr#1-1\relax}{}%
+ \fi%
+}
+
+\def\statement@jaskb#1#2#3#4#5#6{%
+ \stpcl@jaskb{plevel}{\thedepth@jaskb}%
+ \ifnum#1>0\relax%
+ \setle@jaskb{levexpr}{\number\numexpr#1+1\relax}{\frml@jaska{#5}} \genlevexpr@jaskb{#1}{#4#2}%
+ \setle@jaskb{levexpr}{0}{\getle@jaskb{levexpr}{1}}%
+ \else%
+ \setle@jaskb{levexpr}{0}{\boxnot@jaska[#4#2]{\frml@jaska{#5}}{\getdl@jaskb{blockwidth}{#1}}}%
+ \fi%
+ %#3&...
+ \stepcounter{linecount@jaskb}%
+ \thelinecount@jaskb.&\getle@jaskb{levexpr}{0}&\mbox{#6}\\%
+}
+
+\def\cblockmeasure@jaskb#1{%
+ \stepcounter{jdepth@jaskb}%
+ \gdef\hypo@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}}%
+ \gdef\have@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}}%
+ \makdl@jaskb{blockwidth}{\thejdepth@jaskb}%
+ \setdl@jaskb{blockwidth}{\thejdepth@jaskb}{\extrawin@jaskb}%
+ #1%
+ \gdef\hypo@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
+ \gdef\have@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
+ \addtocounter{jdepth@jaskb}{-1}%
+}
+
+\def\cblockprint@jaskb#1#2{%
+ \stepcounter{depth@jaskb}%
+ \stepcounter{jdepth@jaskb}%
+ \pshlsymb@jaskb{guardsym}{\thedepth@jaskb}{#2}%
+ \makcl@jaskb{mlevel}{\thedepth@jaskb}%
+ \setcl@jaskb{mlevel}{\thedepth@jaskb}{0}%
+ \makcl@jaskb{plevel}{\thedepth@jaskb}%
+ \setcl@jaskb{plevel}{\thedepth@jaskb}{0}%
+ \makdl@jaskb{blockwidth}{\thedepth@jaskb}%
+ \setdl@jaskb{blockwidth}{\thedepth@jaskb}{\extrawin@jaskb}%
+ \gdef\hypo@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
+ \gdef\have@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
+ \gdef\cblock@jaskb##1##2{\cblockmeasure@jaskb{##1}}%
+ #1%
+ \gdef\hypo@jaskb##1##2##3##4{\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{\showmark@jaska##3}{##4}}%
+ \gdef\have@jaskb##1##2##3##4{\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{##3}{##4}}%
+ \gdef\cblock@jaskb##1##2{\cblockprint@jaskb{##1}{##2}}%
+ #1%
+ \addtocounter{depth@jaskb}{-1}%
+ \addtocounter{jdepth@jaskb}{-1}%
+}
+
+\def\hypo@jaskb#1#2#3#4{}
+\def\have@jaskb#1#2#3#4{}
+
+\def\cblock@jaskb#1#2{\cblockprint@jaskb{#1}{#2}}
+
+\def\outer@jaskb#1{%
+ \setcounter{depth@jaskb}{0}%
+ \setcounter{jdepth@jaskb}{0}%
+ \setcounter{linecount@jaskb}{0}
+ \makcl@jaskb{mlevel}{\thedepth@jaskb}
+ \setcl@jaskb{mlevel}{\thedepth@jaskb}{0}
+ \makcl@jaskb{plevel}{\thedepth@jaskb}
+ \setcl@jaskb{plevel}{\thedepth@jaskb}{0}
+ \begin{array}{lll}%
+ \gdef\hypo@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{\showmark@jaska##3}{##4}}%
+ \gdef\have@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{##3}{##4}}%
+ #1%
+ \end{array}%
+}
+
+%%%%% OUTPUT LEVEL
+\gdef\setvstate@jaskc{%
+ \gdef\ndline##1##2##3{%
+ \have@jaskb{##1.}{}{##2}{##3}%
+ }%
+}
+
+\gdef\setystate@jaskc{%
+ \gdef\ndline##1##2##3{%
+ \hypo@jaskb{##1.}{}{##2}{##3}%
+ }%
+}
+
+\gdef\setJcondblock@jaskc{%
+ \gdef\condblock##1##2##3{%
+ \cblock@jaskb{##3}{##1\;}%
+ ##2%
+ }%
+}%
+
+\gdef\setJblockcond@jaskc{%
+ \gdef\blockcond##1##2##3{%
+ \cblock@jaskb{##2}{##1\;}%
+ ##3%
+ }%
+}%
+
+\gdef\setKMcondblock@jaskc{%
+ \gdef\condblock##1##2##3{%
+ \setystate@jaskc
+ ##2%
+ \setvstate@jaskc%
+ \cblock@jaskb{##3}{##1\;}%
+ }%
+}%
+
+\gdef\setKMblockcond@jaskc{%
+ \gdef\blockcond##1##2##3{%
+ \setystate@jaskc
+ ##3%
+ \setvstate@jaskc%
+ \cblock@jaskb{##2}{##1\;}%
+ }%
+}%
+
+\gdef\condblock#1#2#3{}
+\gdef\blockcond#1#2#3{}
+\gdef\ndline#1#2#3{}
+
+\newcommand{\Jproof}[1]{
+ \setstylej@jaska%
+ \setvstate@jaskc
+ \setJcondblock@jaskc
+ \setJblockcond@jaskc
+ \outer@jaskb{#1}%
+}
+
+\newcommand{\KMproof}[1]{
+ \setstylekm@jaska%
+ \setvstate@jaskc%
+ \setKMcondblock@jaskc
+ \setKMblockcond@jaskc
+ \outer@jaskb{#1}%
+}
+
+\newcommand{\proofline}[2]{
+ \ndline{}{#1}{#2}
+}
+
+\newcommand{\cablk}[3][]{
+ \blockcond{#1}{#2}{#3}
+}
+
+\newcommand{\cbblk}[3][]{
+ \condblock{#1}{#2}{#3}
+}
+
+
+\makeatother
diff --git a/macros/latex/contrib/natded/natded.tex b/macros/latex/contrib/natded/natded.tex
new file mode 100644
index 0000000000..ebff9e7bb8
--- /dev/null
+++ b/macros/latex/contrib/natded/natded.tex
@@ -0,0 +1,218 @@
+%---|----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}