Metamath Proof Explorer

Table of Contents - 20.45.10. Gottlob Frege's work: _Begriffsschrift_ and _Grundgesetze der Arithmetik_

Gottlob Frege's Begriffsschrift (German for "concept-script") is a book on logic published in 1879. It was eventually recognized as a landmark work; all work in modern formal logic is indebted to it. "During his lifetime Frege's work made little impression. However, the few people he did significantly influence - Husserl, Peano, Russell, Wittgenstein, and Carnap - themselves became enormously influential, so that indirectly he can be said to have shaped a whole philosophical tradition... But Frege was dead long before his importance was generally recognized ...". [Sullivan2004] p. 659.

"From one point of view, Frege's logic needs no explanation. The system of logic he presents in Begriffsschrift simply is modern logic... in Begriffsschrift modern logic appears to spring forth fully formed. The work's list of 'firsts' is remarkable: the first complete presentation of truth-functional propositional logic; the first representation of generality through quantifiers and variables, allowing the first formulation of reasoning involving multiple nested generality; ... (but) the most remarkable feature of Begriffsschrift is that all of these arrive at once." [Sullivan2004] p. 661-662.

Begriffsschrift built on 9 axioms expressed using a two-dimensional notation. Modern notation is significantly different, though the turnstile symbol is a vestage of its two-dimensional notation. A translation challenge for us is that in our system a value must be a (true/false value) or a , while in his system some expressions could be either. In Frege's notation "=" works with either a or a and is called content identity (equivalence/identity). For more, see statement (68) on its page 54. We represent those comparisons as separate symbols, class equivalence () and the biconditional (). In many cases Frege's "a" and "b" clearly correspond to our classes. For example, Frege takes as example for "a" an Ostrich and F(a) for "a can fly" and G(a) for "a is a bird". Later he takes Hydrogen for "a" and Oxygen for "b", and "Hydrogen is lighter than Oxygen" for f(a, b). Note that F, G, and f take classes and produce true/false values. However, "a" sometimes is used for true/false values instead. For example, page 52 statement (61) appears to read as ( ( f(c) a ) a f(a) ) a ; in this case, the "a" stands for a true/false value (a ).

Frege's logic supports second-order logic (in particular, it supports second-order quantification on class variables). In contrast, we intentially use only a first-order formalization, which does not have some of capabilities of a second-order system. Therefore, our goal is to merely show that our formalization supports all the capabilities of Frege's logic (at least his axioms) that are consistent with being a first-order system.

The following list shows the 9 axioms in a more modern notation, along with the Metamath expressions and labels that either assume or prove those axioms.

1. , Proposition 1 of [Frege1879] p. 26. We represent this as , which is our first axiom ax-1.

2. , Proposition 2 of [Frege1879] p. 26. We represent this as , which is our second axiom ax-2.

3. , Proposition 8 of [Frege1879] p. 35. We represent this as , which is proved in pm2.04.

4. , Proposition 28 of [Frege1879] p. 43. We represent this as , which is proved in con3.

5. , Proposition 31 of [Frege1879] p. 44. We represent this as , which is proved in notnotr.

6. , Proposition 41 of [Frege1879] p. 47. We represent this as , which is proved in notnot.

7. f(c) f(d) , Proposition 52 of [Frege1879] p. 50. Frege's functions (as represented by f) appear to generate true/false values in this case. As a remark to (52), Frege wrote: "The case where the content/value of c equals the content/value of d, f(c) is true and f(d) is false doesn't exist. This proposition states that c can be replaced by d if c = d. Within f(c), c could also be used in other places, not only as argument. Therefore, c can still be occur in f(d)." (This is a translation of "der Fall, wo der Inhalt von c gleich dem Inhalt von d ist, wo f(c) bejaht und f(d) verneint wird, findet nicht statt. Dieser Satz drückt aus, dass man überall statt c d setzen könne, wenn c = d ist. In f(c) kann c auch an andern als den Argumentsstellen vorkommen. Daher kann c auch noch in f(d) enthalten sein.") The last two sentences seem to mean that c as an argument of f is a free variable in f, but could also be contained as bound variable in f. Such bound variables are not replaced if c is substituted by d. This is more challenging to represent exactly, but a representation of its spirit seems adequate. We can generally represent this as , which is dfsbcq. Note that we can also handle the case where f produces a class; that would be , which is fveq2,

8. , Proposition 54 of [Frege1879] p. 50. We can represent this for wffs as , which is biid, or for classes as , which is eqid. The rule is also known as the law of identity, and is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20).

9. f(a) f(c) , Proposition 58 of [Frege1879] p. 51. We can represent this as , which is spsbc. Note that we add the condition that the value being replaced (c in the original and in our translation) must itself be a set. Frege assumed naive set theory, where everything expressable is a set. When Bertrand Russell showed that this led to problems, by showing "Russell's paradox" (ru), this began the process that led to ZFC and many other hallmarks of modern logic.

The situation is more complex regarding Frege's inference rules. In his preface Frege claims to have used only one mode of inference, modus ponens (our ax-mp), but he later qualifies this. In practice "Frege is at no great pains to separate out inference rules from his explanation of the notation and conventions governing it" and is inexact in some of their specifications ([Sullivan2004] p. 671-672). This makes it more difficult to map Frege's inference rules into our representation. The additional rules, per [Sullivan2004] p. 671-672, are:

1. Instantiation: "from a [universally quantified] judgement ∀aΦa we can always derive an arbitrary number of judgements with less general content Φ(Γ) by putting something different each time in place of the gothic letter." (CN 130). Something similar is in spsbc.

2. Uniform replacement of bound variables. (CN 130). We believe this is the same as cbval.

3. Substitution: "other substitutions (than previous) are permitted only if the concavity follows immediately after the judgement stroke..." (CN 130).

4. Generalization: "An italic letter may always be replaced by a gothic letter which does not yet occur in the judgement; when this is done, the concavity must be placed immediately after the judgement stroke" (CN 132). We can represent this as , the rule of generalization, which is our axiom ax-gen.

5. Confinement: "... from Γ Φa we can derive Γ a Φa if Γ is an expression in which a does not occur and a stands only in argument places of Φa" (CN 132). This appears to be alrimiv.

Frege's two-volume work of 1893/1903, Grundgesetze der Arithmetik ("Foundations of Arithmetic") proved various fundamental propositions of arithmetic based on the logic of Begriffsschrift plus a few extra laws. For more, see:

Unfortunately Frege's Basic Law V in this work caused the system to be inconsistent because it was subject to Russell's paradox.

Basic Law V is now known as the "axiom schema of unrestricted comprehension)", and is what cause his system to break down. Frege used basic law V primarily to prove "Hume's Principle", and he then used Hume's Principle from then on to prove other matters. So while Frege didn't see the fix at the time, it appears that accepting Hume's Principle instead of basic law V repairs his system.

Hume's Principle is carden (other related theorems are hasheni and the finite-set-only hashen).