path: root/macros/latex/contrib/grundgesetze/grundgesetze.dtx

% \iffalse meta-comment
%
% grundgesetze: LaTeX2e package for typesetting begriffsschrift
% in the of Gottlob Frege's _Grundgesetze der Arithmetik_ (Jena 1893/1903)
%
% Copyright (C) 2003-2021 by Josh Parsons <josh.parsons@ccc.ox.ac.uk>,
% Marcus Rossberg <marcus.rossberg@uconn.edu>,
% J.J. Green <j.j.green@gmx.co.uk>,
% Richard Kimberly Heck <richard_heck@brown.edu>,
% and Agust’n Rayo <arayo@mit.edu>
%
% This package is based on begriff.sty, originally written by 
% Josh Parsons in 2003, 2005.
%
% New in this update (Marcus Rossberg, 2021-04-26):   
% \baselineskip in \GGconditional replaced by \normalbaselineskip
% to allow use in tabular and array environments
% 
% This program is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2 of the License, or
% (at your option) any later version.
% 
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
% General Public License for more details.
% 
% You should have received a copy of the GNU General Public License
% along with this program; if not, write to the Free Software
% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111,
% USA.
%
% \fi
%
% \CheckSum{569}
%% \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         \~}
%
% \iffalse   % this is a METACOMMENT !
%
%<package>\NeedsTeXFormat{LaTeX2e}
%<package>\ProvidesPackage{grundgesetze}
%<package>[2021/04/26 v1.03 grundgesetze package]
%
%<*driver>
\documentclass[a4paper,10pt]{ltxdoc}
\OnlyDescription  % <- comment out to include style code listing at the end of the document
\usepackage[bguq=5]{grundgesetze}
% \usepackage{grundgesetze}
\usepackage{begriff}
\usepackage{fge}
\usepackage{hyperref}
\usepackage{amsfonts}
\usepackage{amstext}
\usepackage{amsmath}
\usepackage{booktabs}
\usepackage{placeins}
\providecommand\dst{\expandafter{\normalfont\scshape docstrip}}
\renewcommand{\quad}{{\hskip1em plus 2em}}
\begin{document}
 \DocInput{grundgesetze.dtx}
\end{document}
%</driver>
% \fi
%
% \GetFileInfo{grundgesetze.sty}
% \title{\emph{Grundgesetze.sty} for \LaTeX2e\ Documentation}
% \author{Marcus Rossberg \\
% University of Connecticut \\
% \texttt{marcus.rossberg@uconn.edu}}
% \date{Version \fileversion{} \filedate}
% \maketitle
% \setcounter{StandardModuleDepth}{1}
%
% \noindent
% \emph{grundgesetze.sty} is a \LaTeX2e\ package for typesetting 
% formulae in Gottlob Frege's \emph{begriffsschrift} [concept-script]  
% in the style of his \emph{Grundgesetze der Arithmetik} 
% (Jena 1893/1903). The package was developed for the 2013 English  
% edition.\footnote{Gottlob Frege: \emph{Basic Laws of Arithmetic}. 
% Translated and edited by Philip A.\ Ebert and Marcus Rossberg. Oxford 2013.}
% The package is based on Josh Parsons's \emph{begriff.sty} which renders 
% the formalism in the style of Frege's earlier work, 
% \emph{Begriffsschrift} (Halle a.S.\ 1879). It was amended by Richard Kimberly Heck, 
% J.J.\ Green, Agust\'in Rayo, and Marcus Rossberg. Thanks to 
% Philip Ebert and Sanford Shieh for testing and suggestions.  Frege's 
% defined function symbols are not rendered by this package, but 
% by J.J.\ Green's \emph{fge.sty}.
%
% \section{Options}
%
% At present the only package option is |bguq|, which causes the package
% to use the |bguq| font for an alternative universal quantifier (concavity),
% and this option accepts a value (corresponding to the size to be used,
% as in |bguq=6|; default is 5).  The |bguq| font is required for this
% option. It is included in recent versions of the big \TeX\ distributions.
%
% \section{Basic Commands}
% 
% \DescribeMacro{\GGhorizontal}
%   \indent The horizontal, $\GGhorizontal$
%
% \DescribeMacro{\GGnot}
%   The negation-stroke, $\GGnot$
%
% \DescribeMacro{\GGconditional}  
%   Conditional-stroke: called as |\GGconditional{p}{q}| yields
%   $\GGconditional{p}{q}$ 
%
% \DescribeMacro{\GGquant} 
%   Concavity: called as |\GGquant{\mathfrak a}| gives 
%   $\GGquant{\mathfrak a}$ 
%
% \DescribeMacro{\GGjudge}
%   Judgement-stroke, $\GGjudge$
%
% \DescribeMacro{\GGdef}
%   Definition-stroke, $\GGdef$
%
% \DescribeMacro{\GGbracket}
%   Automatically scaling brackets, |\GGbracket{\ldots}| yields 
%  $\GGbracket{\ldots}$ (see examples below)
%
% \DescribeMacro{\GGsqbracket}
%   Analogous square brackets, $\GGsqbracket{\ldots}$
%
% A complete list of commands and synonymns in 
% the package can be found in Table~\ref{table:allmacros}, and
% the lengths parameterising the appearance of the output in 
% Table~\ref{table:lengths}.
% 
% \subsection{Examples}
%
% \begin{itemize}
%
% \item
%\begin{verbatim}
%\GGjudge \GGquant{\mathfrak a} \mathfrak a = \mathfrak a
%\end{verbatim}
%   yields
%   \begin{equation*}
%     \GGjudge \GGquant{\mathfrak a} \mathfrak a = \mathfrak a
%   \end{equation*}
%
%
% \item
%\begin{verbatim}
%\GGjudge \GGnot \GGquant{\mathfrak F} \GGnot 
%    \GGquant{\mathfrak a} \mathfrak{Fa}
%\end{verbatim}
%   yields
%   \begin{equation*}
%     \GGjudge \GGnot \GGquant{\mathfrak F} \GGnot 
%        \GGquant{\mathfrak a} \mathfrak{Fa}
%   \end{equation*}
%
% \item
%\begin{verbatim}
%\GGjudge \GGconditional{(\GGhorizontal p)}{p}
%\end{verbatim}
%   yields
%   \begin{equation*}
%     \GGjudge \GGconditional{(\GGhorizontal p)}{p}
%   \end{equation*}
%
% \item
%\begin{verbatim}
%\GGjudge \GGbracket{\GGconditional{p}{q}} =
%    \GGbracket{\GGconditional{\GGnot q}{\GGnot p}}
%\end{verbatim}
%   yields
%   \begin{equation*}
%     \GGjudge \GGbracket{\GGconditional{p}{q}} =
%       \GGbracket{\GGconditional{\GGnot q}{\GGnot p}}
%   \end{equation*}
%
% \end{itemize}
%
% There are further examples, including Frege's six basic laws of logic, 
% available for download on \url{http://www.frege.info/}.
%
%
% \section{Advanced Typesetting}
% 
% \subsection{Left-alignment of terminal forumlae: 
% \texttt{\textbackslash GGterm}\label{term}}
% 
% Conditional-strokes, negation-strokes, and concavities that are 
% embedded in conditionals can result in a ragged appearance of the 
% formula:
% 
% \begin{itemize}
%
% \item
%\begin{verbatim}
%\GGjudge\GGconditional{p}{\GGconditional{q}{p}}
%\end{verbatim}
% yields:
% \begin{equation*}
%   \GGjudge\GGconditional{p}{\GGconditional{q}{p}}
% \end{equation*}
% 
% \item
%\begin{verbatim}
%\GGjudge\GGconditional{Fa}
%    {\GGnot \GGquant{\mathfrak a} \GGnot F \mathfrak a}
%\end{verbatim}
% yields: 
% \begin{equation*}
%   \GGjudge\GGconditional{Fa}
%     {\GGnot \GGquant{\mathfrak a} \GGnot F \mathfrak a}
% \end{equation*}
%
%% \end{itemize}
% 
% In Frege's original work, the component formulae of conditionals
% are left-aligned. This can be achieved by marking ``terminal formulae'' 
% using the command |\GGterm{|$\langle\text{math}\rangle$|}|; the length 
% |\GGlinewidth| specifies the distance of the terminal formula from 
% the left end of the whole formula (typically, `\,$\GGjudge\!$'):
%
% \begin{itemize}
%
% \item
%\begin{verbatim}
%\setlength{\GGlinewidth}{9.2pt} \GGjudge
%\GGconditional
%     {\GGterm{p}}
%     {\GGconditional{\GGterm{q}}
%                    {\GGterm{p}}}
%\end{verbatim}
% yields: 
% \begin{equation*}
%   \setlength{\GGlinewidth}{9.2pt}
%   \GGjudge\GGconditional{\GGterm{p}}{\GGconditional{\GGterm{q}}{\GGterm{p}}}
% \end{equation*}
%
% \item
%\begin{verbatim}
%\setlength{\GGlinewidth}{25.2pt}
%\GGjudge\GGconditional{\GGterm{Fa}}
%                      {\GGnot \GGquant{\mathfrak a} \GGnot 
%                       \GGterm{F \mathfrak a}}
%\end{verbatim}
% yields:
% \begin{equation*}
%   \setlength{\GGlinewidth}{25.2pt}
%   \GGjudge\GGconditional{\GGterm{Fa}}
%                         {\GGnot \GGquant{\mathfrak a} \GGnot 
%                          F \mathfrak a}
% \end{equation*}
%
% \end{itemize}
%
% \begin{table}[ph]
% \begin{center}
% \begin{tabular}{lp{7mm}l}
%   \toprule 
%   negation-stroke          & \GGnot               & 4.4pt\\
%   conditional-stroke       & $\GGconditional{}{}$ & 4.4pt \\
%   concavity                & $\GGquant{}$         & 11.6pt \\
%   judgement-stroke:        & \GGjudge             & \\
%   \hspace{10pt}present     &                      & add .4pt\\
%   \hspace{10pt}not present &                      & subtract 2pt\\ 
%   \bottomrule
% \end{tabular}
% \end{center}
% \caption{Lengths of embedded symbols\label{table:embedded}}
% \end{table}
%
% The correct values for |\GGlinewidth| for each formula can be 
% determined by adding up the lengths 
% of the embedded symbols, as given in Table~\ref{table:embedded},
% or by using a GUI that allows producing \LaTeX\ and XML code for 
% \emph{begriffsschrift} formulae by mouse-click. The GUI will 
% calculate and output the correct values. It is available for 
% download on \url{http://www.frege.info/}.
%
% \subsection{Adding horizontal lengths manually: 
% \texttt{\textbackslash GGnonot}, etc.}
%
% Readability is sometimes aided by moving, e.g., negations to the 
% right end of the horizontal in a complex formula. For instance, 
% Frege nearly always prefers the rendering displayed on the right  
% in these types of formulae:
% 
% \begin{center}
% \begin{tabular}{rp{20mm}p{20mm}}
% (a) & 
% \GGjudge\GGconditional{\GGquant{\mathfrak a}
% \GGnot f(\mathfrak a)}{\GGnot\GGnoquant f(a)} &  
% \GGjudge\GGconditional{\GGquant{\mathfrak a}
% \GGnot f(\mathfrak a)}{\GGnoquant\GGnot f(a)}\\ \addlinespace[10pt]
%
% (b) & 
% \GGjudge\GGconditional{\GGquant{\mathfrak a}
% \GGconditional{f(\mathfrak a)}{g(\mathfrak a)}}
% {\GGconditional{\GGnoquant f(a)}{\GGnoquant g(a)}} &
% \GGjudge\GGconditional{\GGquant{\mathfrak a}
% \GGconditional{f(\mathfrak a)}{g(\mathfrak a)}}
% {\GGnoquant\GGconditional{f(a)}{g(a)}}\\ \addlinespace[10pt]
%
% (c) & 
% \GGjudge\GGconditional{\GGnot\GGnonot f(a)}
% {\GGconditional{\GGnonot f(b)}{\GGnot a=b}} & 
% \GGjudge\GGconditional{\GGnonot\GGnot f(a)}
% {\GGconditional{\GGnonot f(b)}{\GGnot a=b}}
% \end{tabular}
% \end{center}
%
% The right-hand formulae are produced by inserting commands 
% for horizontals of the appropriate length directly at the 
% position where the ``space'' should appear. The three  
% right-hand formulae above are created thus, respectively:
% \begin{itemize}
% \item[(a)] \begin{verbatim}\GGjudge \GGconditional
%       {\GGquant{\mathfrak a} \GGnot f(\mathfrak a)}
%       {\GGnoquant \GGnot f(a)}\end{verbatim}
% \item[(b)] \begin{verbatim}\GGjudge \GGconditional
%       {\GGquant{\mathfrak a}
%             \GGconditional{f(\mathfrak a)}{g(\mathfrak a)}}
%       {\GGnoquant \GGconditional{f(a)}{g(a)}}\end{verbatim}
% \item[(c)] \begin{verbatim}\GGjudge \GGconditional
%       {\GGnonot \GGnot f(a)}
%       {\GGconditional{\GGnonot f(b)}{\GGnot a=b}}\end{verbatim}
% \end{itemize}
%
% \section{Comparison and compatibility with \emph{begriff.sty}}
% 
% Josh Parsons's \emph{begriff.sty}, on which \emph{grundgesetze.sty} 
% is based, is closer in appearance to Frege's formalism as it is 
% presented in Frege's first book, \emph{Begriffs\-schrift} (Halle a.S.\ 1879). 
% The corresponing commands were given different names so that both 
% pack\-ages can be used in the same \TeX~document; see Table~\ref{table:compat}.
%
% \begin{table}[hp]
% \begin{tabular}{lp{16mm}p{13mm}l}
% \toprule
%   \multicolumn{2}{l}{\emph{begriff.sty}} &
%   \multicolumn{2}{l}{\emph{grundgesetze.sty}} \\
%   command & symbol & symbol & command \\
% \midrule
%   |\BGcontent| & \BGcontent & 
%      \GGhorizontal & |\GGhorizontal| \\
%   |\BGnot| & \BGnot & 
%      \GGnot & |\GGnot| \\
%   |\BGconditional{p}{q}| & $\BGconditional{p}{q}$ &
%      $\GGconditional{p}{q}$ & |\GGconditional{p}{q}| \\
%   |\BGquant{\mathfrak a}| & $\BGquant{\mathfrak a}$ &
%     $\GGquant{\mathfrak a}$ & |\GGquant{\mathfrak a}| \\
%   |\BGassert| & \BGassert &
%     \GGjudge & |\GGjudge| \\
%   |\BGbracket{\ldots}| & $\BGbracket{\BGconditional{p}{q}}$ & 
%     $\GGbracket{\GGconditional{p}{q}}$ & |\GGbracket{\ldots}| \\
% \bottomrule
% \end{tabular}
% \caption{Compatibility with \emph{begriff.sty}\label{table:compat}}
% \end{table} 
%
% \noindent Also note the differences in alignment between 
% |\BGbracket| and |\GGbracket| as shown in Table~\ref{table:align}
%
% \begin{table}[hp]
% \begin{tabular}{ll}
% |\BGbracket| &
% $
% \setlength{\BGlinewidth}{28.4pt}
% \BGassert (\spirituslenis{\varepsilon}f(\varepsilon) = 
% \spirituslenis{\alpha}g(\alpha)) =
% \BGquant{\mathfrak{a}}
% \BGbracket{\BGconditional{
%   \BGnot\BGconditional{
%     \BGnot\mathfrak{a}=\spirituslenis{\alpha}g(\alpha)
%   }{
%    \BGterm{\mathfrak{a}=\spirituslenis{\varepsilon}f(\varepsilon)}
%   }
% }
% {\BGterm{f(\mathfrak{a}) = g(\mathfrak{a})}}}
% $ \\
% ~\\
% |\GGbracket|: \hspace{5mm} &
% $
% \GGjudge(\spirituslenis{\varepsilon}f(\varepsilon) = 
% \spirituslenis{\alpha}g(\alpha)) =
% \GGquant{\mathfrak{a}}
% \GGbracket{\GGconditional{
%   \GGnot\GGconditional{
%     \GGnot\mathfrak{a}=\spirituslenis{\alpha}g(\alpha)
%   }{
%    \GGnonot \mathfrak{a}=\spirituslenis{\varepsilon}f(\varepsilon)
%   }
% }
% {\GGnonot\GGnonot\GGnonot f(\mathfrak{a}) = g(\mathfrak{a})}}
% $
% \end{tabular}
% \caption{\texttt{\textbackslash BGbracket} and 
%          \texttt{\textbackslash GGbracket} alignment
%          \label{table:align}}          
% \end{table}
%
% \subsection{Conversion of a \emph{begriff.sty} document into a 
%             \emph{grundgesetze.sty} document}
%
% A straightforward way to convert the a \LaTeX\ document that uses 
% \emph{begriff.sty} into one that uses \emph{grundgesetze.sty} without 
% manually exchanging the commands is to find and replace  
% ``|\BG|" by ``|\GG|". Synonyms have been added to 
% \emph{grundgesetze.sty} to allow the use of all \emph{begriff.sty} 
% commands ``translated" in this way (see Table~\ref{table:allmacros}).
%
% \begin{table}[hp]
% \begin{tabular}{p{39mm}p{12mm}p{58mm}}
% \toprule
% command & symbol & synonym / comment\\
% \midrule
% |\GGterm{\ldots}| &               & (marks terminal formula)\\
% |\GGhorizontal|   & \GGhorizontal & |\GGcontent|\\
% |\GGjudge|        & \GGjudge      & |\GGassert|\\
% |\GGjudgelong|    & \GGjudgealone & 
%    |\GGjudgealone|, |\GGassertlong|, |\GGassertalone|\\
% |\GGjudgevar{|$\langle\text{\emph{length}}\rangle$|}| &
%    \GGjudgevar{6pt} & 
%    |\GGassertvar{|$\langle\text{\emph{length}}\rangle$|}|
%    (variable horizontal length, here: 6pt)\\
% |\GGdef| & $\GGdef$\\
% |\GGdeflong| & \GGdefalone & |\GGdefalone|\\
% |\GGdefvar{|$\langle\text{\emph{length}}\rangle$|}| &
%    \GGdefvar{6pt} & (variable horizontal length, here: 6pt)\\
% |\GGnot| & \GGnot & |\GGneg| \\
% |\GGnotalone| & \GGnotalone & (standalone negation-stroke)\\
% |\GGdnot| & \GGdnot & (standalone double negation-stroke)\\
% |\GGconditional{p}{q}| & $\GGconditional{p}{q}$ \\
% |\GGquant{\mathfrak a}| & $\GGquant{\mathfrak a}$\\
% |\GGall{a}| & $\GGall{a}$ & |\GGquant{\mathfrak a}|\\
% |\GGbracket{\ldots}| & \GGbracket{\ldots} & 
%   (automatically scaling brackets)\\
% |\GGsqbracket{\ldots}| & \GGsqbracket{\ldots} & (ditto square brackets)\\
% |\GGnonot| & \GGnonot & horizontal of |\GGnot| length\\
% |\GGnoquant| & \GGnoquant & horizontal of |\GGquant| length\\
% |\GGnoboth| & \GGnoboth & 
%   horizontal of length: |\GGnot| plus |\GGquant| \\
% |\GGnonotalone| & \GGnonotalone & 
%   horizontal of |\GGnotalone| length \\
% |\GGnodnot| & \GGnodnot & 
%   horizontal of |\GGdnot| length\\
% |\GGoddspace| & \GGoddspace & 
%   horizontal of length: |\GGquant| minus |\GGnot|\\
% |\GGtinyspace| & \GGtinyspace & 
%   horizontal of length: |\GGquant| minus twice |\GGnot|)\\
% |\GGtiniestspace| & \GGtiniestspace & 
%   horizontal of length: thrice |\GGnot| minus |\GGquant|\\
% \bottomrule
% \end{tabular}
% \caption{All commands (and synonyms) defined by the 
%          package\label{table:allmacros}}
% \end{table}
%
% \begin{table}[hp]
% \begin{tabular}{lp{22mm}p{56mm}}
% \toprule
% length & default value & explanation \\
% \midrule
% |\GGthickness| & 0.4pt & thickness of horizontal and vertical lines\\
% |\GGquantthickness| & {$0.75 \times$ |\GGthickness|} & 
%   thickness of the line of the quantifier ``dish''.  Note that
%   this value is unused if the |bguq| option has been selected\\
% |\beforelen| & 2.4pt & 
%   length of horizontal before quantifier, conditional, and negation\\
% |\GGafterlen| & 2pt & 
%   length of horizontal after quantifier, conditional, negation, 
%   judgement-, and definition-stroke\\
% |\GGspace| & 3pt & 
%   space between right end of horizontal and terminal formula\\
% |\GGlift| & 2pt & 
%   lift of horizontal from baseline\\
% |\GGlinewidth| & (n/a) & 
%   total length from left end of formula (typically, 
%   `|\GGjudge|') and the beginning of the terminal formula 
%   (see \S\ref{term})\\
% \bottomrule
% \end{tabular}
% \caption{Length parameters and their default values\label{table:lengths}}
% \end{table}
%
% \FloatBarrier
% \StopEventually{}
% 
% \section{The \dst{} modules}
% 
% The following modules are used in the implementation to direct
% \dst{} in generating the external files:
% \begin{center}
%   \begin{tabular}{ll}
%     driver  & produce a documentation driver file \\
%     package & produce a package file \\
%   \end{tabular}
% \end{center}
% 
% \section{The Implementation}
% 
% \subsection{Lengths and thicknesses}
%
%    \begin{macro}{\GGthickness}
% Thickness of lines
%    \begin{macrocode} 
\newlength{\GGthickness}
\setlength{\GGthickness}{0.4pt}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGquantthickness}
% Thickness of lines for quantifier-curvature
%    \begin{macrocode} 
\newlength{\GGquantthickness}
\setlength{\GGquantthickness}{0.75\GGthickness}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGafterlen}
% Additional length after a quantifier, conditional, negation, or 
% assertion
%    \begin{macrocode} 
\newlength{\GGafterlen}
\setlength{\GGafterlen}{2pt}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGbeforelen}
% Additional length before a quantifier, conditional, or negation
%    \begin{macrocode} 
\newlength{\GGbeforelen}
\setlength{\GGbeforelen}{2.4pt}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGspace}
% Space inserted before a formula
%    \begin{macrocode} 
\newlength{\GGspace}
\setlength{\GGspace}{3pt}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGlift}
% Lift from baseline
%    \begin{macrocode} 
\newlength{\GGlift}
\setlength{\GGlift}{2pt}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGlinewidth}
% Total width of diagram
%    \begin{macrocode} 
\newlength{\GGlinewidth}
\setlength{\GGlinewidth}{\linewidth}
%    \end{macrocode}
%    \end{macro} 
%
% \subsection{Options}
%
%    \begin{macro}{bguq}
% The |bguq| option causes the package to use the |bguq| font,
% providing an alternative universal quantification stroke. Of 
% course, one must have the |bguq| font installed, but it is 
% included in recent versions of the big \TeX\ distributions.
%    \begin{macrocode} 
\RequirePackage{kvoptions}
\SetupKeyvalOptions{family=grundgesetze,prefix=grundgesetze@}
\DeclareStringOption{bguq}[5]
%    \end{macrocode}
%    \end{macro}
% Process the key-value options
%    \begin{macrocode} 
\ProcessKeyvalOptions{grundgesetze}
%    \end{macrocode}
% If the |bguq| option has been chosen the require the |bguq| package
% and pass the option value (the size) as the package option
%    \begin{macrocode} 
\ifx\grundgesetze@bguq\@empty
\else
  \RequirePackage[\grundgesetze@bguq]{bguq}
\fi
%    \end{macrocode}
%
% \subsection{The main part of the code}
%    \begin{macrocode} 
\typeout{Grundgesetze Begriffsschrift: April 2021}
\ifx\grundgesetze@bguq\@empty
  \typeout{Universal quantifier by qbezier}
\else
  \typeout{Universal quantifier by bguq at size \grundgesetze@bguq}
\fi
%    \end{macrocode}
%    \begin{macro}{\GGbracket}
% Variable-sized parenthesis
%    \begin{macrocode}
\newcommand{\GGbracket}[1]{% 
\setbox0=\hbox{\ensuremath{#1}}%
\dimen0=0.5\dp0%
\addtolength{\dimen0}{-1\GGlift}%
\raisebox{-\dimen0}{%
\ensuremath{\left(\raisebox{\dimen0}{\box0}\right)}}%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGsqbracket}
% Variable-sized square parenthesis
%    \begin{macrocode} 
\newcommand{\GGsqbracket}[1]{%
\setbox0=\hbox{\ensuremath{#1}}%
\dimen0=0.5\dp0%
\addtolength{\dimen0}{-1\GGlift}%
\raisebox{-\dimen0}{%
\ensuremath{\left[\raisebox{\dimen0}{\box0}\right]}}%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGterm}
% Generate a terminal node with fill-line to the left
%    \begin{macrocode} 
\newcommand{\GGterm}[1]{\unskip%
\setbox0=\hbox{%
\setlength{\GGlinewidth}{0pt}%
\raisebox{\GGlift}{%
\vrule height \GGthickness width \GGafterlen depth 0pt
}%
\ensuremath{\hskip\GGspace #1}%
}%
\raisebox{\GGlift}{%
\vrule height \GGthickness width \GGlinewidth depth 0pt
}%
\box0%
\setlength{\GGlinewidth}{0pt}%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGconditional}
% Generate a conditional |\GGconditional{antecedent}{consequent}|
%    \begin{macrocode} 
\newcommand{\GGconditional}[2]{\unskip%
\addtolength{\GGlinewidth}{-\GGbeforelen}%
\setbox0=\hbox{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\raisebox{\GGlift}{%
\vrule height 0.49\normalbaselineskip depth 0.425\normalbaselineskip width 0pt
\vrule height \GGthickness width \GGafterlen depth 0pt
}%
\ensuremath{\hskip\GGspace #1}%
}%
\setbox1=\hbox{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
% strut -- depth of conditional here!
\raisebox{\GGlift}{%
\vrule height 0pt depth 0.425\normalbaselineskip width 0pt%
\vrule height \GGthickness width \GGafterlen depth 0pt}%
\ensuremath{\hskip\GGspace #2}%
}%
\dimen0=0pt%
\addtolength{\dimen0}{\dp1}%
\addtolength{\dimen0}{\ht0}%
\addtolength{\dimen0}{\lineskip}%
\hbox{%
\raisebox{\GGlift}{%
\vrule width \GGbeforelen height \GGthickness depth 0pt%
\kern-\GGthickness%
\vrule width \GGthickness height \GGthickness depth \dimen0
}%
\vtop{\box1\box0}%
}%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGjudge}
% Generate a judgement-stroke
%    \begin{macrocode} 
\newcommand{\GGjudge}[0]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\addtolength{\GGlinewidth}{-\GGthickness}%
\raisebox{\GGlift}{%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height \GGthickness width \GGafterlen}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGassert}
% Synonym 
%    \begin{macrocode} 
\newcommand{\GGassert}{\GGjudge}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGjudgealone}
% Generate stand-alone judgement-stroke
%    \begin{macrocode} 
\newcommand{\GGjudgealone}[0]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\addtolength{\GGlinewidth}{-\GGthickness}%
\raisebox{\GGlift}{%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height \GGthickness width 12pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
% Synonyms 
%    \begin{macro}{\GGassertalone}
%    \begin{macrocode} 
\newcommand{\GGassertalone}{\GGjudgealone}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGjudgelong}
%    \begin{macrocode} 
\newcommand{\GGjudgelong}{\GGjudgealone}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGassertlong}
%    \begin{macrocode} 
\newcommand{\GGassertlong}{\GGjudgealone}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGjudgevar}
% Generate a judgement-stroke of variable length
%    \begin{macrocode} 
\newcommand{\GGjudgevar}[1]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\addtolength{\GGlinewidth}{-\GGthickness}%
\raisebox{\GGlift}{%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height \GGthickness width #1}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGassertvar}
% Synonym 
%    \begin{macrocode} 
\newcommand{\GGassertvar}[1]{\GGjudgevar{#1}}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGdef}
% Generate a definition stroke
%    \begin{macrocode} 
\newcommand{\GGdef}[0]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\addtolength{\GGlinewidth}{-\GGthickness}%
\raisebox{\GGlift}{%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height 0pt width \GGafterlen%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height \GGthickness width \GGafterlen}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGdefalone}
% Generate a stand-alone definition stroke
%    \begin{macrocode} 
\newcommand{\GGdefalone}[0]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\addtolength{\GGlinewidth}{-\GGthickness}%
\raisebox{\GGlift}{%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height 0pt width \GGafterlen%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height \GGthickness width 12pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGdeflong}
% Synonym
%    \begin{macrocode} 
\newcommand{\GGdeflong}{\GGdefalone}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGdefvar}
% Generate a definition stroke of variable length
%    \begin{macrocode} 
\newcommand{\GGdefvar}[1]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\addtolength{\GGlinewidth}{-\GGthickness}%
\raisebox{\GGlift}{%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height 0pt width \GGafterlen%
\vrule width \GGthickness height 5pt depth 5pt%
\vrule depth 0pt height \GGthickness width #1}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGhorizontal}
% Generate a horizontal
%    \begin{macrocode} 
\newcommand{\GGhorizontal}[0]{%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\raisebox{\GGlift}{%
\vrule depth 0pt height \GGthickness width 12pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGcontent}
% Synonym 
%    \begin{macrocode} 
\newcommand{\GGcontent}{\GGhorizontal}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnot}
% Generate a negation stroke
%    \begin{macrocode} 
\newcommand{\GGnot}[0]{\unskip%
\addtolength{\GGlinewidth}{-\GGbeforelen}%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\raisebox{\GGlift}{%
\vrule width \GGbeforelen height \GGthickness depth 0pt%
\kern-\GGthickness%
\vrule width \GGthickness height \GGthickness depth 3pt%
\vrule depth 0pt height \GGthickness width \GGafterlen}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnonot}
% Generate a horizontal of negation-stroke length
% to format Frege's negation symbol right-aligned include |\GGnot| in 
% the scope of |\GGterm| --- to compensate alignment include |\GGnonot| 
% in that place in front of formulae that to not contain a negation 
% right before the content-formula
%    \begin{macrocode} 
\newcommand{\GGnonot}[0]{\unskip%
\addtolength{\GGlinewidth}{-\GGbeforelen}%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\raisebox{\GGlift}{%
\vrule width \GGafterlen height \GGthickness depth 0pt%
\vrule width \GGthickness height \GGthickness depth 0pt%
\vrule width \GGafterlen height \GGthickness depth 0pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnotalone}
% Generate a stand-alone negation stroke
%    \begin{macrocode} 
\newcommand{\GGnotalone}[0]{\unskip%
\raisebox{\GGlift}{%
\vrule width 4.2pt height \GGthickness depth 0pt%
\kern-\GGthickness%
\vrule width \GGthickness height \GGthickness depth 3pt%
\vrule depth 0pt height \GGthickness width 3.8pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnonotalone}
% Generate a horizontal of |\GGnotalone| length
%    \begin{macrocode} 
\newcommand{\GGnonotalone}[0]{\unskip%
\raisebox{\GGlift}{%
\vrule width 4.2pt height \GGthickness depth 0pt%
\kern-\GGthickness%
\vrule width \GGthickness height \GGthickness depth 0pt%
\vrule depth 0pt height \GGthickness width 3.8pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGdnot}
% Generate a double-negation for stand-alone use (cmp. Gg I, p. 69a)
%    \begin{macrocode} 
\newcommand{\GGdnot}[0]{\unskip%
\raisebox{\GGlift}{%
\vrule width 1.5\GGbeforelen height \GGthickness depth 0pt%
\kern-\GGthickness%
\vrule width \GGthickness height \GGthickness depth 3pt%
\vrule depth 0pt height \GGthickness width 1.5\GGafterlen%
\vrule width \GGthickness height \GGthickness depth 3pt%
\vrule depth 0pt height \GGthickness width 1.5\GGafterlen}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnodnot}
% Generate a a horizontal of |\GGdnot| length
%    \begin{macrocode} 
\newcommand{\GGnodnot}[0]{\unskip%
\raisebox{\GGlift}{%
\vrule width 1.5\GGbeforelen height \GGthickness depth 0pt%
\kern-\GGthickness%
\vrule width \GGthickness height \GGthickness depth 0pt%
\vrule depth 0pt height \GGthickness width 1.5\GGafterlen%
\vrule width \GGthickness height \GGthickness depth 0pt%
\vrule depth 0pt height \GGthickness width 1.5\GGafterlen}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGquant}
% Generate a concavity (universal quantifier).  The glyph consists
% of some line strokes and a concavity; if the |bguq| package option
% has been used then this is rendered using the |bguq| font; otherwise
% a Bezier curve is drawn with |\qbezier|.
%    \begin{macrocode} 
\newcommand{\GGquant}[1]{\unskip%
\addtolength{\GGlinewidth}{-\GGbeforelen}%
\addtolength{\GGlinewidth}{-7.2pt}%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\hbox{%
\raisebox{\GGlift}{%
\vrule width \GGbeforelen height \GGthickness depth 0pt%
\ifx\grundgesetze@bguq\@empty% use qbezier
  \setlength{\unitlength}{1pt}%
  \kern-\GGthickness%
  \begin{picture}(8,0)(0,0)%
  \linethickness{\GGquantthickness}%
  \qbezier[100](0.3,0.2)(1,-2)(4,-2)%
  \qbezier[100](4,-2)(7,-2)(7.7,0.2)%
  \end{picture}%
  \kern-8pt%
  \kern-\GGthickness
  \vbox{%
  \hbox to 8pt {\hskip1pt\hskip\GGthickness\hss$_{#1}$\hss}\vskip1pt
  }%
\else% use the bguq font
  \ensuremath\bguq
  \kern-\bguqwidth
  \vbox{%
    \hbox to \bguqwidth%
          {\hfill$\scriptstyle{#1}$\hfill}%
    \vskip1pt}%
\fi
\vrule width \GGafterlen height \GGthickness depth 0pt}%
}%
\hskip\GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnoquant}
% Generate a horizontal of concavity length
%    \begin{macrocode} 
\newcommand{\GGnoquant}[0]{\unskip%
\addtolength{\GGlinewidth}{-\GGbeforelen}%
\addtolength{\GGlinewidth}{-7.2pt}%
\addtolength{\GGlinewidth}{-\GGafterlen}%
\raisebox{\GGlift}{%
\vrule width \GGafterlen height \GGthickness depth 0pt%
\vrule depth 0pt height \GGthickness width 7.6pt%
\vrule width \GGafterlen height \GGthickness depth 0pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGoddspace}
% Generate a horizontal line of the length of a concavity minus 
% the length of a negation/conditional
%    \begin{macrocode} 
\newcommand{\GGoddspace}[0]{\unskip%
\addtolength{\GGlinewidth}{-7.2pt}%
\raisebox{\GGlift}{%
\vrule width 7.2pt height \GGthickness depth 0pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGtinyspace}
% Generate a horizontal line of the length of a concavity minus 
% twice the length of a negation/conditional
%    \begin{macrocode} 
\newcommand{\GGtinyspace}[0]{\unskip%
\addtolength{\GGlinewidth}{-2.8pt}%
\raisebox{\GGlift}{%
\vrule width 2.8pt height \GGthickness depth 0pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGtiniestspace}
% Generate a horizontal line three times the length of a 
% of a negation or conditional minus a quantifier
%    \begin{macrocode} 
\newcommand{\GGtiniestspace}[0]{\unskip%
\addtolength{\GGlinewidth}{-1.6pt}%
\raisebox{\GGlift}{%
\vrule width 1.6pt height \GGthickness depth 0pt}%
\hskip \GGspace%
}
%    \end{macrocode}
%    \end{macro} 
%
% \subsection{Convenience functions}
%
%    \begin{macro}{\GGif}
% Synonym for |\GGconditional|
%    \begin{macrocode} 
\newcommand{\GGif}[2]{\GGconditional{#1}{#2}}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGifp}
% Treat premise as a terminal node
%    \begin{macrocode} 
\newcommand{\GGifp}[2]{\GGconditional{\GGterm{#1}}{#2}}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGifc}
% Treat conclusion as a terminal node
%    \begin{macrocode} 
\newcommand{\GGifc}[2]{\GGconditional{#1}{\GGterm{#2}}}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGifb}
% Treat both as terminal nodes
%    \begin{macrocode} 
\newcommand{\GGifb}[2]{\GGconditional{\GGterm{#1}}{\GGterm{#2}}}
\newcommand{\GGneg}[0]{\GGnot}
\newcommand{\GGall}[1]{\GGquant{\mathfrak{#1}}}
%    \end{macrocode}
%    \end{macro} 
%    \begin{macro}{\GGnoboth}
% Convenience shortcut for ``formatting trick"
%    \begin{macrocode} 
\newcommand{\GGnoboth}[0]{\GGnonot\GGnoquant}
%    \end{macrocode}
%    \end{macro} 
%
% The next line goes into all files and in addition prevents \dst{}
% from adding any further code from the main source file (such as a
% character table).
%    \begin{macrocode}
\endinput
%    \end{macrocode}
% 
% \DeleteShortVerb{\|}
% \Finale