Workshop on Mathematical User Interfaces
A mechanised environment for Frege’s Begriffsschrift notation
Abstract:
Frege’s Begriffschrift introduced new levels of sophistication
and complexity in logical syntax and its representation; its twodimensional
nature has proved a stumbling block for those seeking to understand Frege’s
ideas and his system. It is, however, merely a form of abstract syntax for a
higher-order predicate logic, with proofs represented linearly and formulae
two-dimensionally. Our work concerns the development of a Java and XML-based
GUI for the interactive construction of formulae (and, in due course, of
proofs) of this system, with output in concrete form such as LATEX. It is
intended to make Frege’s notation more easily used and understood, and to
illustrate XML techniques on a seriously challenging and unusual problem.
End users will be Frege scholars; we plan to make the system available in
due course as a web-based application either publicly or in association with
a publisher.