summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/grundgesetze
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/grundgesetze
Initial commit
Diffstat (limited to 'macros/latex/contrib/grundgesetze')
-rw-r--r--macros/latex/contrib/grundgesetze/README19
-rw-r--r--macros/latex/contrib/grundgesetze/grundgesetze.dtx1038
-rw-r--r--macros/latex/contrib/grundgesetze/grundgesetze.ins11
-rw-r--r--macros/latex/contrib/grundgesetze/grundgesetze.pdfbin0 -> 224805 bytes
4 files changed, 1068 insertions, 0 deletions
diff --git a/macros/latex/contrib/grundgesetze/README b/macros/latex/contrib/grundgesetze/README
new file mode 100644
index 0000000000..52a2479823
--- /dev/null
+++ b/macros/latex/contrib/grundgesetze/README
@@ -0,0 +1,19 @@
+grundgesetze.sty - a LaTeX2e package for typesetting
+Gottlob Frege's concept-script in the style of his
+Grundgesetze der Arithmetik (Basic Laws of Arithmetic)
+
+See the file grundgesetze.pdf for information on how to access
+to these symbols from LaTeX.
+
+The file grundgesetze.sty is a derivative work of begriff.sty
+(Copyright (c) 2005 Josh Parsons, Richard G. Heck Jr.) and so,
+like it, is released under the GNU General Public License
+(version 2).
+The remainder of this work is Copyright (c) 2008-2014 Richard
+G. Heck Jr., J.J. Green, Agustin Rayo, and Marcus Rossberg.
+
+Further information can be found at
+
+ http://www.frege.info/
+
+Marcus Rossberg 2014 \ No newline at end of file
diff --git a/macros/latex/contrib/grundgesetze/grundgesetze.dtx b/macros/latex/contrib/grundgesetze/grundgesetze.dtx
new file mode 100644
index 0000000000..84005cb1da
--- /dev/null
+++ b/macros/latex/contrib/grundgesetze/grundgesetze.dtx
@@ -0,0 +1,1038 @@
+% \iffalse meta-comment
+%
+% grundgesetze: LaTeX2e package for typesetting begriffsschrift
+% in the of Gottlob Frege's _Grundgesetze der Arithmetik_ (Jena 1893/1903)
+%
+% Copyright (C) 2003-2014 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 G. Heck, Jr. <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.
+%
+% 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> [2014/06/16 1.02 grundgesetze package]
+%
+%<*driver>
+\documentclass[a4paper,10pt,draft]{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{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
+% Gottlob Frege's \emph{begriffs\-schrift} [concept-script] formalism
+% in the style of his \emph{Grundgesetze der Arithmetik}
+% (1893/1903). \emph{Grundgesetze.sty} 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} (1879). It was amended by Richard~G.~Heck~Jr.,
+% J.\,J.~Green, Agust\'in~Rayo, and Marcus~Rossberg. Thanks to
+% Philip Ebert for testing and suggestions. Note that 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 (being the size to be used,
+% as in |bguq=6|, the default being 5). Of course, one must have the
+% |bguq| font installed to use this option, but 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}$ (i.e., `$p\supset q$')
+%
+% \DescribeMacro{\GGquant}
+% Concavity: called as |\GGquant{\mathfrak a}| gives
+% $\GGquant{\mathfrak a}$ (i.e., universal quantifier,
+% `$\mathfrak{a}$' is the quantified variable)
+%
+% \DescribeMacro{\GGjudge}
+% Judgement-stroke, $\GGjudge$
+%
+% \DescribeMacro{\GGdef}
+% Definition-stroke, $\GGdef$
+%
+% \DescribeMacro{\GGbracket}
+% Automatically scaling brackets, |\GGbracket{\ldots}| yields
+% $\GGbracket{\ldots}$ (see examples)
+%
+% \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 basic laws of logic,
+% available for download on \texttt{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 via mouse-click and that will
+% calculate and output the correct values. The GUI is available for
+% download on \texttt{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 preferred 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 in this way:
+% \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} (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 (using wrap
+% search) ``|\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: June 2014}
+\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\baselineskip depth 0.425\baselineskip 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\baselineskip 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
diff --git a/macros/latex/contrib/grundgesetze/grundgesetze.ins b/macros/latex/contrib/grundgesetze/grundgesetze.ins
new file mode 100644
index 0000000000..7649242b35
--- /dev/null
+++ b/macros/latex/contrib/grundgesetze/grundgesetze.ins
@@ -0,0 +1,11 @@
+% -*- tex -*-
+% grundgesetze.ins
+% docstrip wrapper for the grundgesetze wrapper
+\def\batchfile{grundgesetze.ins}
+\input docstrip.tex
+\preamble
+docstrip wrapper for grundgesetze
+\endpreamble
+\keepsilent
+\generateFile{grundgesetze.sty}{t}{\from{grundgesetze.dtx}{package}}
+\endinput
diff --git a/macros/latex/contrib/grundgesetze/grundgesetze.pdf b/macros/latex/contrib/grundgesetze/grundgesetze.pdf
new file mode 100644
index 0000000000..10f3cef32d
--- /dev/null
+++ b/macros/latex/contrib/grundgesetze/grundgesetze.pdf
Binary files differ