summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/bussproofs/BussGuide2.tex
blob: 35bb699f4b3a4d1527f72a000ace20003152b01d (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
%
%Documentation by Peter Smith, July 2004, March 2012
%
%comments to peter_smith@me.com
%

\documentclass[11pt]{article}
\usepackage{graphicx}
\usepackage{amssymb}
%\usepackage{epstopdf}

\usepackage{bussproofs}
\def\fCenter{{\mbox{$\vdash$}}}

\DeclareGraphicsRule{.tif}{png}{.png}{`convert #1 `basename #1 .tif`.png}

\textwidth = 6.5 in
\textheight = 9 in
\oddsidemargin = 0.0 in
\evensidemargin = 0.0 in
\topmargin = 0.0 in
\headheight = 0.0 in
\headsep = 0.0 in
\parskip = 0.0in
\parindent = 0.2in


\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}

\begin{document}

%%%%%%%%%%%%%%%%%%
%%% 
%%% front matter
%%%
%%%%%%%%%%%%%%%%%%

\thispagestyle{empty}
\begin{center}
	\Huge{\LaTeX\ for Logicians}\\[16pt]
	\huge{\texttt{bussproofs.sty}}\\[8pt]
	\huge{A User Guide}\\[16pt]
\end{center}
\vspace{0.5in}
\tableofcontents
\vspace{0.3in}
\begin{center}
	\fbox{\parbox{4.5in}{\begin{center}The latest version of \texttt{bussproofs.sty}
	 is 1.1, July 2011.\end{center}}}
\end{center}
\vspace{0.4in}
\begin{center}
	\small{Guide version 1.1 March 2012. Corrections/suggestions to
	\texttt{peter}\_$\!$\_\texttt{smith@me.com}}
	\\
	\small{\LaTeX\ for Logicians is at \texttt{http://www.logicmatters.net}}
\end{center} 
\newpage

%%%%%%%%%%%%%%%%%%
%%% 
%%% main matter
%%%
%%%%%%%%%%%%%%%%%%
\section{Introduction}

\noindent Sam Buss's powerful and flexible package {\texttt{bussproofs.sty}} offers macros for setting natural deduction and sequent proofs in two different styles. The key difference between the two styles is illustrated by the difference between
\begin{prooftree}
\AxiomC{$\Gamma, A, B \vdash C$}
\UnaryInfC{$\Gamma, A \vdash (B \to C)$}
\UnaryInfC{$\Gamma  \vdash (A \to (B \to C))$}
\end{prooftree}
and
\begin{prooftree}
\Axiom$\Gamma, A, B\ \fCenter\ C$
\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
\end{prooftree}
In one style, the sequents above and below the inference line are centered; in the other, the sequents are placed so as to align their deducibility signs. 

We can divide {\texttt{bussproofs.sty}}'s  commands for building  proofs into four types:
\begin{itemize}\setlength{\itemsep}{0.0in}
\item \emph{the structural commands} for producing proof trees in the  \emph{centering} style;
\item \emph{more structural commands} for producing proof trees in the  \emph{sequent-aligning} style;
\item \emph{additional commands} for adding labels, and changing the setting of inference lines (selecting double, dashed lines, etc.);
\item \emph{fine-tuning commands} for adjusting the spacing and layout of the proof. 
\end{itemize}
{\texttt{bussproofs.sty}} also provides an additional command which enables some very laconic shorthand for the most commonly used commands. We describe these in Section~\ref{abbrev}; but we avoid using shorthand until the full commands have been explained and made familiar.



\section{`Centered' proofs: the structural commands}
\subsection{The commands} There are four basic proof-building commands for producing proofs in the centered style:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\AxiomC{=\textit{form}\verb=}=
\item   \verb=\UnaryInfC{=\textit{form}\verb=}=
\item   \verb=\BinaryInfC{=\textit{form}\verb=}=
\item   \verb=\TrinaryInfC{=\textit{form}\verb=}=
\end{description}
\end{quote}  
where `\textit{form}' holds the place for a formula or sequent. Note
\begin{itemize}\setlength{\itemsep}{0.0in}
\item The use of the surrounding `\verb={}='s is mandatory. 
\item By default, \textit{form} is set in text mode: if you want to set some or all of \textit{form} in math mode, then you need to use \verb=$='s in the usual way.
\end{itemize}
Chaining a series of those commands, however, is not enough to cause a proof to be set. To display a proof you must use one of
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\DisplayProof=, a command placed at the end of a list of proof-building commands, which produces an in-line proof at the current insertion point.
\item   \verb=\begin{prooftree} ... \end{prooftree}=, an environment which contains a list of proof-building commands, and which produces a  proof in a centered display. 
\end{description}
\end{quote}  
Again, note
\begin{itemize}\setlength{\itemsep}{0.0in}
\item The \verb=\DisplayProof= command  allows you to put proofs anywhere normal text might appear; for example, in a paragraph, in a table, in a tabbing environment, etc. 
\item To generate a proof in a centered display, do \emph{not} use \verb=$$ ... $$= or \verb=\[ ... \]=.
\end{itemize}

\subsection{Usage} It will be a \emph{lot} clearer if we start with examples rather than begin with an abstract description of the principles for chaining proof-building commands! So here goes \ldots
\begin{quote}
\begin{verbatim}
\AxiomC{A}
\UnaryInfC{D}
\DisplayProof
\end{verbatim}
\end{quote}
produces the one-step proof
\AxiomC{A}
\UnaryInfC{D}
\DisplayProof
in the current line. While
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\BinaryInfC{D}
\end{prooftree}
\end{verbatim}
\end{quote}
displays the proof 
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\BinaryInfC{D}
\end{prooftree}
centered and set off from the surrounding text. So it will be no surprise to learn that
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\AxiomC{C}
\TrinaryInfC{D}
\end{prooftree}
\end{verbatim}
\end{quote}
produces the proof
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\AxiomC{C}
\TrinaryInfC{D}
\end{prooftree}
Two comments:
\begin{itemize}\setlength{\itemsep}{0.0in}
\item You'll get an error message if there's a mismatch between the arity of the \verb=\...aryInfC= command and the number of inputs.
\item \texttt{bussproof.sty} does not allow arbitrary numbers of premisses appearing as separate \textit{form} items above the inference line.
\end{itemize}

So much for one-step proofs. Now things get a little more fun \ldots. 
Consider
\begin{quote}
\begin{verbatim}
\begin{prooftree}
     \AxiomC{A}
     \AxiomC{B}
     \AxiomC{C}
     \BinaryInfC{D}
     \BinaryInfC{E}
\end{prooftree}
\end{verbatim}
\end{quote}
This produces the proof
\begin{quote}
\begin{prooftree}
\AxiomC{A}
\AxiomC{B}
\AxiomC{C}
\BinaryInfC{D}
\BinaryInfC{E}
\end{prooftree}
\end{quote}
Why? Think of the first \verb=\BinaryInfC= command as `using up' as premisses the two axioms immediately above it. Then the second \verb=\BinaryInfC= command takes as premisses `D' immediately above it and then searches up to the next `unused' item, i.e. `A'. The inputs to a particular \verb=\BinaryInfC= command are then set right-to-left in the order in which the {command} finds them as it looks {up} the series of commands. Which means, as we want, that {the inputs to a particular inference are set left-to-right in the same order as they occur in the chain of commands}.

It probably helps if we set out the proof-building commands like this:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{A}
                 \AxiomC{B}
                           \AxiomC{C}
                     \BinaryInfC{D}
        \BinaryInfC{E}
\end{prooftree}
\end{verbatim}
\end{quote}
That pretty much replicates the layout of the tree we want. This indeed is one of the \emph{very} nice features of \texttt{bussproofs.sty} -- the instructions to build a proof-tree can be set out to look very like the proof we want. 

Suppose then that we want to set a tree that is arranged like this:
\begin{prooftree}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\end{prooftree}
The following does the trick:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{A}
   \UnaryInfC{B}
                 \AxiomC{C}
        \BinaryInfC{D}
                                \AxiomC{E}
                                              \AxiomC{F}
                                    \BinaryInfC{G}
                                    \UnaryInfC{H}
                    \BinaryInfC{J}
\end{prooftree}
\end{verbatim}
\end{quote}
In sum, then, the rule to produce a given tree is
\begin{quote}
\emph{Set out the commands for the left-hand sub-proof first; and then within a sub-proof, do its left-hand sub-sub-proof first; and so on.}
\end{quote}
Two more points about general structure: 
\begin{itemize}\setlength{\itemsep}{0.0in}
\item The command \verb=\noLine= can be inserted before any inference command to suppress the drawing of an inference line.
\item Null axioms are allowed! 
\end{itemize}
Hence, the commands
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{$A \lor B$}
         \AxiomC{[$A$]}
         \noLine
         \UnaryInfC{$C$}
              \AxiomC{[$B$]}
              \noLine
              \UnaryInfC{$C$}
         \TrinaryInfC{$C$}
\end{prooftree}
\end{verbatim}
\end{quote}
yield
\begin{prooftree}
\AxiomC{$A \lor B$}
\AxiomC{[$A$]}
\noLine
\UnaryInfC{$C$}
\AxiomC{[$B$]}
\noLine
\UnaryInfC{$C$}
\TrinaryInfC{$C$}
\end{prooftree}
And we can use the fact that null axioms are allowed to generate natural deduction proofs with formulae overlined to indicate the discharge of premisses (by treating the formula to be overlined as a unary inference from a null axiom). For example:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{$P$}
                   \AxiomC{}
                   \UnaryInfC{$\neg P$}
          \BinaryInfC{$\bot$}
          \UnaryInfC{$\neg\neg P$}
\end{prooftree}
\end{verbatim}
\end{quote}
generates the proof
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}

\subsection{More than three premisses}

So far we've only considered inference steps that take one premiss (like double negation), two premisses (like modus ponens), or three inputs (like or-elimination). But Buss proofs in fact supplies -- should you want it -- the capacity to deal with four or five premisses. The syntax is as you would expect. We have the two commands
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\QuaternaryInfC{=\textit{form}\verb=}=
\item   \verb=\QuinaryInfC{=\textit{form}\verb=}=
\end{description}
\end{quote}  
These aren't pointless! After all, you might want to illustrate the $\omega$-rule thus:
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\AxiomC{$\varphi(0)$}
\AxiomC{$\varphi(1)$}
\AxiomC{$\varphi(2)$}
\AxiomC{$\varphi(3)$}
\AxiomC{$\ldots$}
\QuinaryInfC{$\forall n\varphi(n)$}
\end{prooftree}
\end{verbatim}
\end{quote}
to give
\begin{quote}
\begin{prooftree}
\AxiomC{$\varphi(0)$}
\AxiomC{$\varphi(1)$}
\AxiomC{$\varphi(2)$}
\AxiomC{$\varphi(3)$}
\AxiomC{$\ldots$}
\QuinaryInfC{$\forall n\varphi(n)$}
\end{prooftree}
\end{quote}




\section{`Sequent-aligned' proofs: the structural commands}
\subsection{The commands} There are four basic proof-building commands for producing proofs in the second style:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\Axiom$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\UnaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\BinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\TrinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\end{description}
\end{quote}  
where `\textit{form}' holds the place for a formula or formulae, and \verb=\fCenter= marks the point of alignment.
\begin{itemize}\setlength{\itemsep}{0.0in}
\item This time, the use of the surrounding `\verb=$='s is mandatory; and material between the `\verb=$='s is set in math mode.
\item The `\verb=\fCenter=' is by default just a place-marker; however, it can be redefined to be printed character such as a sequent arrow or turnstile.
\end{itemize}
And for multi-premiss usage, we also have the additional commands:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\QuaternaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
\item   \verb=\QuinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=\end{description}
\end{quote}  

\subsection{Usage}
The basic usage is illustrated by the following:
\def\fCenter{}
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\Axiom$A, B, C, D,\fCenter\ E, F$
\UnaryInf$A, B,\fCenter\ C,  D, E, F$
\end{prooftree}
\end{verbatim}
\end{quote}
\begin{prooftree}
\Axiom$A, B, C, D,\fCenter\ E, F$
\UnaryInf$A, B,\fCenter\ C,  D, E, F$
\end{prooftree}
Now let's redefine \verb=\fCenter= to be the turnstile surrounded by spaces. Then
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\def\fCenter{\ \vdash\ }
\Axiom$A, B, C, D \fCenter E, F$
\UnaryInf$A, B \fCenter C,  D, E, F$
\end{prooftree}
\end{verbatim}
\end{quote}
produces 
\begin{prooftree}
\def\fCenter{\ \vdash\ }
\Axiom$A, B, C, D \fCenter E, F$
\UnaryInf$A, B \fCenter C,  D, E, F$
\end{prooftree}
However, it is in general preferable to redefine \verb=\fCenter= using an \verb=\mbox= as in the next example (this allows more options):
\begin{quote}
\begin{verbatim}
\def\fCenter{\mbox{\Large$\rightarrow$}}
\begin{prooftree}
\Axiom$\Gamma, A, B\ \fCenter\ B$
\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
\end{prooftree}
\end{verbatim}
\end{quote}
produces
\def\fCenter{\mbox{\Large$\rightarrow$}}
\begin{prooftree}
\Axiom$\Gamma, A, B\ \fCenter\ B$
\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
\end{prooftree}
And this time, since the \verb=\def\fCenter{...}= command precedes the following \verb=prooftree= environment, it will stay in effect until overridden later in the document. 
\begin{itemize}
\item The chaining of multiple sequent-aligning commands to build complex proofs works just as with the earlier centering-style commands.
\item It should go without saying that the point of the \verb=\BinaryInf$...$= command is not to align the sequent turnstile, (arrow, or whatever) in the conclusion of the two-premiss inference with the turnstiles in the premisses, but to provide a new alignment point for later sequents. 
\item Mixing and matching sensible combinations of \verb=C{...}=-type centering commands and \verb=$...$=-type sequent-aligning commands is in fact legitimate. 
\end{itemize}
Thus, to illustrate the last point,  
\begin{quote}
\begin{verbatim}
\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}
\AxiomC{$\Gamma \vdash A$}
\AxiomC{$A, B \vdash C$}
\BinaryInf$\Gamma, B \fCenter C$
\UnaryInf$\Gamma \fCenter B \to C$
\end{prooftree}
\end{verbatim}
\end{quote}
is acceptable, and yields
\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}
\AxiomC{$\Gamma \vdash A$}
\AxiomC{$A, B \vdash C$}
\BinaryInf$\Gamma, B \fCenter C$
\UnaryInf$\Gamma \fCenter B \to C$
\end{prooftree}



\section{Additional layout commands}
Conventionally, the proof
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}
needs labelling. This section describes how to add labels to proofs, and also how to change the style of inference-line (to double lines, etc.).

\subsection{Adding labels} There are two commands for decorating a proof with labels:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\LeftLabel{text}= 
\item   \verb=\RightLabel{text}=
 \end{description}
\end{quote}  
These put \verb=text= as a label to the left/right of the next inference line (and they work even if \verb=\noLine= is used and line isn't actually drawn).

So, for example, the commands
\begin{quote}
\begin{verbatim}
\begin{prooftree}
         \AxiomC{$\Gamma, A \vdash B$}
    \LeftLabel{Conditional Proof:}
         \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
\end{verbatim}
\end{quote}
will generate
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \LeftLabel{Conditional Proof:}
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
You can insert spacing commands and other text commands into the label text, so e.g. substituting  \verb=\LeftLabel{Conditional Proof:\quad}= will generate
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \LeftLabel{Conditional Proof:\quad}
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
However, there is also a global command for adjusting the position of labels, and in general it might be better to use that. 

You can reduce the size of the label font, so that 
\begin{quote}
\begin{verbatim}
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
				  \RightLabel{\scriptsize(1)}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \RightLabel{\scriptsize(1)}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}
\end{verbatim}
\end{quote}
will set the conventionally annotated proof
\begin{prooftree}
   \AxiomC{$P$}
   				  \AxiomC{}
				  \RightLabel{\scriptsize(1)}
                   \UnaryInfC{$\neg P$}
        \BinaryInfC{$\bot$}
        \RightLabel{\scriptsize(1)}
        \UnaryInfC{$\neg\neg P$}
\end{prooftree}
\subsection{Varieties of inference lines} The inference line between premiss and derived conclusion defaults, as we've seen, to a single solid line. But this can be changed, either locally or more globally. The local change commands are
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\noLine=
\item   \verb=\singleLine=
\item   \verb=\doubleLine=
\item   \verb=\solidLine=
\item   \verb=\dottedLine=
\item   \verb=\dashedLine=
\end{description}
\end{quote}
Each applies to the next inference, and line-\emph{number} and line-\emph{type} commands can be combined: so, for example,
\begin{quote}
\begin{verbatim}
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \doubleLine\dashedLine
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
\end{verbatim}
\end{quote}
produces the following:
\begin{prooftree}
     \AxiomC{$\Gamma, A \vdash B$}
     \doubleLine\dashedLine
     \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
\end{prooftree}
There are corresponding global commands that can be placed anywhere in a proof and will affect all succeeding lines unless and until overridden.
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\alwaysNoLine=
\item   \verb=\alwaysSingleLine=
\item   \verb=\alwaysDoubleLine=
\item   \verb=\alwaysSolidLine=
\item   \verb=\alwaysDottedLine=
\item   \verb=\alwaysDashedLine=
\end{description}
\end{quote}
Here `succeeding lines' means `succeeding in the (vertical) order that commands are given' not `logically succeeding'. (Note: Sam Buss comments that \verb=\alwaysNoLine= is `untested': but it seems to work fine on my trials.)

So, for example, the commands
\begin{quote}
\begin{verbatim}
\begin{prooftree}
     \alwaysNoLine
     \AxiomC{$\Pi_1$}
     \UnaryInfC{$A$}
               \AxiomC{[$A$]}
               \UnaryInfC{$\Pi_2$}
               \UnaryInfC{$B$}
               \alwaysSingleLine
               \UnaryInfC{$A \to B$}
         \BinaryInfC{$B$}
\end{prooftree}
\end{verbatim}
\end{quote}
produces the following:
\begin{prooftree}

\alwaysNoLine
\AxiomC{$\Pi_1$}
\UnaryInfC{$A$}
\AxiomC{[$A$]}
\UnaryInfC{$\Pi_2$}
\UnaryInfC{$B$}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\BinaryInfC{$B$}
\end{prooftree}

\subsection{Turning a proof upside down}

Suppose you want to set a proof-tree the other way up, i.e. get a \emph{downward} branching tree with the root at the \emph{top}. Then you need the command \verb=\rootAtTop=. Note, this applies only to the current proof. If you want to make this behaviour persistent, then use \verb=\alwaysRootAtTop=. (The default behaviour can be restored using \verb=\rootAtBottom= and \verb=\alwaysRootAtBottom=.)


\section{Fine-tuning the proof layout}
\texttt{bussproofs.sty} allows a lot of user-modification of the default style of proof lay-out, either by global modifications of parameters, or by local tweakings within a proof. We'll divide these commands into
\begin{itemize}\setlength{\itemsep}{0.0in}
\item commands for determining \emph{where a whole proof is set};
\item commands for \emph{adjusting the `geometry' within a proof};
\item commands for \emph{redefining line styles}.
\end{itemize}

\subsection{Where a proof is set}

\noindent\textbf{i}\quad The amount of \emph{space above and below} a proof-tree display is set by the parameter
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item    \verb=\proofSkipAmount=  
\end{description}
\end{quote}
Its default setting is \verb={\vskip.8ex plus.8ex minus.4ex}=. This can be modified, and negative values of \verb=\vskip= are accepted. 

To change the space above the tree (which you'll want to do if the top lines are null axioms, which generate additional white space), use \verb=\def\proofSkipAmount{\vskip= \emph{new-skip}\verb=}= \emph{before} the opening command \verb=\begin{prooftree}=; the size of the skip after the proof can then be reset by another \verb=\def\proofSkipAmount{...}= command before the proof closes.

\vspace{12pt}\noindent\textbf{ii}\quad  Whole proofs set using the proof-tree environment can be \emph{nudged sideways} by using the command \verb=\hskip= \emph{nudge} (no brackets!) placed e.g. immediately after the command \verb=\begin{prooftree}=. A positive value of \emph{nudge} such as \verb=0.5in= shifts the proof to the right, a negative value such as \verb=-20pt= shifts the proof left.

\EnableBpAbbreviations
\vspace{4pt}\noindent\textbf{iii}\quad  For \emph{vertical positioning of in-line proofs}, compare \AXC{$\phi \land \psi$}\UIC{$\phi$}\DP with \centerAlignProof\AXC{$\phi \land \psi$}\UIC{$\phi$}\DP and \bottomAlignProof\AXC{$\phi \land \psi$}\UIC{$\phi$}\DP\hspace{-6pt}. The first is set vertically centered within the current line (the default position), the second is set rather lower so (at least with a one-step proof) the inference line is on a level with the foot of the current line, and the third is set with the conclusion aligned to the current line. To produce the second tree, use the command \verb=\centerAlignProof=; to produce the third tree, use \verb=\bottomAlignProof=; to restore the default positioning
use \verb=\normalAlignProof=.

\subsection{Layout within a proof}
In this section, we consider the use of

\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\ScoreOverhang= (controls how far inference lines `overhang' the premisses/conclusion)
\item   \verb=\extraVskip= (controls the extra space above and below lines)
\item   \verb=\labelSpacing= (controls horizontal space separating labels and inference lines)
\item   \verb=\defaultHypSeparation= (controls horizontal spread of proof tree)
\item   \verb=\insertBetweenHyps= (can be used to adjust position of hypotheses in next inference)
\item    \verb=\kernHyps= (nudges hypotheses left or right)
\end{description}
\end{quote}

\noindent\textbf{i}\quad The default setting of \verb=\ScoreOverhang= is \verb={4pt}=. This produces e.g. the tree
\begin{prooftree}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\end{prooftree}
Inserting, for example, the line \verb=\def\ScoreOverhang{1pt}= at the beginning of the chain of proof-commands changes (improves!?) the look of the tree by reducing the `overhang' of inference lines:
\begin{prooftree}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\end{prooftree}
\vspace{12pt}
\noindent\textbf{ii}\quad The default setting of \verb=\extraVskip= is \verb={2pt}=, which inserts 2 pt spacing above and below an inference line, as in the last two proofs. To increase this throughout the proof, use e.g.  the line \verb=\def\extraVskip{3pt}= at the beginning of the chain of proof-commands to get
\begin{prooftree}
\def\extraVskip{3pt}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\end{prooftree}
You can also change the interline skip on the fly, during a proof, to improve alignments. Thus compare
\begin{center}
\alwaysNoLine
\AxiomC{$\Pi_1$}
\UnaryInfC{$A$}
\AxiomC{[$A$]}
\UnaryInfC{$\Pi_2$}
\UnaryInfC{$B$}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\BinaryInfC{$B$}
\DisplayProof
\hspace{24pt}
\alwaysNoLine
\AxiomC{$\Pi_1$}
\def\extraVskip{1pt}\UnaryInfC{$A$}
\AxiomC{[$A$]}
\def\extraVskip{2pt}
\UnaryInfC{$\Pi_2$}
\UnaryInfC{$B$}
\def\extraVskip{2.5pt}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\BinaryInfC{$B$}
\DisplayProof
\end{center}
Here, the proof on the left was created by using the default settings, and the one on the right was created by the following commands (with the two proofs being set in the same line in a \verb=\begin{center} ... \end{center}= environment):
\begin{quote}
\begin{verbatim}
\alwaysNoLine
\AxiomC{$\Pi_1$}
\def\extraVskip{1pt}
\UnaryInfC{$A$}
          \AxiomC{[$A$]}
          \def\extraVskip{2pt}
          \UnaryInfC{$\Pi_2$}
          \UnaryInfC{$B$}
          \def\extraVskip{2.5pt}
          \alwaysSingleLine
          \UnaryInfC{$A \to B$}
     \BinaryInfC{$B$}
\DisplayProof
\end{verbatim}
\end{quote}

\vspace{4pt}
\noindent\textbf{iii}\quad The default setting of \verb=\labelSpacing= is \verb={3pt}=, which inserts 3 pt between inference lines and their associated labels. To change this, use the command \verb=\def\labelSpacing{=\emph{new-space}\verb=}= at the beginning of a chain of proof-commands. For example
\begin{prooftree}
\def\extraVskip{2pt}
\def\labelSpacing{8pt}
\def\ScoreOverhang{1.2pt}
\AxiomC{$(\phi \land \psi)$}
\UnaryInfC{$\psi$}
\AxiomC{}
\RightLabel{\scriptsize(1)}
\def\extraVskip{1pt}
\UnaryInfC{$\neg\psi$}
\def\extraVskip{2pt}
\BinaryInfC{$\bot$}
\RightLabel{\scriptsize(1)}
\UnaryInfC{$\neg(\psi \land \phi)$}
\end{prooftree}
is set with \verb=\def\labelSpacing{8pt}=.




\vspace{12pt}

\noindent\textbf{iv}\quad The default setting of \verb=\defaultHypSeparation= is \verb={\hskip.2in}=. Increase this to spread out a spread out a proof horizontally, decrease it to squeeze the proof. Thus compare
\begin{center}
\def\defaultHypSeparation{\hskip .1in}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\DisplayProof
\hspace{24pt}
\def\defaultHypSeparation{\hskip.5in}
\def\ScoreOverhang{1pt}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\psi$}
\AxiomC{$\phi \land \psi$}
\UnaryInfC{$\phi$}
\BinaryInfC{$\psi \land \phi$}
\DisplayProof
\end{center}
where the proof commands for the left tree start \verb=\def\defaultHypSeparation{\hskip .1in}=, and for the right tree start \verb=\def\defaultHypSeparation{\hskip .5in}=.

\vspace{12pt}
\noindent\textbf{v}\quad Use the command \verb=\insertBetweenHyps{=\emph{stuff}\verb=}= before a binary or trinary inference command to insert \emph{stuff} between the hypotheses of that inference. The obvious use of this is to adjust the spacing between the hypotheses of that inference, by using e.g. 
\verb=\insertBetweenHyps{\hskip -4pt}=.

\vspace{12pt}
\noindent\textbf{vi}\quad Use the command \verb=\kernHyps{=\emph{kern}\verb=}= before an inference command to nudge the hypotheses of that inference right by the distance \emph{kern}, e.g. \verb=4pt=. Negative values of \emph{kern} nudge the hypotheses to the left.

\subsection{Inference-line styles}

In this section, we consider the use of

\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\ruleScoreFiller= (sets the style of solid rules)
\item   \verb=\dottedScoreFiller= (sets the style of dotted rules)
\item   \verb=\dashedBuildScore= (sets the style of dashed rules)
\end{description}
\end{quote}
\noindent\textbf{i}\quad The default setting of \verb=\ruleScoreFiller= is \verb={\hrule}=, and in \LaTeX\ an unqualified \verb=\hrule= command produces a horizontal line of thickness 0.4 pt. To change the rule's thickness, use the command \verb=\def\ruleScoreFiller{\hrule height= \emph{new-thickness}\verb=}=.

\vspace{12pt}
\noindent\textbf{ii}\quad The default setting of \verb=\dottedScoreFiller= is \verb={\hbox to4pt{\hss.\hss}}=. The default for \verb=\dashedBuildScore= is \begin{quote}
\verb={\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}=
\end{quote} Both defaults can be altered to produce any other desired type of line.
 
\section{Abbreviating the commands}\label{abbrev}
Using the command \verb=\EnableBpAbbreviations= enables some laconic shorthand for various commands:
\begin{quote}
\begin{description}\setlength{\itemsep}{0.0in}
\item   \verb=\AX= and \verb=\AXC= abbreviate \verb=\Axiom= and \verb=\AxiomC=
\item   \verb=\UI= and \verb=\UIC= abbreviate \verb=\UnaryInf= and \verb=\UnaryInfC=
\item   \verb=\BI= and \verb=\BIC= abbreviate \verb=\BinaryInf= and \verb=\BinaryInfC=
\item   \verb=\TI= and \verb=\TIC= abbreviate \verb=\TrinaryInf= and \verb=\TrinaryInfC=
\item   \verb=\DP= abbreviates \verb=\DisplayProof=
\end{description}
\end{quote}
The enabling of these short abbreviations is optional, and users should guard against conflicts with commands  from other
macro packages or their own defined abbreviations.

\end{document}