Begriffsschrift

Last updated
Begriffsschrift
Begriffsschrift Titel.png
The title page of the original 1879 edition
AuthorGottlob Frege
LanguageEnglish
Genre Logic
PublisherLubrecht & Cramer
Publication date
1879
Pages124
ISBN 978-3487-0062-39
OCLC 851287

Begriffsschrift (German for, roughly, "concept-writing") is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book.

Contents

Begriffsschrift is usually translated as concept writing or concept notation; the full title of the book identifies it as "a formula language, modeled on that of arithmetic, for pure thought." Frege's motivation for developing his formal approach to logic resembled Leibniz's motivation for his calculus ratiocinator (despite that, in the foreword Frege clearly denies that he achieved this aim, and also that his main aim would be constructing an ideal language like Leibniz's, which Frege declares to be a quite hard and idealistic—though not impossible—task). Frege went on to employ his logical calculus in his research on the foundations of mathematics, carried out over the next quarter-century. This is the first work in Analytical Philosophy, a field that future British and Anglo philosophers such as Bertrand Russell further developed.

Notation and the system

The calculus contains the first appearance of quantified variables, and is essentially classical bivalent second-order logic with identity. It is bivalent in that sentences or formulas denote either True or False; second order because it includes relation variables in addition to object variables and allows quantification over both. The modifier "with identity" specifies that the language includes the identity relation, =. Frege stated that his book was his version of a characteristica universalis, a Leibnizian concept that would be applied in mathematics. [1]

Frege presents his calculus using idiosyncratic two-dimensional notation: connectives and quantifiers are written using lines connecting formulas, rather than the symbols ¬, ∧, and ∀ in use today. For example, that judgement B materially implies judgement A, i.e. is written as BS-05-Kondicionaliskis-svg.svg .

In the first chapter, Frege defines basic ideas and notation, like proposition ("judgement"), the universal quantifier ("the generality"), the conditional, negation and the "sign for identity of content" (which he used to indicate both material equivalence and identity proper); in the second chapter he declares nine formalized propositions as axioms.

Basic conceptFrege's notationModern notations
Judging

Negation Begriffsschrift connective1.svg

Conditional (implication) Begriffsschrift connective2.svg

Universal quantification BS-12-Begriffsschrift Quantifier1-svg.svg
Existential quantification BS-14-Begriffsschrift Quantifier3-svg.svg
Content identity (equivalence/identity)


In chapter 1, §5, Frege defines the conditional as follows:

"Let A and B refer to judgeable contents, then the four possibilities are:
  1. A is asserted, B is asserted;
  2. A is asserted, B is negated;
  3. A is negated, B is asserted;
  4. A is negated, B is negated.

Let

Kondicionaliskis wb.png

signify that the third of those possibilities does not obtain, but one of the three others does. So if we negate Begriffsschrift connective2.svg , that means the third possibility is valid, i.e. we negate A and assert B."

The calculus in Frege's work

Frege declared nine of his propositions to be axioms, and justified them by arguing informally that, given their intended meanings, they express self-evident truths. Re-expressed in contemporary notation, these axioms are:

These are propositions 1, 2, 8, 28, 31, 41, 52, 54, and 58 in the Begriffschrifft. (1)–(3) govern material implication, (4)–(6) negation, (7) and (8) identity, and (9) the universal quantifier. (7) expresses Leibniz's indiscernibility of identicals, and (8) asserts that identity is a reflexive relation.

All other propositions are deduced from (1)–(9) by invoking any of the following inference rules:

The main results of the third chapter, titled "Parts from a general series theory," concern what is now called the ancestral of a relation R. "a is an R-ancestor of b" is written "aR*b".

Frege applied the results from the Begriffsschrifft, including those on the ancestral of a relation, in his later work The Foundations of Arithmetic . Thus, if we take xRy to be the relation y = x + 1, then 0R*y is the predicate "y is a natural number." (133) says that if x, y, and z are natural numbers, then one of the following must hold: x < y, x = y, or y < x. This is the so-called "law of trichotomy".

Influence on other works

For a careful recent study of how the Begriffsschrift was reviewed in the German mathematical literature, see Vilko (1998). Some reviewers, especially Ernst Schröder, were on the whole favorable. All work in formal logic subsequent to the Begriffsschrift is indebted to it, because its second-order logic was the first formal logic capable of representing a fair bit of mathematics and natural language.

Some vestige of Frege's notation survives in the "turnstile" symbol derived from his "Urteilsstrich" (judging/inferring stroke) │ and "Inhaltsstrich" (i.e. content stroke) ──. Frege used these symbols in the Begriffsschrift in the unified form ├─ for declaring that a proposition is true. In his later "Grundgesetze" he revises slightly his interpretation of the ├─ symbol.

In "Begriffsschrift" the "Definitionsdoppelstrich" (i.e. definition double stroke) │├─ indicates that a proposition is a definition. Furthermore, the negation sign can be read as a combination of the horizontal Inhaltsstrich with a vertical negation stroke. This negation symbol was reintroduced by Arend Heyting [2] in 1930 to distinguish intuitionistic from classical negation. It also appears in Gerhard Gentzen's doctoral dissertation.

In the Tractatus Logico Philosophicus , Ludwig Wittgenstein pays homage to Frege by employing the term Begriffsschrift as a synonym for logical formalism.

Frege's 1892 essay, "On Sense and Reference," recants some of the conclusions of the Begriffsschrifft about identity (denoted in mathematics by the "=" sign). In particular, he rejects the "Begriffsschrift" view that the identity predicate expresses a relationship between names, in favor of the conclusion that it expresses a relationship between the objects that are denoted by those names.

Editions

Translations:

See also

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

<span class="mw-page-title-main">Logical connective</span> Symbol connecting sentential formulas in logic

In logic, a logical connective is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .

The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, equivalence, and negation. Some sources include other connectives, as in the table below.

In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Although it is quite freely used in mathematical proofs, not every school of mathematical thought accepts this kind of nonconstructive proof as universally valid.

<span class="mw-page-title-main">De Morgan's laws</span> Pair of logical equivalences

In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.

In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when there is no formula such that and .

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", or "for any". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, but not universally, called relevant logic by British and, especially, Australian logicians, and relevance logic by American logicians.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.

In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation-complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

In mathematical logic, a tautology is a formula or assertion that is true in every possible interpretation. An example is "x=y or x≠y". Similarly, "either the ball is green, or the ball is not green" is always true, regardless of the colour of the ball.

In metalogic and metamathematics, Frege's theorem is a metatheorem that states that the Peano axioms of arithmetic can be derived in second-order logic from Hume's principle. It was first proven, informally, by Gottlob Frege in his 1884 Die Grundlagen der Arithmetik and proven more formally in his 1893 Grundgesetze der Arithmetik I. The theorem was re-discovered by Crispin Wright in the early 1980s and has since been the focus of significant work. It is at the core of the philosophy of mathematics known as neo-logicism.

In mathematical logic and computer science the symbol ⊢ has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails".

In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices called predicate functors that operate on terms to yield terms. PFL is mostly the invention of the logician and philosopher Willard Quine.

In mathematical logic, the ancestral relation of a binary relation R is its transitive closure, however defined in a different way, see below.

The mathematical concept of a function dates from the 17th century in connection with the development of the calculus; for example, the slope of a graph at a point was regarded as a function of the x-coordinate of the point. Functions were not explicitly considered in antiquity, but some precursors of the concept can perhaps be seen in the work of medieval philosophers and mathematicians such as Oresme.

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier in the first order formula expresses that everything in the domain satisfies the property denoted by . On the other hand, the existential quantifier in the formula expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula. A quantified formula must contain a bound variable and a subformula specifying a property of the referent of that variable.

References

  1. Korte, Tapio (2008-10-22). "Frege's Begriffsschrift as a lingua characteristica". Synthese. 174 (2): 283–294. doi:10.1007/s11229-008-9422-7. S2CID   20587814.
  2. Arend Heyting: "Die formalen Regeln der intuitionistischen Logik," in: Sitzungsberichte der preußischen Akademie der Wissenschaften, physikalisch-mathematische Klasse, 1930, pp. 42–65.

Bibliography