Frege's theorem
Metatheorem From Wikipedia, the free encyclopedia
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 (The Foundations of Arithmetic)[1] and proven more formally in his 1893 Grundgesetze der Arithmetik I (Basic Laws of Arithmetic I).[2] 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 (at least of the Scottish School variety).
Overview
In The Foundations of Arithmetic (1884), and later, in Basic Laws of Arithmetic (vol. 1, 1893; vol. 2, 1903), Frege attempted to derive all of the laws of arithmetic from axioms he asserted as logical (see logicism). Most of these axioms were carried over from his Begriffsschrift; the one truly new principle was one he called the Basic Law V[2] (now known as the axiom schema of unrestricted comprehension):[3] the "value-range" of the function f(x) is the same as the "value-range" of the function g(x) if and only if ∀x[f(x) = g(x)]. However, not only did Basic Law V fail to be a logical proposition, but the resulting system proved to be inconsistent, because it was subject to Russell's paradox.[4]
The inconsistency in Frege's Grundgesetze overshadowed Frege's achievement: according to Edward Zalta, the Grundgesetze "contains all the essential steps of a valid proof (in second-order logic) of the fundamental propositions of arithmetic from a single consistent principle."[4] This achievement has become known as Frege's theorem.[4][5]
Frege's theorem in propositional logic
Summarize
Perspective
( | P | → | ( | Q | → | R | )) | → | (( | P | → | Q | ) | → | ( | P | → | R | )) |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✗ | ✓ | ✗ | ![]() | ✗ | ✓ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✗ | ✓ | ✗ | ![]() | ✗ | ✓ | ✓ | |||||||
![]() | ![]() | ![]() | ✗ | ![]() | ![]() | ✗ | ✓ | ✓ | ![]() | ✗ | ✓ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✗ | ✓ | ✓ | ![]() | ✗ | ✓ | ✓ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✓ | ✗ | ✗ | ![]() | ✓ | ✗ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✓ | ✗ | ✗ | ![]() | ✓ | ✓ | ✓ | |||||||
![]() | ![]() | ![]() | ✗ | ![]() | ![]() | ✓ | ✓ | ✓ | ![]() | ✓ | ✗ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✓ | ✓ | ✓ | ![]() | ✓ | ✓ | ✓ | |||||||
1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 |
In propositional logic, Frege's theorem refers to this tautology:
The theorem already holds in one of the weakest logics imaginable, the constructive implicational calculus. The proof under the Brouwer–Heyting–Kolmogorov interpretation reads . In words: "Let f denote a reason that P implies that Q implies R. And let g denote a reason that P implies Q. Then given a f, then given a g, then given a reason p for P, we know that both Q holds by g and that Q implies R holds by f. So R holds."
The truth table to the right gives a semantic proof. For all possible assignments of false (✗) or true (✓) to P, Q, and R (columns 1, 3, 5), each subformula is evaluated according to the rules for material conditional, the result being shown below its main operator. Column 6 shows that the whole formula evaluates to true in every case, i.e. that it is a tautology. In fact, its antecedent (column 2) and its consequent (column 10) are even equivalent.
Special cases
One commonly takes to mean , where denotes a false proposition. With for , the theorem entails the curried form of the negation introduction principle,
Notes
References
Wikiwand - on
Seamless Wikipedia browsing. On steroids.