Gottlob Frege · Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens · Halle a/S.: Louis Nebert · 1879
A note on this presentation: the booklet's two-dimensional notation cannot be reproduced in running text, and its German prose is summarised below rather than quoted. The full original is at the source link.
Preface
Frege explains that, while testing how far arithmetic could be carried by inference alone, he found ordinary language too pliable to keep a chain of reasoning free of unnoticed gaps; so he devised a written notation for 'pure thought' in which every assumption is made explicit. He invokes Leibniz's old dream of a universal characteristic — a calculus of reasoning — while disclaiming that he had achieved anything so vast. He likens his concept-script to a microscope and everyday language to the eye: the eye is versatile but limited in resolving power, the microscope useless for daily life yet unmatched for the single scientific purpose it is built for.
[ … ]
Part I — Definition of the symbols
Frege sets out his primitive signs: the judgment stroke, which asserts a content; the conditional, joining two contents and denied only when the first holds while the second does not; negation; the identity of content; and, decisively, the sign for generality — a concavity carrying a variable letter — which binds a variable and lets a statement speak of every object at once. Replacing the old subject–predicate split with a function–argument analysis, he can now express relations and nested generality that earlier logic could not.
[ … ]
Part II — Representation and derivation of some judgments of pure thought
From a small set of basic laws (axioms) and essentially a single rule of inference — detaching the consequent of an asserted conditional whose antecedent is also asserted — Frege derives a sequence of logical theorems, each step formally justified. It is the first worked demonstration of proof carried out inside a fully specified formal system.
[ … ]
Part III — Some elements of a general theory of sequences
Frege defines, in purely logical terms, what it means for one object to follow another in a series: he frames the notion of a property inherited along a relation, and from it the 'ancestral' of that relation. With no appeal to intuition or counting, this captures 'following in a sequence' — the logical seed of mathematical induction and of his later attempt to ground arithmetic in logic alone.
Jena · 1879