summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/lplfitch/lplfitch.dtx
blob: e0f8bb4741eda305c2940e08a180ca06083d7feb (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
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
% \iffalse meta-comment
%
% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer, 
% and Richard Zach
% -------------------------------------------------------
% 
% 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.
%
% \fi
%
% \iffalse
%<*driver>
\ProvidesFile{lplfitch.dtx}
%</driver>
%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%<package>\ProvidesPackage{lplfitch}
%<*package>
    [2013/05/16 v0.9 LPL Fitch style]
%</package>
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{lplfitch}[2013/05/16]
\usepackage{hyperref}
\EnableCrossrefs         
\CodelineIndex
\RecordChanges
\begin{document}
  \DocInput{lplfitch.dtx}
  \PrintChanges
  \PrintIndex
\end{document}
%</driver>
% \fi
%
% \CheckSum{0}
%
% \CharacterTable
%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
%   Digits        \0\1\2\3\4\5\6\7\8\9
%   Exclamation   \!     Double quote  \"     Hash (number) \#
%   Dollar        \$     Percent       \%     Ampersand     \&
%   Acute accent  \'     Left paren    \(     Right paren   \)
%   Asterisk      \*     Plus          \+     Comma         \,
%   Minus         \-     Point         \.     Solidus       \/
%   Colon         \:     Semicolon     \;     Less than     \<
%   Equals        \=     Greater than  \>     Question mark \?
%   Commercial at \@     Left bracket  \[     Backslash     \\
%   Right bracket \]     Circumflex    \^     Underscore    \_
%   Grave accent  \`     Left brace    \{     Vertical bar  \|
%   Right brace   \}     Tilde         \~}
%
%
% \changes{v0.1}{Aeons ago}{Initial version}
% \changes{v0.9}{2012/05/16}{First public beta}
%
% \GetFileInfo{lplfitch.dtx}
%
% \DoNotIndex{\newcommand,\newenvironment}
%
% \title{The \textsf{lplfitch} package\thanks{This document
%   corresponds to \textsf{lplproof}~\fileversion, dated \filedate.}}
% \author{John Etchemendy \and Dave Barker-Plummer \and Richard Zach}
%
% \maketitle
%
% \section{Introduction}
%
% The package |lplfitch| provides macros for typesetting natural
% deduction proofs in ``Fitch'' style, with subproofs indented and
% offset by scope lines.  It produces proofs in the format used in the
% textbook \href{http://lpl.stanford.edu/}{\textit{Language, Proof,
% and Logic}} by Dave Barker-Plummer, Jon Barwise, and John
% Etchemendy.  The package was originally written by John
% Etchemendy. The current version incorporates changes by Dave
% Barker-Plummer and Richard Zach.
%
% \section{Fitch Proofs by Example}
% \label{sect:proofs-by-example}
%
% In this section we will describe how to typeset the Fitch-style
% natural deduction proof shown in figure~\ref{fig:example-proof}.
% This proof uses all of the macros that we have developed for
% typesetting proofs and therefore serves as a good illustration.
%
% \begin{figure}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \boxedsubproof[3.]{a}{Cube(a)}{
%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
%             }
%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] 
% }
% \caption{An Example Proof}
% \label{fig:example-proof}
% \end{figure}
%
% The commands for producing this proof are given in
% figure~\ref{fig:proof-eg-cmds}.  This proof is a little hard to take
% in all at once, and so in the remainder of this section we will
% describe the development of this proof, which we hope is of use to
% readers.
%
%\begin{figure}
%\begin{verbatim}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \boxedsubproof[3.]{a}{Cube(a)}{
%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
%             }
%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] 
% }
% \end{verbatim}
% \caption{The commands for producing the proof of
% figure~\ref{fig:example-proof}}
% \label{fig:proof-eg-cmds}
% \end{figure}
%
% We recommend developing the commands to typeset a proof from the
% inside out, starting with the most deeply nested subproof.  We also
% recommend ignoring justifications until the proof is complete,
% primarily for simplicity but also because the line numbers are not
% known until the complete proof structure is present.
%
% We begin by writing the lines of the innermost subproof (lines 3--6
% of the main proof).
%
% \begin{quote}
% \begin{tabular}{ll}
% |\pline{Cube(a)}| & \formula{Cube(a)}\\
% |\pline{Cube(a)\lif Small(a)}| & \formula{Cube(a)\lif Small(a)}\\
% |\pline{Small(a)}| & \formula{Small(a)}\\
% |\pline{\exi{x}{Small(x)}}| & \formula{\exi{x}{Small(x)}}
% \end{tabular}
% \end{quote}
%
% The macro |\pline| produces a single line of the proof.  The
% mandatory argument to |\pline| is the formula to appear within the
% step.  You will notice that we have used the macro |\lif| to produce
% an conditional arrow, and |\exi| to produce an existentially
% quantified formula.  These are members of a suite of macros that we
% find convenient for producing formulae.  These are described in
% section~\ref{sect:formulae}.
%
% The |\pline| macro may only be used inside a proof context.  We
% construct such a context by using the |\fitchprf| macro.  This macro
% has two mandatory arguments, corresponding to the premises and the
% body of the proof.  Each argument is a list of lines, separated by a
% newline (|\\|) command.  We therefore embed the lines of our example
% proof like this:
%
% \begin{verbatim}
% \fitchprf{\pline{Cube(a)}}{
%     \pline{Cube(a) \lif Small(a)}\\
%     \pline{Small(a)}\\
%     \pline{\exi{x}{Small(x)}}
% }\end{verbatim}
%
% Typesetting a document containing this command results in
% the proof:
% \begin{quote}
% \fitchprf{\pline{Cube(a)}}{
%     \pline{Cube(a) \lif Small(a)}\\
%     \pline{Small(a)}\\
%     \pline{\exi{x}{Small(x)}}
% }
% \end{quote}
%
% Our next step is to embed this proof as a subproof within the larger
% proof.  This is simply achieved.  We first change the use of
% |\fitchprf| to a |\subproof| command, and then treat this as a line
% of the body of another |\fitchprf| command.  The result of doing
% this is:
%
% \begin{verbatim}
% \fitchprf{\pline{\exi{x}{Cube(x)}}}{
%     \subproof{\pline{Cube(a)}}{
%         \pline{Cube(a)\lif Small(a)}\\
%         \pline{Small(a)}\\
%         \pline{\exi{x}{Small(x)}}
%     }
%     \pline{\exi{x}{Small(x)}}
% }\end{verbatim}
%
% \noindent which yields the proof:
%
% \begin{quote}
% \fitchprf{\pline{\exi{x}{Cube(x)}}}{
%     \subproof{\pline{Cube(a)}}{
%         \pline{Cube(a)\lif Small(a)}\\
%         \pline{Small(a)}\\
%         \pline{\exi{x}{Small(x)}}
%     }
%     \pline{\exi{x}{Small(x)}}
% }
% \end{quote}
%
% \noindent The new outer |\fitchprf| has two elements in the second
% argument, one of which is the subproof that we just wrote and the
% second is a formula.  As we embedded the subproof in the body of the
% main proof we changed the command from |\fitchprf| to |\subproof|,
% the definitions of these two macros are almost identical but for the
% adjustment of vertical spacing after the use of a |\subproof|
% command.  Note that no |\\| command is required after the use of a
% |\subproof| command.
%
% Two further applications of this technique give us the command:
%
% \begin{verbatim}
% \fitchprf{}{
%     \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline{\exi{x}{Cube(x)}}}{
%             \subproof{\pline{Cube(a)}}{
%                 \pline{Cube(a)\lif Small(a)}\\
%                 \pline{Small(a)}\\
%                 \pline{\exi{x}{Small(x)}}
%             }
%             \pline{\exi{x}{Small(x)}}
%         }
%         \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }
% \end{verbatim}
%
% \noindent which produces the proof
%
% \begin{quote}
% \fitchprf{}{
%     \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline{\exi{x}{Cube(x)}}}{
%             \subproof{\pline{Cube(a)}}{
%                 \pline{Cube(a)\lif Small(a)}\\
%                 \pline{Small(a)}\\
%                 \pline{\exi{x}{Small(x)}}
%             }
%             \pline{\exi{x}{Small(x)}}
%         }
%         \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }
% \end{quote}
%
% Notice that the last line contains a long formula, and we have used
% the |\brokenform| command to typeset this formula.  The
% |\brokenform| command takes two arguments, the first is the first
% part of the formula, which will be typeset left justified in the
% space available, while the second argument contains the remaining
% pieces of the formula which will appear in subsequent lines.  These
% lines should be separated by uses of the |\\| command, and each line
% should (usually) be a |\formula|.  These lines will be typeset right
% justified in the available space.
%
% \subsection{Adding Line Numbers}
%
% The |\pline| command takes an optional argument which is the number
% of the line within the proof.  We can simply add these now that we
% have all of the lines of the proof.
%
% \begin{verbatim}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \subproof{\pline[3.]{Cube(a)}}{
%                 \pline[4.]{Cube(a)\lif Small(a)}\\
%                 \pline[5.]{Small(a)}\\
%                 \pline[6.]{\exi{x}{Small(x)}}
%             }
%             \pline[7.]{\exi{x}{Small(x)}}
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }\end{verbatim}
% \noindent which results in the proof:
% \begin{quote}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \subproof{\pline[3.]{Cube(a)}}{
%                 \pline[4.]{Cube(a)\lif Small(a)}\\
%                 \pline[5.]{Small(a)}\\
%                 \pline[6.]{\exi{x}{Small(x)}}
%             }
%             \pline[7.]{\exi{x}{Small(x)}}
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }
% \end{quote}
%
% In the eventual proof, a boxed constant is introduced at line~3.  We
% can convert the simple subproof into a boxed subproof.  We use the
% |\boxedsubproof| macro to achieve this.  The conversion is
% straightforward, we replace the first argument of the |\subproof|
% command which was |{\pline[3.]{Cube(a)}}}| by the three arguments
% |[3.]{a}{Cube(a)}| obtaining
%
% \begin{verbatim}
% \boxedsubproof[3.]{a}{Cube(a)}{
%     \pline[4.]{Cube(a)\lif Small(a)}\\
%     \pline[5.]{Small(a)}\\
%     \pline[6.]{\exi{x}{Small(x)}}
% }\end{verbatim}
%
% \subsection{Adding Justifications}
%
% The final thing that we need to do to complete the desired proof is
% the addition of justifications.  To produce a justified line we need
% to then add the optional justification argument.
%
% \begin{verbatim}\pline[5.]{Small(a)}[\ife{4}{3}]\end{verbatim}
%
% \noindent The \verb|\ife| macro produces a justification using the
% $\lif$-elimination rule of the logic.  This is one of a suite of
% macros that we developed to produce justifications in a uniform
% manner.  These are described in section~\ref{sect:justifications}.
%
% \subsection{Command Reference}
% 
% The |\pline| command can be used to typeset proof lines. It takes
% the formula as a mandatory argument, and line number and
% justification as optional arguments: |\pline|\oarg{line
% number}\marg{formula}\oarg{justification}.  The variant |\fpline|
% works the same, except it produces a focus slider.  In case you want
% to typeset a line in an argument or proof that is not typeset as a
% formula (e.g., plain text), use the |\tline| command. It takes a
% line number as optional argument.
%
% \subsection{Obsolete Commands}
%
% The original version of |lplfitch| set lines of proofs using two
% separate macros, the |\nline| and |\jline| commands.  They are
% superceded by the |\pline| command and are included for backward
% compatibility only.
%
% A numbered line is produced by |\nline|, with the optional argument
% the line number.  A justified line is produced using the
% \verb|\jline| macro, which has one mandatory and one optional
% argument.  The optional argument contains the justification, while
% the mandatory argument must contain {\em all} of the arguments
% previously given to \verb|\nline|.  So the command
%
% \begin{verbatim}\nline[5.]{Small(a)}\end{verbatim}
% 
% \noindent produces exactly the same output as
%
% \begin{verbatim}\jline{[5.]{Small(a)}}\end{verbatim}
% 
% \noindent but notice that both the arguments to \verb|\nline| are
% passed within the single argument to \verb|\jline|. To produce a
% justified line using |\jline|, you would also include the
% justification as an optional argument, say,
%
% \begin{verbatim}\jline{[5.]{Small(a)}}[\life{2}{3}]\end{verbatim}
%
% \section{Logical Formulae}
% \label{sect:formulae}
%
% We set our formulae using sans-serif font and we also need to be in
% math mode because the use of logical connectives.  The
% \verb|\formula| command takes a formula to set as its argument, and
% handles both font and mode change.  If the LPL convention of sans-serif
% formulas is not desired, you can simly redefine |\formula| as
% \begin{verbatim}\renewcommand{\formula}[1]{\ensuremath{#1}}\end{verbatim}
%
% Many of the commands that follow require that they are used in a
% formula, or math, context.
%
% \subsection{Connectives}
%
% We introduce our own (usually) shorter names for logical
% connectives.  All of these commands require a formula context.
%
% \begin{center}
% \begin{tabular}{lc}
% \bf Usage & \bf Output\\
% \hline\\
% \verb|\land| & \formula{\land}\\
% \verb|\lor| & \formula{\lor}\\
% \verb|\lif| & \formula{\lif}\\
% \verb|\liff| & \formula{\liff}\\
% \verb|\lnot| & \formula{\lnot}\\
% \verb|\lfalse| & \formula{\lfalse}\\
% \verb|\lall| & \formula{\lall}\\
% \verb|\lis| & \formula{\lis}
% \end{tabular}
% \end{center}
%
% \subsection{Quantified Formulae}
%
% So that we don't have to think about spacing when setting quantified
% formulae, we defined the commands |\exi| and |\uni|.  Use
% |\exi{x}{P(x)}| to obtain \formula{\exi{x}{P(x)}}, and
% |\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}| for
% \formula{\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}}, for example.  |\exi|
% and |\uni| require a formula context.
%
% \section{Justifications}
% \label{sect:justifications}
%
% Here are the macros that we have developed to typeset justifications
% within a proof.  These do not require a formula context.
%
% \begin{center}
% \begin{tabular}{ll}
% \bf Usage & \bf Output\\
% \hline\\
% |\landi{2, 3}| &\landi{2, 3}\\
% |\lande{4}|&\lande{4}\\
% |\lori{5}| & \lori{5}\\
% |\lore{6}{7--9}{11--13}| &\lore{6}{7--9}{11--13}\\
% |\lnoti{14--15}| &\lnoti{14-15}\\
% |\lnote{16}| &\lnote{16}\\
% |\lfalsei{17}{19}| &\lfalsei{17}{19}\\
% |\lfalsee{20}|&\lfalsee{20}\\
% |\lifi{21--25}| &\lifi{21--25}\\
% |\life{27}{30}| &\life{27}{30}\\
% |\liffi{33--37}{40-50}|&\liffi{33--37}{40--50}\\
% |\liffe{55}{57}| &\liffe{55}{57}\\
% |\reit{4}|&\reit{4}\\
% |\eqi| &\eqi\\
% |\eqe{7}{11}|&\eqe{7}{11}\\
% |\lalli{9--12}|&\lalli{9--12}\\
% |\lalle{13}|&\lalle{13}\\
% |\lexii{15}| &\lexii{15}\\
% |\lexie{17}{18-30}| &\lexie{17}{18--30}\\
% \end{tabular}
% \end{center}
%
% \section{Other Macros}
% \label{sect:other-macros}
%
% \subsection{Arguments}
%
% When you want to typeset an argument, for example when setting an
% exercise requiring the proof of some conclusion from a collection of
% premises, you should use the |\fitcharg| command.  This command
% takes two arguments, both mandatory, the premise lines which are set
% above the Fitch bar, and the conclusion lines, which go below.
% Here's an example.  The argument
%
%\begin{quote}
%  \fitcharg{\formula{P(a)}\\ \formula{Q(a)}}{\formula{S(a)}}
%\end{quote}
%
%\noindent is typeset by the command:
%\begin{verbatim}\fitcharg{
%     \formula{P(a)}\\ 
%     \formula{Q(a)}
% }{
%     \formula{S(a)}
% }\end{verbatim}
% \noindent Notice that multiple lines are separated by a use of the
% \LaTeX\ command |\\|.
%
% \subsection{Fitch Contexts}
%
% The |\fitchctx| command is used for setting proof fragments which do
% not include the horizontal Fitch bar.  We use these, for example,
% when formally describing the inference rules of our logic.  The
% command below, for example, typesets our description of the rule of
% conditional proof.
%
% Notice here that we use the command |\ellipsesline| to produce a
% line of the ``proof'' containing a vertical ellipses (using the
% |\pline{\vdots}| results in the ellipses not being centered on the
% line).
%
% Another new feature of this situation is the use of the |\fpline|
% command.  This command works just like the |\pline| command and
% produces exactly what the |\pline| command would, except that a
% focus slider appears to the left of the Fitch bar in question.  The
% |\fpline| command does not work in the argument lines of
% |\fitchprf|  or |\fitcharg|.
%
% \begin{verbatim}
% \fitchctx{
%     \subproof{\pline[$n$.]{P}}{
%         \ellipsesline\\
%         \pline[$m$.]{Q}
%     }
%     \fpline{P \lif Q}[\lifi{$n$--$m$}]
% }
% \end{verbatim}
%
% \begin{quote}
% \fitchctx{
%     \subproof{\pline[$n$.]{P}}{
%         \ellipsesline\\
%         \pline[$m$.]{Q}
%     }
%     \fpline{P \lif Q}[\lifi{$n$--$m$}]
% }
% \end{quote}
%
% \section{Other Packages}
%
% Two other \LaTeX{} packages provide functionality to typeset
% Fitch-style proofs. They differ from |lplfitch| in that they set the
% line numbers close to the left edge of the proof, while |lplfitch|
% sets them close to the formula.  Another difference is that subroofs
% can easily be copied and work the same regardless of the depth of
% nesting.
%
% Peter Selinger's package is
% available at
%\begin{quote}
% \href{http://www.mathstat.dal.ca/~selinger/fitch/}{|http://www.mathstat.dal.ca/\~{
% }selinger/fitch/|},
% \end{quote}
% and that by Johan Kl\"uwer at
% \begin{quote}
% \href{http://folk.uio.no/johanw/FitchSty.html}{|http://folk.uio.no/johanw/FitchSty.html|}.
% \end{quote}
%
% \StopEventually{}
%
% \section{Implementation}
%
%    \begin{macrocode}
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL]
%    \end{macrocode}
%
% \begin{macro}{\formula}
% Typesets a formula (in math mode, letters typeset in sans-serif as in LPL
%    \begin{macrocode}
\newcommand*{\formula}[1]{\ensuremath{\sf{#1}}}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Connectives and Quantifiers}
% We provide convenient and short commands for logical symbols.
%    \begin{macrocode}
\newcommand*\lif{\rightarrow}
\newcommand*\liff{\leftrightarrow}
\newcommand*\lfalse{\bot}
\newcommand*\lall{\forall}
\newcommand*\lis{\exists}
%    \end{macrocode}
% The following provide for commands for setting quantified formulae, inserting correct space
% between variable and formula.  It can be redifined using |\renewcommand| if you want to use them but
% want quantifiers set differently (e.g., with parentheses)
%    \begin{macrocode}
\newcommand*{\quant}[3]{#1 #2\;#3}
\newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}}
\newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}}
%    \end{macrocode}
% \subsection{Justifications}
%
% The folowing commands are used to generate justifications, e.g.,
% |\landi{1, 2}| produces ``\landi{1, 2}''.
%    \begin{macrocode}
\newcommand*\intro[1]{\formula{#1\,}{\bf Intro:}}
\newcommand*\elim[1]{\formula{#1\,}{\bf Elim:}}

\newcommand*\landi[1]{\intro{\land} #1}
\newcommand*\lande[1]{\elim{\land} #1}
\newcommand*\lori[1]{\intro{\lor} #1}
\newcommand*\lore[3]{\elim{\lor} #1, #2, #3}
\newcommand*\lnoti[1]{\intro{\lnot} #1} 
\newcommand*\lnote[1]{\elim{\lnot} #1}

\newcommand*\lfalsei[2]{\intro{\lfalse} #1, #2}
\newcommand*\lfalsee[1]{\elim{\lfalse} #1}

\newcommand*\lifi[1]{\intro{\lif} #1}
\newcommand*\life[2]{\elim{\lif} #1, #2}

\newcommand*\liffi[2]{\intro{\liff} #1, #2}
\newcommand*\liffe[2]{\elim{\liff} #1, #2}

\newcommand*\reit[1]{{\bf Reit:} #1}

\newcommand*\eqi[0]{$=\,${\bf Intro}}
\newcommand*\eqe[2]{\elim{=} #1, #2}

\newcommand*\lalli[1]{\intro{\lall} #1}
\newcommand*\lalle[1]{\elim{\lall} #1}

\newcommand*\lexii[1]{\intro{\lis} #1}
\newcommand*\lexie[2]{\elim{\lis} #1, #2}
%    \end{macrocode}
%
% \subsection{Dimensions}
%
% The following dimensions can be redefined with |\setlength|
%
% \begin{macro}{\fitchargwidth}
% Width of formulas in arguments
%    \begin{macrocode}
\newlength{\fitchargwidth}  
\setlength{\fitchargwidth}{3.5in}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchprfwidth}
% Width of formulas in proofs
%    \begin{macrocode}
\newlength{\fitchprfwidth}
\setlength{\fitchprfwidth}{3.0in}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchctxwidth}
% Width of formulas in Fitch contexts
%    \begin{macrocode}
\newlength{\fitchctxwidth}  
\setlength{\fitchctxwidth}{1in}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchsep}
% Distance between scope line and formula
%    \begin{macrocode}
\newlength{\fitchsep}   
\setlength{\fitchsep}{10pt}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Contexts, Arguments, Proofs}
%
% \begin{macro}{\fitchctx} Typesets a Fitch context, e.g., specification of 
% a rule, in which a focus slider is typeset to the left of the conclusion 
%    \begin{macrocode} 
\newcommand{\fitchctx}[1]{%
	\advance \fitchctxwidth by -\fitchsep%
	\advance \fitchctxwidth by .5pt%
	\begin{tabular}[t]{r@{}|p{\fitchctxwidth}@{}l}
 		\phantom{\slider}  \\[-1.75ex]
 		#1 \\[-1.75ex] & & 
 	\end{tabular}
	\advance \fitchctxwidth by \fitchsep%
	\advance \fitchctxwidth by -.5pt%
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchprf} Typesets a fitch proof
%    \begin{macrocode}
\newcommand{\fitchprf}[2]{%
	\advance \fitchprfwidth by -\fitchsep%
	\advance \fitchprfwidth by .5pt%
	\hspace*{.35em}%
	\begin{tabular}[t]{|p{0pt}@{}p{\fitchprfwidth}@{\hspace*{\fitchsep}}l}
 		\multicolumn{3}{@{}l@{}}{\ }\\[-2.35ex]
		  #1 \\ 
		  \ \\[-2.5ex] \cline{1-1}\\[-2ex]
		  #2 \\ \multicolumn{3}{@{}l@{}} \ \\[-2.35ex]
	 \end{tabular}
	\advance \fitchprfwidth by \fitchsep%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\fitcharg} Typesets an argument (without line
% numbers). Takes two arguments, the premises and conclusion lines of
% the argument.
%    \begin{macrocode}
\newcommand{\fitcharg}[2]{
	\advance \fitchargwidth by -\fitchsep%
	\hspace*{.35em}
	\begin{tabular}[t]{|p{\fitchsep}@{}p{\fitchargwidth}@{}}
		\multicolumn{2}{@{}l@{}}{\ }\\[-2.35ex]
		#1 \\ 
		\ \\[-2.5ex] \cline{1-1}\\[-2ex]
 		#2 \\ \multicolumn{2}{@{}l@{}} \ \\[-2.35ex]
	\end{tabular}
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\slider} Typesets the focus arrow.
%    \begin{macrocode}
\newcommand*{\slider}{\mbox{$\triangleright \;$}}
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\pline} Typesets a proof line with an optional line
% number (before the formula argument) and an optional justification
% (after the formula argument)
%    \begin{macrocode}
\def\pline{\@ifnextchar[\@plinenum{\@plinenum[\@empty]}} 
\def\@plinenum[#1]#2{\@ifnextchar[{\@plinex{#1}{#2}}{%
    \@plinex{#1}{#2}[\@empty]}} 
\def\@plinex#1#2[#3]{ & #1\formula{\; #2} & #3} 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fpline} Like |pline| except produces a focus slider
% on the left
%    \begin{macrocode}
\newcommand*\fpline{\slider\pline} 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\tline} Typesets proof line containing text with an
% optional line number.
%    \begin{macrocode}
\newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}}
%    \end{macrocode}
% \end{macro}
%
% The following macros |\nline|, |\jline|, and |\fline|
% are the commands provided in the original version
% of |lplfitch| and are included for backwards compatibility. 
%    \begin{macrocode}
\newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}}
%    \end{macrocode}
% justified line (justification optional)
% |\jline[justification]{args for line}|
%    \begin{macrocode}
\newcommand*{\jline}[2][{}]{\nline#2 & #1}
%    \end{macrocode}
% focused line
%    \begin{macrocode}
\newcommand*{\fline}[1]{\slider \jline#1}
%    \end{macrocode}
%
% \begin{macro}{\ellipsesline}
% Producing vertical ellipses in a line on their own.
% This takes care of centering the ellipses in their line.
%    \begin{macrocode}
\newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\subproof}
% This command sets a subproof within a proof.
% The arguments are the line before, and the lines after
% the horizontal fitch bar.
%    \begin{macrocode}
\newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\boxedsubproof}
% Produces a new boxed subproof.
% |\boxedsubproof|\oarg{n}\marg{c}\marg{premise}\marg{body}, where
% \meta{n} is the number of the premise line, \meta{c} is the
% constant(s) to be boxed, \meta{premise} is the premise of the
% subproof, and \meta{body} contains the lines of the subproof.
%    \begin{macrocode}
\newcommand{\boxedsubproof}[4][{}]{
     \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4}
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\brokenform}
% A crude attempt at dealing with a formula which need to be broken to
% fit in the proof.  We take two arguments, the first line of the
% formula which is left justified, and the remainder of the lines,
% which are right justified.  The first argument is set as a
% |\formula| but the second is not (as it may contain line breaks
% itself).
%    \begin{macrocode}
\newcommand{\brokenform}[2]{
   \advance\fitchprfwidth by-\fitchsep
   \begin{tabular}[c]{rp{\fitchprfwidth}}
    \multicolumn{1}{p{\fitchprfwidth}@{}}{\formula{#1}}\\
    \formula{#2}
   \end{tabular}
   \advance\fitchprfwidth by\fitchsep
}
%    \end{macrocode}
% \end{macro}
%
% \Finale
\endinput