/:\ecc€ typesets an inference rule.
{\tt} is the position to the right, {\tt} is a formula number used in the inference,
and {\tt} is the rule itself. The parameter {\tt} is either `l', 'm', or `r' to
position the formula number to the left, in the middle, or to the right.
And {\tt} is either `.'\ or `:'\ to output one or two colons after the formula number.
\Example3
The following code
\Epause
\verbatim
\nlp4\ci{\hss\thinspace58\hss}\rep3\*___\*_[-\*-:-\*---\*-:-\ce{$f(b)$}
\nlpc4{$f(A)$}\*_|_\*-:-\ci{$f(A)$}\rep2\*___\*_!_\*___\*_'-\ce{$g(b)$}
\nlp4\*_|_\*_'-\ci{$g(A)$}\rep2\*___\*_'-\*.a.\*-:-\ce{$f(\da)$}
\nlpc4{$c$}\*_|_\ci{$b$} \rep3\*___\*___\*___\*_'-\ce{$g(\da)$}
\bcc4/m30:.\rep3\*___\null \rep6\*---\ecc
\nlpc4{$a$}\*_|_\ci{$f(b)$} \rep2\*___\*_[-\*-:-\*-:-\*,a.\*-:-\ce{$f(\da)$}
\nlpc4{$c$}\*_|_\ci{$g(b)$} \rep2\*___\*___\*_!_\*_!_\*___\*_'-\ce{$g(\da)$}
\nlpc4{$b$}\*_|_\*.a.\*-:-\ci{$f(\da)$} \*___\*_!_\*_'-\*---\*--(\ce{$f(b)$}
\nlp4\*_|_\*___\*_'-\ci{$g(\da)$} \*___\*_'-\*---\*---\*---\ce{$g(b)$}
\fono{59}
\endverbatim\Econt
outputs formula~59 of the {\it Begriffsschrift}:
\smallskip
\nlp4\ci{\hss\thinspace58\hss}\rep3\*___\*_[-\*-:-\*---\*-:-\ce{$f(b)$}
\nlpc4{$f(A)$}\*_|_\*-:-\ci{$f(A)$}\rep2\*___\*_!_\*___\*_'-\ce{$g(b)$}
\nlp4\*_|_\*_'-\ci{$g(A)$}\rep2\*___\*_'-\*.a.\*-:-\ce{$f(\da)$}
\nlpc4{$c$}\*_|_\ci{$b$} \rep3\*___\*___\*___\*_'-\ce{$g(\da)$}
\bcc4/m30:.\rep3\*___\null \rep6\*---\ecc
\nlpc4{$a$}\*_|_\ci{$f(b)$} \rep2\*___\*_[-\*-:-\*-:-\*,a.\*-:-\ce{$f(\da)$}
\nlpc4{$c$}\*_|_\ci{$g(b)$} \rep2\*___\*___\*_!_\*_!_\*___\*_'-\ce{$g(\da)$}
\nlpc4{$b$}\*_|_\*.a.\*-:-\ci{$f(\da)$} \*___\*_!_\*_'-\*---\*--(\ce{$f(b)$}
\nlp4\*_|_\*___\*_'-\ci{$g(\da)$} \*___\*_'-\*---\*---\*---\ce{$g(b)$}
\fono{59}\Eend0
\noindent
One more command is required for collections of inferences:
\item{8.}€\decollator€ outputs a thick line of width €0.\hsize€. The line is
centered. It is preceded and followed by vertical space.
\Example4
Here are some inferences of the {\it Begriffsschrift\/}:
\outof p3,0"1"with\thatis
\formula p9|{..{..a.b}.a}
\followswith p3"8"a.p8s5
\substituting p3 d:a \whichgives
\formula p9|{..{..a.a}.b}
\named "26"
\decollator4
\outof p3,0"26"with b:{..{..a.b}.a} \thatis
\formula p8|{..{=.{..a.a}}.{..{..a.b}.a}}
\followswith p3"1"a:p8s5
\formula p8|{=.{=.{..a.a}}}
\named "27"
The command €\decollator4€ appears after formula~26.
\Eend0
% %%%%%%%%%%%
\beginsection 7. Input of formulas using the ``short form''
This input format reduces the amount of typing compared to the
symbolic representation. It follows given rules and produces as an
intermediate step the code of the symbolic representation.
The input is recursively entered using four constructions:
\smallskip
\item{1.}{\tt=<}sign{\tt>\char"7B<}formula{\tt>\char"7D} to add a
signed content stroke in front of a formula;
\item{2.}{\tt<}sign{\tt><}sign{\tt>\char"7B<}formula{\tt>\char"7D<}%
sign{\tt>\char"7B<}formula{\tt>\char"7D}
to build a signed condition from two signed formulas;
\item{3.}{\tt*<}sign{\tt><}character{\tt><}sign{\tt>\char"7B<}%
formula{\tt>\char"7D} to add a signed
concavity in front of a signed formula;
\item{4.}{\tt!\char92<}nameofdef{\tt><}arguments{\tt>} to insert a
previously defined subformula.
\noindent
Here {\tt<}formula{\tt>} is either a valid formula constructed with
the four rules or a terminal string (both are typeset in math mode)
and {\tt<}sign{\tt>} is one of the following symbols:
\item{\tt.} represents no sign;
\item{\tt-} represents the negation;
\item{\tt+} represents the affirmation.
In rule~4 {\tt<}nameofdef{\tt>} is together with the preceding
backslash a defined control word that has at most three arguments
given in {\tt<}arguments{\tt>}. The control word must define a part
of a formula. This rule implements {\sl macro expansion\/} to avoid
retyping of often used parts in formulas.
Most formulas are created by rules~2 and~3; rule~1 is only needed to
type a single line.
{\it Important note\/}: The braces around {\tt<}formula{\tt>} can be
omitted if the formula is a terminal string that consists of a single
token. Double curly braces are required around terminal strings that
have more than five tokens. But single braces must always be used for
formulas in rules 1--3, which are not terminal strings. (In Example~5
below case~i shows that a single token needs no braces. The cases ii
and~iii show the use of single and double curly braces.)
Formulas that are created by the above rules must be given to the
following commands:
\smallskip
\item{1.}€\frege{}€ where {\tt} is a formula created by the above
stated rules and {\tt} is either `{\tt.}'\ or `{\tt|}'.
\item{2.}€\formula p{}€ adds a position parameter {\tt} to
move the formula {\tt} units to the right.
\noindent
The formula {\tt} is output as a judgment if {\tt} equals
{\tt|}. The command €\frege€ shall be used in running text,
€\formula€ in vertical mode. But €\frege€ doesn't start a paragraph;
use €\indent€ (or €\noindent€) if €\frege€ is the first item
in a paragraph.
\Example5
\def\0#1{*.a.{#1(\da)}}
Here are a few examples for all four rules:
\smallskip
\advance\leftskip by 20pt
\item{i)}€\frege|{=-\gA}€ outputs \frege|{=-\gA}.
\item{ii)}€\frege.{-.\gA-{{g(\ka,\kb)}}}€ outputs \frege.{-.\gA-{{g(\ka,\kb)}}}.
\item{iii)}€\frege.{*-a+{f(\da)}}€ outputs \frege.{*-a+{f(\da)}}.
\item{iv)}€\def\0#1{*.a.{#1(\da)}}€ together with €\frege|{-.\gA-{!\0f}}€
outputs \frege|{-.\gA-{!\0f}}.
\smallskip
\advance\leftskip by -20pt
The output of iv) is nearly the formula of Section~1 (\frege|{..\gA.{!\0f}});
it can be coded (without €\0€) as €\frege|{..\gA.{*.a.{f(\da)}}}€.
\Eend0
Of course, a formula in Frege's notation that has several lines is not
easy to read in a sequential form. The periods and braces do not help
to make the structure of that formula easy to recognize.
I suggest to copy a Frege formula from left to right and from bottom
to top and to use more than one line for the sequential coding.
\Example6
This example shows how to construct in a structured manner the short
form of a given formula, which is written in Frege's notation.
The formula is \frege|{.-{..\gA.\gB}.{*.a.{..\gG-\gD}}}.
Step~1: The formula is a judgment and starts at the left with a
condition, whose upper line contains a negation indicator.
So the coding starts with
\verbatim
\frege|{.-{}.{}}
\endverbatim
Or write it in two lines to make the structure visible:
\verbatim
\frege|{.-{}
.{}}
\endverbatim
Step~2: The bottom part starts with a concavity, so the input becomes
\verbatim
\frege|{.-{}
.{*.a.{}}}
\endverbatim
Step~3: A simple condition comes after the concavity
\verbatim
\frege|{.-{}
.{*.a.{..\gG-\gD}}}
\endverbatim
And the final step is to add the condition in the upper part:
\verbatim
\frege|{.-{..\gA.\gB}
.{*.a.{..\gG-\gD}}}
\endverbatim
\medskip
{\it Note\/}: The input
\verbatim
\frege|{..{-.\gA.\gB}
.{*.a.{..\gG-\gD}}}
\endverbatim
outputs
\frege|{..{-.\gA.\gB}
.{*.a.{..\gG-\gD}}},
which looks very similar to the given formula but, of course,
the negation indicator in the upper part has moved a little bit
to the right.
\Eend0
% %%%%%%%%%%%
\beginsection 8. Inferences of the Begriffsschrift in the ``short form''
Five commands are available to typeset inferences with the short form:
\smallskip
\item{1.}€\outof p,""with\thatis€ starts the inference chain.
The parameter {\tt} is the number of units the output is moved to
the right, {\tt} is a number of a formula, {\tt} is an offset to
position the number {\tt} {\tt} lines lower, and {\tt} is
either empty or a space separated list of pairs {\tt v:F} to indicate
the substitution of {\tt v} by the formula {\tt F}.
\item{2.}€\use p""€ is a shortcut of €\outof€ if the parameters {\tt}
and {\tt} are not needed; {\tt} is set 0 and {\tt} is empty.
\item{3.}€\followswith p""aps€ draws the inference rule and
can be expressed in the €\bcc€ macro of Section~6, no~7, as
€\bcc{}/m{}:\rep(-)\*___\rep{}\*---\ecc€.
\item{4.}€\substituting p \whichgives€ has the usual position parameter
{\tt} and a list of substitutions {\tt} in the above described form {\tt
v:F}.
\item{5.}€\named ""€ outputs the number {\tt} as the number of the
previous formula.
An inference chain is typically typed with the sequence:
\verbatim
\outof ... with ... \thatis
\formula ...
\followswith ...
\substituting ... \whichgives
\formula ...
\named ...
\endverbatim
\noindent
or if no substitution in the first formula is required, the €\outof€ line
is replaced by the simpler €\use€.
\Example7
The formula of Example~3
\smallskip
\outof p4,0"58"with f(A):{..{f(A)}.{g(A)}}
c:b
\thatis
\formula p8|{..{..{f(b)}.{g(b)}}
.{*.a.{..{f(\da)}.{g(\da)}}}}
\followswith p4"30"a.p8s6
\substituting p4 a:{f(b)}
c:{g(b)}
b:{*.a.{..{f(\da)}.{g(\da)}}}
\whichgives
\formula p8|{..{..{*-a.{..{f(\da)}.{g(\da)}}}
-{f(b)}}
.{g(b)}}
\named "59"
\bigskip
has this coding:
\verbatim
\outof p4,0"58"with f(A):{..{f(A)}.{g(A)}}
c:b
\thatis
\formula p8|{..{..{f(b)}.{g(b)}}
.{*.a.{..{f(\da)}.{g(\da)}}}}
\followswith p4"30"a.p8s6
\substituting p4 a:{f(b)}
c:{g(b)}
b:{*.a.{..{f(\da)}.{g(\da)}}}
\whichgives
\formula p8|{..{..{*-a.{..{f(\da)}.{g(\da)}}}
-{f(b)}}
.{g(b)}}
\named "59"
\endverbatim\Eend1
% %%%%%%%%%%%
\beginsection 9. Terminal symbols of the Begriffsschrift
In part~3 of the {\it Begriffsschrift\/} four symbols are
defined. They are available as \TeX\ commands. The commands get more
flexibility than the {\it Begriffsschrift\/} requires as all possible
content can be addressed by parameters.
\item{1.}€\gfvererbe€ with four parameters:
€$\gfvererbe\kd\ka{x(\ka)}{f(\kd,\ka)}$€ outputs
$\gfvererbe\kd\ka{x(\ka)}{f(\kd,\ka)}$.
\item{2.}€\gffolgt€ with three parameters:
€$\gffolgt\kg\kb{f(x_\kg,y_\kb)}$€ outputs $\gffolgt\kg\kb{f(x_\kg,y_\kb)}$.
\item{3.}€\gfgehoertan€ with three parameters:
€$\gfgehoertan\kg\kb{f(x_\kg,z_\kb)}$€ outputs
$\gfgehoertan\kg\kb{f(x_\kg,z_\kb)}$.
\item{4.}€\gfeindeutig€ with three parameters:
€$\gfeindeutig\kd\ke{f(\kd,\ke)}$€ outputs $\gfeindeutig\kd\ke{f(\kd,\ke)}$.
\noindent
I use shortcuts for these special terminal symbols and reduce the
number of parameters to the amount that is used in the text;
see Example~11 below.
% %%%%%%%%%%%
\beginsection 10. Output style of the Grundgesetze
\toggleGGstyle
Frege made changes to the notation in his main work. A command and
several flags are defined to switch from the style of the {\it
Begriffsschrift\/} to the style of the {\it Grundgesetze}.
\smallskip
\item{1.}€\toggleGGstyle€ switches the styles; the default is the style of
the {\it Begriffsschrift}. Several of the changes are global so even
if the switch is made inside a group it shall be called a second time
to switch it back. This happens when it is called for the first time:
\itemitem{a)}€\gfbsuseGGstyletrue€ is set. Together with a call to
€\gfbsneuestriche€ the thickness of the lines is changed.
\itemitem{b)}€\gfbskompakttrue€ is set. This reduces the width of the formulas
that are input with the short form.
\itemitem{c)}€\gfggschlussweisetrue€ is set. This activates more symbols
to express the eight inferences of the {\it Grundgesetze\/} (see Section~12).
\itemitem{d)}€\gfbsfonoohnepunkttrue€ is set. No period after the number of
a formula is set in €\fono€ or €\named€.
\itemitem{e)}€\gfbsnegdirekttrue€ is set. The negation indicator touches
the content stroke.
\item{2.}The flags can be set individually, for example, to get a compact output
but keep the line thicknesses etc.\ of the {\it Begriffsschrift}.
\item{3.}To control the compact output of the generality when the flag
€\gfbskompakttrue€ is set more flags are available. Examples are given to
show how these flags influences the output.
\itemitem{$\alpha$)}The output is not compact if €\gfbskeinekompaktehoehlungtrue€
is set. At the left the flag is false and at the right true; the source code
is €\frege|{..{*-a.{\gY(\da)}}.{*.e.{\gF(\de)}}}€:
\smallskip\indent\indent
{\gfbskompakttrue \gfbskeinekompaktehoehlungfalse
\frege|{..{*-a.{\gY(\da)}}.{*.e.{\gF(\de)}}}
}\quad
{\gfbskompakttrue \gfbskeinekompaktehoehlungtrue
\frege|{..{*-a.{\gY(\da)}}.{*.e.{\gF(\de)}}}
}.
\itemitem{$\beta$)}The output of the short form rule~1 (with the {\tt=}) can
have no effect except if the flag named €\gfbsaussagesichtbartrue€ is set.
At the left the flag is false and at the right true; the line reads
€\frege.{=.a} vs \frege.{=.{=.a}}€:
{\gfbskompakttrue \gfbsaussagesichtbarfalse
\frege.{=.a} vs \frege.{=.{=.a}}
}\quad
{\gfbskompakttrue \gfbsaussagesichtbartrue
\frege.{=.a} vs \frege.{=.{=.a}}
}
{\it Note\/}: Both input forms, the symbolic representation and the
short form, can be used with this style. But only the short form
creates smaller formulas if €\gfbscompakttrue€ is set. The width of a
formula in symbolic representation must be changed manually if it is
not coded with the symbols of the last list in Section~5.
\Example8
Here is the example of Sections 1 and~5; it is coded in the
short form as €\frege|{..\gA.{*.a.{f(\da)}}}€:
\frege|{..\gA.{*.a.{f(\da)}}}.
\Eend0
% %%%%%%%%%%%
\beginsection 11. Setting formulas in parentheses and brackets (Grundgesetze)
In the {\it Grundgesetze\/} some formulas must be placed in
parentheses or brackets. A few commands are provided to make this an
easy task.
\smallskip
\item{1.}€\pfrege{}€ acts like €\frege{}€ and adds parentheses around
this formula. The result is stored in a box with the number {\tt}. In total
there are four boxes for this task.
\item{2.}€\bfrege{}€ is like €\pfrege€ but the formula is placed between
brackets. The pool of boxes is independent from the €\pfrege€ boxes and there are
four boxes.
\item{3.}€\pparens€ places the math {\tt} with parentheses in the box
numbered {\tt}. The boxes are taken from the pool that is available for
€\pfrege€.
\item{4.}€\bparens€ acts like €\pparens€ but it uses brackets and the
pool of boxes of €\bfrege€.
\item{5.}€\pfbox€ outputs box number {\tt} from the €\pfrege€ pool.
\item{6.}€\bfbox€ outputs the box {\tt} from the pool used by €\bfrege€.
\Example9
The following formula appears on page~115 of the {\it Grundgesetze},
vol.~1.
\Epause
\smallskip
\begingroup
\pfrege1.{.-{\ke=c}.{\ke\G^v}}
\pfrege2.{.-{\ke=b}.{\ke\G^u}}
\bfrege1.{-.{\ke=n}.{{\ke\G^\kesl\pfbox1}}}
\bfrege2.{-.{\ke=m}.{{\ke\G^\kesl\pfbox2}}}
\bfrege3.{--{{\ke\G^(\ka\G^q)}}-{..{\ke=b}-{\ka=c}}}
\pfrege1.{-.{\ke=n}.{{\ke\G^\kesl\pfbox1}}}
\pfrege2.{-.{\ke=m}.{{\ke\G^\kesl\pfbox2}}}
\pparens3{\kesl\bfbox1\G^\G>q}
\pparens4{\bfbox1\G^\G>\kasl\kesl\bfbox3}
$$\frege|{..{..{..{{\kesl\pfbox2\G^\pfbox4}}
-{{b\G^\kesl\pfbox2}}}
-{{c\G^\kesl\pfbox1}}}
.{{\kesl\pfbox2\G^\pfbox3}}}
$$
\endgroup
\Econt
And here is the source:
\verbatim
\pfrege1.{.-{\ke=c}.{\ke\G^v}}
\pfrege2.{.-{\ke=b}.{\ke\G^u}}
\bfrege1.{-.{\ke=n}.{{\ke\G^\kesl\pfbox1}}}
\bfrege2.{-.{\ke=m}.{{\ke\G^\kesl\pfbox2}}}
\bfrege3.{--{{\ke\G^(\ka\G^q)}}-{..{\ke=b}-{\ka=c}}}
\pfrege1.{-.{\ke=n}.{{\ke\G^\kesl\pfbox1}}}
\pfrege2.{-.{\ke=m}.{{\ke\G^\kesl\pfbox2}}}
\pparens3{\kesl\bfbox1\G^\G>q}
\pparens4{\bfbox1\G^\G>\kasl\kesl\bfbox3}
\endverbatim\smallskip\verbatim
$$\frege|{..{..{..{{\kesl\pfbox2\G^\pfbox4}}
-{{b\G^\kesl\pfbox2}}}
-{{c\G^\kesl\pfbox1}}}
.{{\kesl\pfbox2\G^\pfbox3}}}
$$\endverbatim\Eend1
% %%%%%%%%%%%
\beginsection 12. Inferences of the Grundgesetze
The list entry~1c of Section~10 needs some explanation as it extends
the list of available symbols for inferences. Two of the symbols have
no output ({\tt?}\ and {\tt>}). In the following list the text in
parentheses contains the sequence €\*?#"€ or €\*?>#€ for the symbol
`{\tt\#}'.
\smallskip
\item{\tt ?} (must be the first in the triple) signals that the next
two symbols build an inference line in the style of the {\it
Grundgesetze\/}. Such symbols use 50\% more space than ordinary symbols.
\item{\tt -}(\*?-") is a single horizontal stroke;
\item{\tt .}(\*?.") is a single (centered) period;
\item{\tt =}(\*?=") is a double stroke;
\item{\tt *}(\*?*") is a single stroke in the height of the upper line of the
double stroke;
\item{\tt\char95 }(\*?_") is an empty space;
\item{\tt "}(\*?"") is a skip;
\item{\tt >}has no output; the next symbol must be a {\sl transition-sign\/}:
\itemitem{\tt x}(\*?>x) it must follow a {\tt >};
\itemitem{\tt u}(\*?>u) it must follow a {\tt >}.
\noindent
Inferences of the {\it Grundgesetze\/} are separated by a new type of line:
\item{1.}€\separator€ outputs a thick line with a centered dot.
\Example{10}
Here is an inference chain from the {\it Grundgesetze\/}:
\smallskip
\advance\rightskip by 2\rightskip
\use p3"III"
\formula p5|{.-{*.f.{..{\df(a)}.{\df(a)}}}-{a=a}}
\nlp{6.5}\*?>x
\formula p5|{..{a=a}.{*.f.{..{\df(a)}.{\df(a)}}}}
\named "$\ka$"
\separator
\use p3"I"
\formula p5|{..{f(a)}.{f(a)}}
\nlp5\*?_"\*?>u
\formula p5|{*.f.{..{\df(a)}.{\df(a)}}}
\named"$\kb$"
\bcc3/m$\ka$:.\*__"\rep3\*?--\ecc
\formula p5|{=.{a=a}}
\named"IIIe"
\rightskip=\leftskip
\medskip
And this is the code:
\verbatim
\use p3"III"
\formula p5|{.-{*.f.{..{\df(a)}.{\df(a)}}}-{a=a}}
\nlp{6.5}\*?>x
\formula p5|{..{a=a}.{*.f.{..{\df(a)}.{\df(a)}}}}
\named "$\ka$"
\separator
\use p3"I"
\formula p5|{..{f(a)}.{f(a)}}
\nlp5\*?_"\*?>u
\formula p5|{*.f.{..{\df(a)}.{\df(a)}}}
\named"$\kb$"
\bcc3/m$\ka$:.\*__"\rep3\*?--\ecc
\formula p5|{=.{a=a}}
\named"IIIe"
\endverbatim\Eend1
% %%%%%%%%%%%
\beginsection 13. Terminal symbols of the Grundgesetze
The {\it Grundgesetze\/} has not such complex constructions as the
{\it Begriffsschrift\/} (see Section~9). But it contains a lot of
special symbols.
\smallskip
\settabs 2 \columns
\def\hsnor#1.{\hbox to 3em{\hss#1.}\ }
\+\hsnor1.€\G!€: $\G!\kx$.&
\hsnor16.€\Gfm€: $u\Gfm q$.\cr
\+\hsnor2.€\kasl€: $\kasl\gF(\ka)$.&
\hsnor17.€\Gsm€: $p\Gsm q$.\cr
\+\hsnor3.€\G^€: $a\G^b$.&
\hsnor18.€\G<€: $p\G€: $\G>p$.&
\hsnor20.€\Ge€: $p\Ge q$.\cr
\+\hsnor6.€\GU€: $\GUorg p$ (or $\GU p$).&
\hsnor21.€\Gc€: $p\Gc q$.\cr
\+\hsnor7.€\Gn€: $\Gnorg u$ (or $\Gn u$).&
\hsnor22.€\Gmf€: $p\Gmf q$.\cr
\+\hsnor8.€\G0€: $\G0$.&
\hsnor23.€\G*€: $\G*t$.\cr
\+\hsnor9.€\G1€: $\G1$.&
\hsnor24.€\G6€: $\G6s$.\cr
\+\hsnor10.€\Gbf€ or €\Gff€: $\Gbf$.&
\hsnor25.€\Gf€: $\Gf s$.\cr
\+\hsnor11.€\G-€: $\G-q$.&
\hsnor26.€\GF€: $s\GF u$.\cr
\+\hsnor12.€\G~€: $\G~q$.&
\hsnor27.€\Gl€: $s\Gl u$.\cr
\+\hsnor13.€\G_€: $p\G_q$.&
\hsnor28.€\Gp€: $\Gp s$.\cr
\+\hsnor14.€\Guu€: $\Guu$.&
\hsnor29.€\Gss€ or €\Gsz€: $s\Gss p$.\cr
\+\hsnor15.€\G;€: $o\G;a$.\cr
\noindent
The symbols are constructed with the Computer Modern
and \AmSTeX\ fonts. But with the external flag €\fgefontsknown€ the
second symbol in numbers 6 and 7 is selected (see Section~3).
Several symbols are rotated and this requires the package {\tt
rotate.tex}. The output of unrotated symbols is activated by default;
the external flag €\let\showrotation=t€ must be given to activate
rotation (see Section~3).
\toggleGGstyle
% %%%%%%%%%%%
\beginsection 14. Typesetting definitions
The following command is provided to typeset definitions:
\smallskip
\item{1.}€\gfdefinition p {}=€ outputs the formula
€\frege{}€ in parentheses and sets it equal to the new symbol
{\tt} if the parameter {\tt} is either {\tt|} to type a judgment
or {\tt.}\ for a definition. In the style of the {\it Grundgesetze\/}
the parameter {\tt} can also be {\tt:}. In this case write €€
and this is interpreted as a math formula and not as a formula created
by €\frege€. The parameter {\tt} is the position parameter to move
the output the given amount of units to the right.
\noindent
The output of a definition depends on the style.
\Example{11}
The definition in formula~69 of the {\it Begriffsschrift\/} is:
\smallskip
\def\1#1{{\gfvererbe\kd\ka{#1(\ka)}{f(\kd,\ka)}}}
\gfdefinition p4. .{*.d.{..{*.a.{..{F(\da)}.{{f(\dd,\da)}}}}.{F(\dd)}}}={\1F}
\smallskip
In the style of the {\it Grundgesetze\/} the output is:
\smallskip
\toggleGGstyle
\def\1#1{{\gfvererbe\kd\ka{#1(\ka)}{f(\kd,\ka)}}}
\gfdefinition p4. .{*.d.{..{*.a.{..{F(\da)}
.{{f(\dd,\da)}}}}
.{F(\dd)}}}={\1F}
\toggleGGstyle
\smallskip
And here is the source (note that €\1€ is a normal macro and needs no
macro expansion):
\verbatim
\def\1#1{{\gfvererbe\kd\ka{#1(\ka)}{f(\kd,\ka)}}}
\gfdefinition p4. .{*.d.{..{*.a.{..{F(\da)}
.{{f(\dd,\da)}}}}
.{F(\dd)}}}={\1F}
\endverbatim\Eend1
\Example{12}
Here is an example of the {\it Grundgesetze}, in which the {\tt} is
a colon.
\smallskip
\advance\rightskip by 2\rightskip
\toggleGGstyle
\gfdefinition p4: \kesl(o\G^(a\G^\ke))={o\G;a}
\named "$\gX$"
\toggleGGstyle
\smallskip
\rightskip=\leftskip
And this is the source:
\verbatim
\gfdefinition p4: \kesl(o\G^(a\G^\ke))={o\G;a}
\named "$\gX$"
\endverbatim\Eend1
% %%%%%%%%%%%
\beginsection 15. Commands to improve page breaks
The formulas are never broken. A page or column break must appear
at a decollator, separator, or after an inference rule. To gain some
space the formulas can be typeset in a smaller height and depth.
(€\offinterlineskip€ should be set.)
\smallskip
\item{1.}€\gfbssetzeabstand€ sets the height and depth between the lines to
{\tt}\thinspace pt and {\tt}\thinspace pt, resp.;
\item{2.}€\gfbsreduziereabstandum€ reduces the height and depth each by {\tt}\%
({\tt} is a two-digit number);
\item{3.}€\gfbsabstandzuruecksetzen€ sets height and depth to the values of €\strutbox€.
\Example{13}
The right formula uses €\gfbsreduziereabstandum20€:
\smallskip
\begingroup
\offinterlineskip
\setbox0=\hbox to .3\hsize{\vtop to 30pt{%
\nlp4\*_[-\*-:-\*---\ce{$a$}
\nlp4\*___\*_'-\*-:-\ce{$c$}
\nlp4\*___\*___\*_'-\ce{$e$}\vss}\hss}
\setbox1=\hbox to .3\hsize{\vtop to 30pt{%
\nlp1\*_[-\*-:-\*---\ce{$a$}
\gfbsreduziereabstandum20
\nlp1\*___\*_'-\*-:-\ce{$c$}
\nlp1\*___\*___\*_'-\ce{$e$}\vss}\hss}
\centerline{\box0 \box1 }
\gfbsabstandzuruecksetzen
\endgroup
And this is the code:
\verbatim
\offinterlineskip
\setbox0=\hbox to .3\hsize{\vtop to 30pt{%
\nlp4\*_[-\*-:-\*---\ce{$a$}
\nlp4\*___\*_'-\*-:-\ce{$c$}
\nlp4\*___\*___\*_'-\ce{$e$}\vss}\hss}
\setbox1=\hbox to .3\hsize{\vtop to 30pt{%
\nlp1\*_[-\*-:-\*---\ce{$a$}
\gfbsreduziereabstandum20
\nlp1\*___\*_'-\*-:-\ce{$c$}
\nlp1\*___\*___\*_'-\ce{$e$}\vss}\hss}
\centerline{\box0 \box1 }
\gfbsabstandzuruecksetzen
\endverbatim\Eend1
% %%%%%%%%%%%
\beginsection 16. List of parameters
Nearly all aspects of the lines that build the structure of Frege's
notation is controlled by parameters. They can be changed to fit
better with a certain type of font. But note that a couple of tests
have been made with these values to guarantee, for example, that the
affirmation can be placed in front of a quantification.\\
\noindent
Here is the list of registers that make up the style of the
{\it Begriffsschrift}.
\item{1.}$€\gfbsvolleeinheit€=\rm0.57\,em$; width of one €\*€ triple
\item{2.}$€\gfbsraise€=\rm0.5\,ex$; height of the horizontal line
\item{3.}$€\gfbsneg€=\rm0.25\,ex$; height of the negation indicator
\item{4.}$€\gfbsstrichdicke€=\rm0.5\,pt$; thickness of the horizontal line
\item{5.}$€\gfbsurteildicke€=\rm1\,pt$; thickness of the judgment stroke\\
\item{6.}$€\gfbsuht€=\rm1.5\,ex$; height of the judgment stroke\\
\item{7.}$€\gfbsudp€=\rm0.5\,ex$; depth of the judgment stroke\\
\item{8.}$€\gfbsersetzungdicke€=\rm0.8\,pt$; thickness of the substitution line\\
\item{9.}$€\gfbsdefdicke€=\rm0.75\,pt$; thickness of the definition strokes
\item{10.}$€\gfbsschlussabstand€=\rm2.5\,pt$; distance of double lines in an inference
\item{11.}$€\gfbsschlussdicke€=\rm0.8\,pt$; thickness of the second line in an inference
\item{12.}$€\gfbsdpabstand€=\rm0.2\,em$; distance between colons in front of an inference
\smallskip
\item{13.}$€\gfbsmaxanzahlzeilen€=25$; the maximal amount of lines
in a single formula of the short form (the package declares for each
line one or two token and skip registers; two registers of each kind
are needed if substitutions are allowed);
\item{14.}$€\gfbsnegpct€=70$; when €\ifgfbsnegdirect€ is set to false the negation
indicator has only a height of this percentage so that a gap occurs.
\smallskip
\noindent
And this is the list of additional dimen parameters for the style of
the {\it Grundgesetze}.
\item{15.}$€\gfggstrichdicke€=\rm0.58\,pt$; common line thickness
\item{16.}$€\gfggraise€=\rm0.14\,ex$; height of horizontal line
\item{17.}$€\gfggneg€=\rm0.47\,ex$; height of negation indicator
\item{18.}$€\gfgguht€=\rm1.4\,ex$; height of the judgment stroke
\item{19.}$€\gfggudp€=\rm0.9\,ex$; depth of the judgment stroke
\item{20.}$€\gfggdpabstand€=\rm0.06\,em$; distance between colons in front of an inference
% %%%%%%%%%%%
\beginsection 17. Related work
Other people have worked on the problem to typeset Frege's notation
in \TeX\ too. J.~Parsons has developed a package {\it begriff.sty\/}
for \LaTeX\ (see [7]). Later the package was improved by
Q.~Pamp~([8]). A team that translated the {\it Grundgesetze\/} created
its own package from {\it begriff.sty\/} and called it {\it
grundgesetze.sty\/} (see [9]). It uses the fonts [5] that J.~J.~Green
has developed for the special terminal symbols in the {\it
Grundgesetze}.
% %%%%%%%%%%%
\beginsection 18. References
\raggedright\frenchspacing
\item{[1]}Gottlob Frege,
{\sl Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache
des reinen\hfil\break Denkens\/}
(Halle an der Saale: Louis Nebert, 1879)
\item{}``Begriffsschrift, a formula language, modeled upon that of arthmetic, for
pure thought,'' in: Jean van Heijenoort (ed.),
{\sl From Frege to G\"odel: A Sourcebook in Mathematical Logic,
1879--1931\/},\hfil\break(Cambridge, MA: Harvard University Press, 1967), 1--82;
translation by S. Bauer-Mengelberg
\item{[2]}Gottlob Frege,
{\sl Grundgesetze der Arithmetik --- begriffsschriftlich abgeleitet\/}
(Jena: Hermann Pohle, Volume 1 1893, Volume 2 1903)
\item{}{\sl Basic Laws of Arithmetic\/} (Oxford: Oxford Univ. Press, 2013);
translation by Philip A. Ebert, Marcus Rossberg, Crispin Wright
\item{[3]}American Mathematical Society, {\tt amstex},
€http://www.ams.org/publications/authors/tex/tex€ or
€http://www.ctan.org/tex-archive/macros/amstex€
(accessed: 2014-11-29)
\item{[4]}{\tt rotate},
€http://www.ctan.org/tex-archive/macros/plain/contrib/misc€
(accessed: 2014-11-29)
\item{[5]}J. J. Green, {\tt fge},
€http://www.ctan.org/tex-archive/fonts/fge€
(accessed: 2014-11-29)
\item{[6]}Silvio Levy, ``Using Greek fonts with \TeX,''
TUGboat {\bf 9,1} (1988), 20--24
\item{[7]}Josh Parsons, {\tt begriff.sty},
€http://www.ctan.org/tex-archive/macros/latex/contrib/begriff€
(accessed: 2014-11-29)
\item{[8]}Quirin Pamp, {\tt frege.sty},
€http://www.ctan.org/tex-archive/macros/latex/contrib/frege€
(accessed: 2014-11-29)
\item{[9]}Marcus Rossberg, {\tt grundgesetze.sty},
€http://www.ctan.org/tex-archive/macros/latex/contrib/€\hfil\break€grundgesetze€
(accessed: 2014-11-29)
\bye
% Local Variables:
% coding: iso-latin-9-unix
% End: