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
|
% $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
% Macros for Fitch-style formal proofs
% Johan W. Klüwer, June 10, 2001
\RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
% Line height in proofs
\newlength{\fitchlineht}
\setlength{\fitchlineht}{1.5\baselineskip}
% Horizontal indent between proof levels
\newlength{\fitchindent}
\setlength{\fitchindent}{1em}
% Indent to comment
\newlength{\fitchcomind}
\setlength{\fitchcomind}{2em}
% Line number width
\newlength{\fitchnumwd}
\setlength{\fitchnumwd}{1em}
% Altered from mdwtab.sty: shorter vline, for start of subproof
\makeatletter
\newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
\makeatother
% Ordinary vertical line
\newcommand{\fa}{\vline\hspace*{\fitchindent}}
% Vertical line, shorter: Use at start of (sub)proof
\newcommand{\fb}{\fvline\hspace*{\fitchindent}}
% Hypothesis
\newcommand{\fh}{\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Hypothesis, with longer vert line: for >1 hypothesis
\newcommand{\fj}{\vline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Modal subproof: takes argument = operator
\newcommand{\fitchmodal}[1]{%
\makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
\newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
\newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
% Modal subproof with hypothesis in first line (as in Fitch)
\newcommand{\fitchmodalh}[1]{%
\makebox[0pt][r]{${}^{#1}$\,}%
\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Rule: formula introduction marker. \fr with line, \fs without line
\newcommand{\fr}{%
\makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
\newcommand{\fs}{%
\makebox[0pt][r]{${\rhd}$\,\,}}
% Box around argument, like new variable in ql
\newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
%
\newcounter{fitchcounter}
\setcounter{fitchcounter}{0}
%To avoid starting from 1, \setboolean{resetfitchcounter}{false}
\newboolean{resetfitchcounter}
\setboolean{resetfitchcounter}{true}
%To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
\newboolean{increasefitchcounter}
\setboolean{increasefitchcounter}{true}
%\formatfitchcounter can be altered if need be, though only once per proof
\newcommand{\formatfitchcounter}[1]{\arabic{#1}}
%Typeset the counter
\newcommand{\fitchcounter}{%
\ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
\formatfitchcounter{fitchcounter}}
%A line with a special number -- a tag, e.g. \ftag{\vdots}{}
\newcommand{\ftag}[2]{\multicolumn{1}%
{!{\makebox[\fitchnumwd][r]{#1}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}}%
{#2}}
\newenvironment{fitchnum}%
{\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
\begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter }\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitchunum}%
{\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
\begin{fitchnum}}{\end{fitchnum}}
\newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
\begin{fitchunum}}{\end{fitchunum}}
% The following is useful for giving a numbered formula, then the proof.
\newenvironment{flem}[2]%
{\begin{eqnarray}
\label{#2}\\
&\begin{fitch}}%
{\end{fitch}\notag\end{eqnarray}}
%To write comment field for two consecutive lines, with brace
\newcommand{\ftwocom}[1]{%
\parbox[t]{3cm}{
\raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
$\left.
\begin{aligned}
\,\\ \,
\end{aligned}
\right\}$\quad #1}
}}
|