Gottlob Frege's Grundgesetze der Arithmetik: Computational Linguistics Meets the Founder of Logicism

Our paper deals with the text technological challenges
which arise from the retrodigitalization of Gottlob Frege's
Basic Laws of Arithmetic. The digitalization is the basis for a
hypermedia presentation with various views about the text.
The German mathematician, logician, and philosopher Gottlob
Frege is regarded as the founder of logicism, i.e., the view that
mathematics can be completely derived from pure logic. The
two volumes of the Basic Laws of Arithmetic are Frege's major
work (1893/1903). Here he develops his logicist program in
detail, i.e., he deduces central arithmetic laws from logic.
Frege's work is seen as the basis of modern logic. Therefore it
is of interest not only for mathematicians but also for scholars
of various arts. Apart from its metamathematical considerations
the Basic Laws are relevant especially for philosophers of
language and for linguists, because Frege's investigations on
sense and reference, functions and concepts are accumulated
in these books.
Frege uses in his work a peculiar two-dimensional notation for
formulas of predicate logic. His notation was not taken up by
other logicians and is therefore regarded as hardly readable.
The structure of a formula is primarily symbolized by horizontal
and vertical branching lines, e.g., a little vertical line
symbolizing negation. A line which runs vertically downwards
and then parallel to another horizontal line represents a
conditional clause. Formula parts may be written linearly.
Furthermore Frege uses a lot of special symbols, which he
defines in the Basic Laws. Like his two-dimensional notation,
they were not taken up by others. For these reasons Frege's
notation deviates quite a lot from contemporary logical
formalisms. Compared to his smaller writings the Basic Laws
are therefore studied less frequently.
Our project has the goal to make Frege's work accessible to a
broader scientific community. We will offer various views with modern notations. As a precondition we have digitalized the
Basic Laws using an XML structure according to a specific
DTD. The pure text part was scanned and converted into plain
text by OCR. This part has posed only few problems due to the
high quality of the original typesetting. The digitalization of
the formula parts has cost much more effort. The logical
structure of formulas had to be entered completely by hand.
Automated methods failed due to the peculiarity of the
formalism. Special attention had to be given to the encoding
scheme of the formulas. From the XML code the original
notation should be derivable as well as various modern
notations, among these heuristically simplified notations. Frege
refers from the text to parts and single symbols of the formulas.
Changes of the form of formulas can therefore have impact on
the surrounding text. For example, he represents a universal
quantifier by a bow in a horizontal line which is superscripted
by a Gothic character. He refers to this symbol as the cavity
(Höhlung). In the text all occurrences of cavity must be replaced
by some other description in views with modern formula
notations and deviating symbols for universal quantifiers.
The XML coding of the formula trees has another scientific
application apart from providing the basis for alternate views:
it allows for an automated verification and analysis of Frege's
proofs (formula forests). The extremely compact derivations
in the Fregean calculus practically exclude a manual
verification. Here automated procedures can provide essential
help for the reader by 'unfolding the proofs', i.e., by making
intermediate implicit proof steps fully explicit.
The immediate goal of this project is the derivation of
presentations for two media. We will produce a print and web
version. The target format of the print version is valid LaTeX
documents. For the webpages we use XHTML in order to arrive
at a maximally browser independent representation. We use
exclusively XSLT for transformations. The print version with
the original Fregean formula notation is produced primarily for
control purposes. A print version with modern notational
variants is applied in an ongoing commentary project.
The web version will support a couple of notational variants
as well as proof unfolding. Links will be generated between
text and proof references. A full text search and search facilities
for formulas, definitions and lemmas will be provided.
The forms of presentation and the views sketched above will
considerably enhance the accessibility of Gottlob Frege's Basic
Laws of Arithmetic for many recipients. It provides new ways
of reception for a relevant but formally peculiar text.
Bibliography
Frege, Gottlob. Grundgesetze der Arithmetik, Band I/II. Jena:
Verlag Herman Pohle, 1893/1903