Semi-Formal Description of Frege's Begriffsschrift

See also: informal description of first order predicate logic
formal description of predicate logic
and What is Logic?.

This is a semi-formal specification of something close to the logic described by Gottlob Frege in [Frege1879]. I call the specification semi-formal because I am not supplying a definition of the metalanguage in which it is written. The concrete syntax of the formal system described by Frege in Begriffsschrift is graphical (for details see: ). I have not attempted to replicate this, but have confined myself to describing an equivalent system in more conventional linear syntax. Though the Begriffsschrift marked the beginning of a new epoch in Logic it falls short of perfection in some aspects of the definition of the formal system, and it has thefore been necessary (for the purpose of presenting a fully defined formal system) to make some definite choices which are not drawn from the text of the Begriffsschrift.

The main areas in which this has been necessary are: substitution Frege is not explicit about how substitution is to be undertaken or about the inference rules which involve substitution. Abstraction and beta reduction In this system functional abstractions are permitted in substitutions and are automatically beta-reduced as a part of the substitution operation. This all needs to be spelled out in detail. Type system Some kind of type-like constraint system is necessary for the logic to be consistent. The system is usually read as a second order logic, though there is very little in the Begriffsscrift to justify this interpretation.