Frege’s Begriffsschrift is one of the most important works in the history of logic. Frege is also an extremely careful writer and, it is in general a delight to read his works. However, he uses a unique logical notation, which can be a little disorienting. So, when I started reading the work, I had to translate the formulas into standard modern notation: first in my mind, then on a piece of paper, and eventually by typing them out to make it easier to look them up. Let me show what a page looks like in the original notation:
As you can see (but probably can’t tell if you are unfamiliar with his notation), he repeatedly uses previously derived formulas, together with substitution and modus ponens, to derive new ones. After 20-30 pages of this, you really don’t remember those formulas, and it is hard to navigate the book to find them again because a single derivation often takes at least half a page.
To be clear, this notation is ingenious, but it is not convenient as a reference while reading the book.1 So, this page gives the numbered formulas of Begriffsschrift in modern notation. I include Frege’s numbering and keep his short glosses when needed for his definitions.
In (1)-(51), $a$, $b$, $c$, etc. are sentence letters. Lowercase Greek letters are bound object variables, and $F$ is a concept variable. I use $:=$ for explicit definitions, $=$ for Frege’s content-identity sign, and $\lor$ where he expresses disjunction using negation and implication.2 I write $\lambda u.\,\varphi(u)$ for the property that holds of $u$ exactly when the condition $\varphi(u)$ does. In Part III, I abbreviate
\[
\begin{aligned}
&\operatorname{In}_f(x,F) \;:=\; \forall\alpha\,\bigl(f(x,\alpha)\to F(\alpha)\bigr).
\end{aligned}
\]
Thus, $\operatorname{In}_f(x,F)$ says that every immediate $f$-result of $x$ has property $F$.
Propositional logic: (1)-(51)
\[
\begin{aligned}
&a \to (b \to a)
\end{aligned}
\]
(1)
\[
\begin{aligned}
&(c \to (b \to a)) \to ((c \to b) \to (c \to a))
\end{aligned}
\]
(2)
\[
\begin{aligned}
&(b \to a) \to ((c \to (b \to a)) \to{} \\
&\quad\quad((c \to b) \to (c \to a)))
\end{aligned}
\]
(3)
\[
\begin{aligned}
&((b \to a) \to (c \to (b \to a))) \to{} \\
&\quad((b \to a) \to ((c \to b) \to (c \to a)))
\end{aligned}
\]
(4)
\[
\begin{aligned}
&(b \to a) \to ((c \to b) \to (c \to a))
\end{aligned}
\]
(5)
\[
\begin{aligned}
&(c \to (b \to a)) \to (c \to ((d \to b) \to (d \to a)))
\end{aligned}
\]
(6)
\[
\begin{aligned}
&(b \to a) \to ((d \to (c \to b)) \to (d \to (c \to a)))
\end{aligned}
\]
(7)
\[
\begin{aligned}
&(d \to (b \to a)) \to (b \to (d \to a))
\end{aligned}
\]
(8)
\[
\begin{aligned}
&(c \to b) \to ((b \to a) \to (c \to a))
\end{aligned}
\]
(9)
\[
\begin{aligned}
&((e \to (d \to b)) \to a) \to ((d \to (e \to b)) \to a)
\end{aligned}
\]
(10)
\[
\begin{aligned}
&((c \to b) \to a) \to (b \to a)
\end{aligned}
\]
(11)
\[
\begin{aligned}
&(d \to (c \to (b \to a))) \to (d \to (b \to (c \to a)))
\end{aligned}
\]
(12)
\[
\begin{aligned}
&(d \to (c \to (b \to a))) \to (b \to (d \to (c \to a)))
\end{aligned}
\]
(13)
\[
\begin{aligned}
&(e \to (d \to (c \to (b \to a)))) \to{} \\
&\quad(e \to (b \to (d \to (c \to a))))
\end{aligned}
\]
(14)
\[
\begin{aligned}
&(e \to (d \to (c \to (b \to a)))) \to{} \\
&\quad(b \to (e \to (d \to (c \to a))))
\end{aligned}
\]
(15)
\[
\begin{aligned}
&(e \to (d \to (c \to (b \to a)))) \to{} \\
&\quad(e \to (d \to (b \to (c \to a))))
\end{aligned}
\]
(16)
\[
\begin{aligned}
&(d \to (c \to (b \to a))) \to (c \to (b \to (d \to a)))
\end{aligned}
\]
(17)
\[
\begin{aligned}
&(c \to (b \to a)) \to ((d \to c) \to (b \to (d \to a)))
\end{aligned}
\]
(18)
\[
\begin{aligned}
&(d \to (c \to b)) \to ((b \to a) \to (d \to (c \to a)))
\end{aligned}
\]
(19)
\[
\begin{aligned}
&(e \to (d \to (c \to b))) \to{} \\
&\quad((b \to a) \to (e \to (d \to (c \to a))))
\end{aligned}
\]
(20)
\[
\begin{aligned}
&((d \to b) \to a) \to ((d \to c) \to ((c \to b) \to a))
\end{aligned}
\]
(21)
\[
\begin{aligned}
&(f \to (e \to (d \to (c \to (b \to a))))) \to{} \\
&\quad(f \to (e \to (d \to (b \to (c \to a)))))
\end{aligned}
\]
(22)
\[
\begin{aligned}
&(d \to (c \to (b \to a))) \to{} \\
&\quad((e \to d) \to (c \to (b \to (e \to a))))
\end{aligned}
\]
(23)
\[
\begin{aligned}
&(c \to a) \to (c \to (b \to a))
\end{aligned}
\]
(24)
\[
\begin{aligned}
&(d \to (c \to a)) \to (d \to (c \to (b \to a)))
\end{aligned}
\]
(25)
\[
\begin{aligned}
&b \to (a \to a)
\end{aligned}
\]
(26)
\[
\begin{aligned}
&a \to a
\end{aligned}
\]
(27)
\[
\begin{aligned}
&(b \to a) \to (\neg a \to \neg b)
\end{aligned}
\]
(28)
\[
\begin{aligned}
&(c \to (b \to a)) \to (c \to (\neg a \to \neg b))
\end{aligned}
\]
(29)
\[
\begin{aligned}
&(b \to (c \to a)) \to (c \to (\neg a \to \neg b))
\end{aligned}
\]
(30)
\[
\begin{aligned}
&\neg\neg a \to a
\end{aligned}
\]
(31)
\[
\begin{aligned}
&((\neg b \to a) \to (\neg a \to \neg\neg b)) \to{} \\
&\quad((\neg b \to a) \to (\neg a \to b))
\end{aligned}
\]
(32)
\[
\begin{aligned}
&(\neg b \to a) \to (\neg a \to b)
\end{aligned}
\]
(33)
\[
\begin{aligned}
&(c \to (\neg b \to a)) \to (c \to (\neg a \to b))
\end{aligned}
\]
(34)
\[
\begin{aligned}
&(c \to (\neg b \to a)) \to (\neg a \to (c \to b))
\end{aligned}
\]
(35)
\[
\begin{aligned}
&a \to (\neg a \to b)
\end{aligned}
\]
(36)
\[
\begin{aligned}
&((\neg c \to b) \to a) \to (c \to a)
\end{aligned}
\]
(37)
\[
\begin{aligned}
&\neg a \to (a \to b)
\end{aligned}
\]
(38)
\[
\begin{aligned}
&(\neg a \to a) \to (\neg a \to b)
\end{aligned}
\]
(39)
\[
\begin{aligned}
&\neg b \to ((\neg a \to a) \to a)
\end{aligned}
\]
(40)
\[
\begin{aligned}
&a \to \neg\neg a
\end{aligned}
\]
(41)
\[
\begin{aligned}
&\neg\neg(a \to a)
\end{aligned}
\]
(42)
\[
\begin{aligned}
&(\neg a \to a) \to a
\end{aligned}
\]
(43)
\[
\begin{aligned}
&(\neg a \to c) \to ((c \to a) \to a)
\end{aligned}
\]
(44)
\[
\begin{aligned}
&((\neg c \to a) \to (\neg a \to c)) \to{} \\
&\quad((\neg c \to a) \to ((c \to a) \to a))
\end{aligned}
\]
(45)
\[
\begin{aligned}
&(\neg c \to a) \to ((c \to a) \to a)
\end{aligned}
\]
(46)
\[
\begin{aligned}
&(\neg c \to b) \to ((b \to a) \to ((c \to a) \to a))
\end{aligned}
\]
(47)
\[
\begin{aligned}
&(d \to (\neg c \to b)) \to{} \\
&\quad((b \to a) \to ((c \to a) \to (d \to a)))
\end{aligned}
\]
(48)
\[
\begin{aligned}
&(\neg c \to b) \to ((c \to a) \to ((b \to a) \to a))
\end{aligned}
\]
(49)
\[
\begin{aligned}
&(c \to a) \to ((b \to a) \to ((\neg c \to b) \to a))
\end{aligned}
\]
(50)
\[
\begin{aligned}
&(d \to (c \to a)) \to{} \\
&\quad((b \to a) \to (d \to ((\neg c \to b) \to a)))
\end{aligned}
\]
(51)
Identity and quantification: (52)-(68)
\[
\begin{aligned}
&(c=d) \to (f(c) \to f(d))
\end{aligned}
\]
(52)
\[
\begin{aligned}
&f(c) \to ((c=d) \to f(d))
\end{aligned}
\]
(53)
\[
\begin{aligned}
&c=c
\end{aligned}
\]
(54)
\[
\begin{aligned}
&(c=d) \to (d=c)
\end{aligned}
\]
(55)
\[
\begin{aligned}
&((d=c) \to (f(d) \to f(c))) \to{} \\
&\quad((c=d) \to (f(d) \to f(c)))
\end{aligned}
\]
(56)
\[
\begin{aligned}
&(c=d) \to (f(d) \to f(c))
\end{aligned}
\]
(57)
\[
\begin{aligned}
&(\forall \alpha\,f(\alpha)) \to f(c)
\end{aligned}
\]
(58)
\[
\begin{aligned}
&g(b) \to \bigl(\neg f(b) \to \neg\forall\alpha\,(g(\alpha)\to f(\alpha))\bigr)
\end{aligned}
\]
(59)
\[
\begin{aligned}
&(\forall\alpha\,\bigl(h(\alpha)\to(g(\alpha)\to f(\alpha))\bigr)) \to \bigl(g(b)\to(h(b)\to f(b))\bigr)
\end{aligned}
\]
(60)
\[
\begin{aligned}
&(f(c) \to a) \to ((\forall\alpha\,f(\alpha)) \to a)
\end{aligned}
\]
(61)
\[
\begin{aligned}
&g(y) \to \bigl((\forall\alpha\,(g(\alpha)\to f(\alpha))) \to f(y)\bigr)
\end{aligned}
\]
(62)
\[
\begin{aligned}
&g(y) \to \bigl(m \to ((\forall\alpha\,(g(\alpha)\to f(\alpha))) \to f(y))\bigr)
\end{aligned}
\]
(63)
\[
\begin{aligned}
&(h(z) \to g(y)) \to{} \\
&\quad\bigl((\forall\alpha\,(g(\alpha)\to f(\alpha))) \to (h(z)\to f(y))\bigr)
\end{aligned}
\]
(64)
\[
\begin{aligned}
&(\forall\alpha\,(h(\alpha)\to g(\alpha))) \to{} \\
&\quad\bigl((\forall\alpha\,(g(\alpha)\to f(\alpha))) \to (h(y)\to f(y))\bigr)
\end{aligned}
\]
(65)
\[
\begin{aligned}
&(\forall\alpha\,(g(\alpha)\to f(\alpha))) \to{} \\
&\quad\bigl((\forall\alpha\,(h(\alpha)\to g(\alpha))) \to (h(y)\to f(y))\bigr)
\end{aligned}
\]
(66)
\[
\begin{aligned}
&(((\forall\alpha\,f(\alpha))=b) \to (b\to\forall\alpha\,f(\alpha))) \to{} \\
&\quad(((\forall\alpha\,f(\alpha))=b) \to (b\to f(c)))
\end{aligned}
\]
(67)
\[
\begin{aligned}
&((\forall\alpha\,f(\alpha))=b) \to (b\to f(c))
\end{aligned}
\]
(68)
A general theory of sequences: (69)-(133)
§24. Heredity
\[
\begin{aligned}
&\mathcal H_f(F) \;:=\; \forall\beta\,\bigl(F(\beta)\to \operatorname{In}_f(\beta,F)\bigr)
\end{aligned}
\]
(69)
$\mathcal H_f(F)$ means that $F$ is hereditary in the $f$-sequence.
§25. Consequences
\[
\begin{aligned}
&\mathcal H_f(F) \to \bigl(F(x)\to \operatorname{In}_f(x,F)\bigr)
\end{aligned}
\]
(70)
\[
\begin{aligned}
&\bigl(\operatorname{In}_f(x,F)\to(f(x,y)\to F(y))\bigr) \to{} \\
&\quad\bigl(\mathcal H_f(F)\to(F(x)\to(f(x,y)\to F(y)))\bigr)
\end{aligned}
\]
(71)
\[
\begin{aligned}
&\mathcal H_f(F) \to \bigl(F(x)\to(f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(72)
\[
\begin{aligned}
&\bigl(\mathcal H_f(F)\to F(x)\bigr) \to \bigl(\mathcal H_f(F)\to(f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(73)
\[
\begin{aligned}
&F(x) \to \bigl(\mathcal H_f(F)\to(f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(74)
\[
\begin{aligned}
&(\forall\beta\,\bigl(F(\beta)\to \operatorname{In}_f(\beta,F)\bigr)) \to \mathcal H_f(F)
\end{aligned}
\]
(75)
§26. Succession in a sequence
\[
\begin{aligned}
&\mathcal A_f(x,y) \;:=\; \forall F\,\bigl(\mathcal H_f(F)\to(\operatorname{In}_f(x,F)\to F(y))\bigr)
\end{aligned}
\]
(76)
$\mathcal A_f(x,y)$ means that $y$ follows $x$ in the $f$-sequence, or that $x$ precedes $y$.
§27. Consequences
\[
\begin{aligned}
&\mathcal A_f(x,y) \to \bigl(\mathcal H_f(F)\to(\operatorname{In}_f(x,F)\to F(y))\bigr)
\end{aligned}
\]
(77)
\[
\begin{aligned}
&\mathcal H_f(F) \to \bigl(\operatorname{In}_f(x,F)\to(\mathcal A_f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(78)
\[
\begin{aligned}
&\bigl(\mathcal H_f(F)\to \operatorname{In}_f(x,F)\bigr) \to{} \\
&\quad\bigl(\mathcal H_f(F)\to(\mathcal A_f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(79)
\[
\begin{aligned}
&\bigl(F(x)\to(\mathcal H_f(F)\to \operatorname{In}_f(x,F))\bigr) \to{} \\
&\quad\bigl(F(x)\to(\mathcal H_f(F)\to(\mathcal A_f(x,y)\to F(y)))\bigr)
\end{aligned}
\]
(80)
§28. Further consequences
\[
\begin{aligned}
&F(x) \to \bigl(\mathcal H_f(F)\to(\mathcal A_f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(81)
Frege notes: Bernoullian induction rests upon this.
\[
\begin{aligned}
&(a\to F(x)) \to \bigl(\mathcal H_f(F)\to(a\to(\mathcal A_f(x,y)\to F(y)))\bigr)
\end{aligned}
\]
(82)
\[
\begin{aligned}
&\mathcal H_f(\lambda u.\,h(u)\lor g(u)) \to{} \\
&\quad\bigl(h(x)\to(\mathcal A_f(x,y)\to(h(y)\lor g(y)))\bigr)
\end{aligned}
\]
(83)
\[
\begin{aligned}
&\mathcal H_f(F) \to \bigl(F(x)\to(\mathcal A_f(x,y)\to F(y))\bigr)
\end{aligned}
\]
(84)
\[
\begin{aligned}
&\mathcal A_f(x,y) \to \bigl(\operatorname{In}_f(x,F)\to(\mathcal H_f(F)\to F(y))\bigr)
\end{aligned}
\]
(85)
\[
\begin{aligned}
&\bigl((\mathcal H_f(F)\to F(y))\to(\mathcal H_f(F)\to(f(y,z)\to F(z)))\bigr) \to{} \\
&\quad\bigl(\mathcal A_f(x,y)\to(\operatorname{In}_f(x,F)\to{} \\
&\quad\quad\quad(\mathcal H_f(F)\to(f(y,z)\to F(z))))\bigr)
\end{aligned}
\]
(86)
\[
\begin{aligned}
&\mathcal A_f(x,y) \to \bigl(\operatorname{In}_f(x,F)\to{} \\
&\quad\quad(\mathcal H_f(F)\to(f(y,z)\to F(z)))\bigr)
\end{aligned}
\]
(87)
\[
\begin{aligned}
&f(y,z) \to \bigl(\mathcal A_f(x,y)\to{} \\
&\quad\quad(\operatorname{In}_f(x,F)\to(\mathcal H_f(F)\to F(z)))\bigr)
\end{aligned}
\]
(88)
\[
\begin{aligned}
&(\forall F\,\bigl(\mathcal H_f(F)\to(\operatorname{In}_f(x,F)\to F(y))\bigr)) \to \mathcal A_f(x,y)
\end{aligned}
\]
(89)
\[
\begin{aligned}
&\bigl(c\to\forall F\,(\mathcal H_f(F)\to(\operatorname{In}_f(x,F)\to F(y)))\bigr) \to{} \\
&\quad\bigl(c\to \mathcal A_f(x,y)\bigr)
\end{aligned}
\]
(90)
\[
\begin{aligned}
&f(x,y) \to \mathcal A_f(x,y)
\end{aligned}
\]
(91)
\[
\begin{aligned}
&(x=z) \to \bigl(f(x,y)\to \mathcal A_f(z,y)\bigr)
\end{aligned}
\]
(92)
\[
\begin{aligned}
&(\forall F\,\bigl(\operatorname{In}_f(x,F)\to(\mathcal H_f(F)\to F(y))\bigr)) \to \mathcal A_f(x,y)
\end{aligned}
\]
(93)
\[
\begin{aligned}
&\bigl(f(y,z)\to(\mathcal A_f(x,y)\to{} \\
&\quad\quad\quad\forall F\,(\operatorname{In}_f(x,F)\to(\mathcal H_f(F)\to F(z))))\bigr) \to{} \\
&\quad\bigl(f(y,z)\to(\mathcal A_f(x,y)\to \mathcal A_f(x,z))\bigr)
\end{aligned}
\]
(94)
\[
\begin{aligned}
&f(y,z) \to \bigl(\mathcal A_f(x,y)\to \mathcal A_f(x,z)\bigr)
\end{aligned}
\]
(95)
\[
\begin{aligned}
&\mathcal A_f(x,y) \to \bigl(f(y,z)\to \mathcal A_f(x,z)\bigr)
\end{aligned}
\]
(96)
\[
\begin{aligned}
&\mathcal H_f(\lambda u.\,\mathcal A_f(x,u))
\end{aligned}
\]
(97)
\[
\begin{aligned}
&\mathcal A_f(x,y) \to \bigl(\mathcal A_f(y,z)\to \mathcal A_f(x,z)\bigr)
\end{aligned}
\]
(98)
Formula (98) says that the ancestral is transitive.
§29. Belonging to a sequence
\[
\begin{aligned}
&\mathcal A_f^{=}(x,z) \;:=\; \mathcal A_f(x,z)\lor(z=x)
\end{aligned}
\]
(99)
$\mathcal A_f^{=}(x,z)$ means that $z$ belongs to the $f$-sequence beginning with $x$; equivalently, $z=x$ or $z$ follows $x$.
\[
\begin{aligned}
&\mathcal A_f^{=}(x,z) \to \bigl(\mathcal A_f(x,z)\lor(z=x)\bigr)
\end{aligned}
\]
(100)
\[
\begin{aligned}
&\bigl((z=x)\to(f(z,v)\to \mathcal A_f(x,v))\bigr) \to{} \\
&\quad\bigl((\mathcal A_f(x,z)\to(f(z,v)\to \mathcal A_f(x,v))) \to{} \\
&\quad\quad(\mathcal A_f^{=}(x,z)\to(f(z,v)\to \mathcal A_f(x,v)))\bigr)
\end{aligned}
\]
(101)
\[
\begin{aligned}
&\mathcal A_f^{=}(x,z) \to \bigl(f(z,v)\to \mathcal A_f(x,v)\bigr)
\end{aligned}
\]
(102)
\[
\begin{aligned}
&\bigl((z=x)\to(x=z)\bigr) \to \bigl(\mathcal A_f^{=}(x,z)\to(\mathcal A_f(x,z)\lor(x=z))\bigr)
\end{aligned}
\]
(103)
\[
\begin{aligned}
&\mathcal A_f^{=}(x,z) \to \bigl(\mathcal A_f(x,z)\lor(x=z)\bigr)
\end{aligned}
\]
(104)
§30. Further consequences
\[
\begin{aligned}
&\bigl(\mathcal A_f(x,z)\lor(z=x)\bigr) \to \mathcal A_f^{=}(x,z)
\end{aligned}
\]
(105)
\[
\begin{aligned}
&\mathcal A_f(x,z) \to \mathcal A_f^{=}(x,z)
\end{aligned}
\]
(106)
\[
\begin{aligned}
&\bigl(\mathcal A_f^{=}(z,y)\to(f(y,v)\to \mathcal A_f(z,v))\bigr) \to{} \\
&\quad\bigl(\mathcal A_f^{=}(z,y)\to(f(y,v)\to \mathcal A_f^{=}(z,v))\bigr)
\end{aligned}
\]
(107)
\[
\begin{aligned}
&\mathcal A_f^{=}(z,y) \to \bigl(f(y,v)\to \mathcal A_f^{=}(z,v)\bigr)
\end{aligned}
\]
(108)
\[
\begin{aligned}
&\mathcal H_f(\lambda u.\,\mathcal A_f^{=}(z,u))
\end{aligned}
\]
(109)
\[
\begin{aligned}
&\operatorname{In}_f(y,\lambda u.\,\mathcal A_f^{=}(z,u)) \to{} \\
&\quad\bigl(\mathcal A_f(y,m)\to \mathcal A_f^{=}(z,m)\bigr)
\end{aligned}
\]
(110)
\[
\begin{aligned}
&\mathcal A_f^{=}(z,y) \to \bigl(f(y,v)\to(\mathcal A_f(v,z)\lor \mathcal A_f^{=}(z,v))\bigr)
\end{aligned}
\]
(111)
\[
\begin{aligned}
&(z=x) \to \mathcal A_f^{=}(x,z)
\end{aligned}
\]
(112)
\[
\begin{aligned}
&\bigl(\mathcal A_f^{=}(z,x)\to(\mathcal A_f(z,x)\lor(z=x))\bigr) \to{} \\
&\quad\bigl(\mathcal A_f^{=}(z,x)\to(\mathcal A_f(z,x)\lor \mathcal A_f^{=}(x,z))\bigr)
\end{aligned}
\]
(113)
\[
\begin{aligned}
&\mathcal A_f^{=}(z,x) \to \bigl(\mathcal A_f(z,x)\lor \mathcal A_f^{=}(x,z)\bigr)
\end{aligned}
\]
(114)
§31. Single-valued procedures
\[
\begin{aligned}
&\mathcal S_f \;:=\; \forall\varepsilon\,\forall\beta\,\forall\alpha\,\bigl(f(\beta,\varepsilon)\to(f(\beta,\alpha)\to\alpha=\varepsilon)\bigr)
\end{aligned}
\]
(115)
$\mathcal S_f$ means that $f$ is single-valued: an object has at most one immediate $f$-result.
\[
\begin{aligned}
&\mathcal S_f \to \forall\beta\,\forall\alpha\,\bigl(f(\beta,x)\to(f(\beta,\alpha)\to\alpha=x)\bigr)
\end{aligned}
\]
(116)
\[
\begin{aligned}
&\bigl(\forall\beta\,\forall\alpha\,(f(\beta,x)\to(f(\beta,\alpha)\to\alpha=x)) \to{} \\
&\quad\quad\forall\alpha\,(f(y,x)\to(f(y,\alpha)\to\alpha=x))\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to\forall\alpha\,(f(y,x)\to(f(y,\alpha)\to\alpha=x))\bigr)
\end{aligned}
\]
(117)
\[
\begin{aligned}
&\mathcal S_f \to \forall\alpha\,\bigl(f(y,x)\to(f(y,\alpha)\to\alpha=x)\bigr)
\end{aligned}
\]
(118)
\[
\begin{aligned}
&\bigl(\forall\alpha\,(f(y,\alpha)\to\alpha=x) \to (f(y,a)\to a=x)\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to(f(y,x)\to(f(y,a)\to a=x))\bigr)
\end{aligned}
\]
(119)
\[
\begin{aligned}
&\mathcal S_f \to \bigl(f(y,x)\to(f(y,a)\to a=x)\bigr)
\end{aligned}
\]
(120)
\[
\begin{aligned}
&\bigl((a=x)\to \mathcal A_f^{=}(x,a)\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to(f(y,x)\to(f(y,a)\to \mathcal A_f^{=}(x,a)))\bigr)
\end{aligned}
\]
(121)
\[
\begin{aligned}
&\mathcal S_f \to \bigl(f(y,x)\to\forall\alpha\,\bigl(f(y,\alpha)\to \mathcal A_f^{=}(x,\alpha)\bigr)\bigr)
\end{aligned}
\]
(122)
\[
\begin{aligned}
&\bigl(\operatorname{In}_f(y,\lambda u.\,\mathcal A_f^{=}(x,u))\to{} \\
&\quad\quad(\mathcal A_f(y,m)\to \mathcal A_f^{=}(x,m))\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to(f(y,x)\to(\mathcal A_f(y,m)\to \mathcal A_f^{=}(x,m)))\bigr)
\end{aligned}
\]
(123)
\[
\begin{aligned}
&\mathcal S_f \to \bigl(f(y,x)\to(\mathcal A_f(y,m)\to \mathcal A_f^{=}(x,m))\bigr)
\end{aligned}
\]
(124)
\[
\begin{aligned}
&\bigl(\mathcal A_f^{=}(x,m)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x))\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to(f(y,x)\to{} \\
&\quad\quad\quad(\mathcal A_f(y,m)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x))))\bigr)
\end{aligned}
\]
(125)
\[
\begin{aligned}
&\mathcal S_f \to \bigl(f(y,x)\to{} \\
&\quad\quad(\mathcal A_f(y,m)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x)))\bigr)
\end{aligned}
\]
(126)
\[
\begin{aligned}
&\mathcal S_f \to \bigl(\mathcal A_f(y,m)\to{} \\
&\quad\quad(f(y,x)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x)))\bigr)
\end{aligned}
\]
(127)
\[
\begin{aligned}
&\bigl(\mathcal A_f^{=}(m,y)\to{} \\
&\quad\quad(f(y,x)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x)))\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to((\mathcal A_f(y,m)\lor \mathcal A_f^{=}(m,y))\to{} \\
&\quad\quad\quad(f(y,x)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x))))\bigr)
\end{aligned}
\]
(128)
\[
\begin{aligned}
&\mathcal S_f \to \bigl((\mathcal A_f(y,m)\lor \mathcal A_f^{=}(m,y))\to{} \\
&\quad\quad(f(y,x)\to(\mathcal A_f(x,m)\lor \mathcal A_f^{=}(m,x)))\bigr)
\end{aligned}
\]
(129)
For the final steps, write
\[
\begin{aligned}
&P_m(u) \;:=\; \mathcal A_f(u,m)\lor\mathcal A_f^{=}(m,u)
\end{aligned}
\]
Thus, $P_m(u)$ says that $u$ precedes $m$, or belongs to the $f$-sequence beginning with $m$.
\[
\begin{aligned}
&\bigl((\forall\delta\,(P_m(\delta)\to\forall\alpha\,(f(\delta,\alpha)\to P_m(\alpha))))\to \mathcal H_f(P_m)\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to \mathcal H_f(P_m)\bigr)
\end{aligned}
\]
(130)
\[
\begin{aligned}
&\mathcal S_f \to \mathcal H_f(P_m)
\end{aligned}
\]
(131)
\[
\begin{aligned}
&\bigl(\mathcal H_f(P_m)\to(\mathcal A_f(x,m)\to(\mathcal A_f(x,y)\to P_m(y)))\bigr) \to{} \\
&\quad\bigl(\mathcal S_f\to(\mathcal A_f(x,m)\to(\mathcal A_f(x,y)\to P_m(y)))\bigr)
\end{aligned}
\]
(132)
\[
\begin{aligned}
&\mathcal S_f \to \bigl(\mathcal A_f(x,m)\to{} \\
&\quad\quad(\mathcal A_f(x,y)\to(\mathcal A_f(y,m)\lor \mathcal A_f^{=}(m,y)))\bigr)
\end{aligned}
\]
(133)
Formula (133) says: if $f$ is single-valued and both $m$ and $y$ follow $x$, then $y$ precedes $m$ or belongs to the $f$-sequence beginning with $m$.
Checked against Frege’s 1879 text, the Bauer-Mengelberg and Bynum translations, Mendelsohn’s modern transcriptions of (1)-(68), and the modern reconstructions by Boolos and Heck.
-
As far as notations go, one can do much worse. I am looking at you, Peano. ↩︎
-
I didn’t want to use $\lor$, but writing it out the way Frege does makes the already long expressions even longer and much harder to fit nicely on the page. However, the usage is consistent in the sense that whenever you see $\lor$ here, you can do the classic substitution to get exactly what Frege wrote. ↩︎