Updating Frege’s Begriffsschrift to Modern Notation
I am going to update this post later but right now, I am only publishing it in this form to make it easier for me to keep reading the book. Just to give a sense of why this is necessary, many of the pages in Begriffsschrift looks like follows:
As you can see (but probably can’t tell if you are unfamiliar with his notation), he keeps using previously deduced sentences with substitution and modus ponens to deduce new ones but after 20-30 pages of this, you really don’t remember those formulas and it is hard to navigate the book to find them because each derivation takes half a page.
So I decided to type them out here so that I can check this post out while I am reading. As such, the post will grow as I make progress. (Also, I’m sorry for the horrible formatting below but for some reason, I couldn’t get standard ways of aligning equations in $\LaTeX$ to work and I want to keep reading instead of fixing the theme/math issues. I’ll revisit this issue and try to align them better at some point.) $$ (1) \quad A \to (B \to A) $$ $$ (2) \quad (C \to (B \to A)) \to ((C \to B) \to (C \to A)) $$ $$ (3) \quad (B \to A) \to ((C \to (B \to A)) \to ((C \to B) \to (C \to A))) $$ $$ (4) \quad ((B \to A) \to (C \to (B \to A))) \to ((B \to A) \to ((C \to B) \to (C \to A))) $$
$$ (5) \quad (B \to A) \to ((C \to B) \to (C \to A)) $$
$$ (6) \quad (C \to (B \to A)) \to (C \to ((D \to B) \to (D \to A))) $$
$$ (7) \quad (B \to A) \to ((D \to (C \to B)) \to (D \to ((C \to A)))) $$
$$ (8) \quad (D \to (B \to A)) \to (B \to (D \to A)) $$
$$ (9) \quad (C \to B) \to ((B \to A) \to (C \to A)) $$
$$ (10) \quad ((E \to (D \to B)) \to A) \to ((D \to (E \to B)) \to A) $$
$$ (11) \quad (C \to (B \to A)) \to (B \to (C \to A)) $$
$$ (12) \quad (D \to (C \to (B \to A))) \to (D \to (B \to (C \to A))) $$
$$ (13) \quad (D \to (C \to (B \to A))) \to (B \to (D \to (C \to A))) $$
$$ (14) \quad (E \to (D \to (C \to (B \to A)))) \to (E \to (B \to (D \to (C \to A)))) $$
$$ (15) \quad (E \to (D \to (C \to (B \to A)))) \to (B \to (E \to (D \to (C \to A)))) $$
$$ (16) \quad (E \to (D \to (C \to (B \to A)))) \to (E \to (D \to (B \to (C \to A)))) $$
$$ (17) \quad (D \to (C \to (B \to A))) \to (C \to (B \to (D \to A))) $$
$$ (18) \quad (C \to (B \to A)) \to ((D \to C) \to (B \to (D \to A))) $$
$$ (19) \quad (D \to (C \to B)) \to ((B \to A) \to (D \to (C \to A))) $$
$$ (20) \quad (E \to (D \to (C \to B))) \to ((B\to A)\to (E \to (D \to (C \to A)))) $$
$$ (21) \quad ((D \to B) \to A) \to ((D\to C)\to ((C \to B) \to A)) $$
…
$$ (27) \quad (A \to A) $$
$$ (28) \quad (B \to A) \to (\neg A \to \neg B) $$
$$ (29) \quad (C \to (B \to A)) \to (C \to (\neg A \to \neg B)) $$
$$ (30) \quad (B \to (C \to A)) \to (C \to (\neg A \to \neg B)) $$
$$ (31) \quad (\neg\neg A \to A) $$
…
$$ (33) \quad (\neg B \to A) \to (\neg A \to b) $$
$$ (34) \quad (C\to (\neg B \to A)) \to (C\to(\neg A \to b)) $$
…
$$ (36) \quad (A \to (\neg A \to B)) $$
…
$$ (41) \quad (A \to \neg\neg A) $$
…
$$ (52) \quad (C \iff D) \to (f(C) \to f(D)) $$
$$ (54) \quad (C \iff C) $$
$$ (58) \quad (\forall A, f(A)) \to f(C) $$
…
$$ (68) \quad ((\forall A, f(A)) \iff B) \to (B \to F(C)) $$
$$ (69) \quad (\forall D, (F(D) \to (\forall A, (f(D, A) \to F(A))))) \iff (\text{The property $F$ is hereditary in the $f$-sequence.}) $$