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.