summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/natded/extended_doc.tex
blob: ef3dd29af4c69cf76ca11a0f83048d74aa8abef3 (plain)
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
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
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}