1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
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}
|
