Frege's theorem

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 Die Grundlagen der Arithmetik (The Foundations of Arithmetic),[page needed] published in 1884, and proven more formally in his Grundgesetze der Arithmetik (The Basic Laws of Arithmetic),[page needed] published in two volumes, in 1893 and 1903. 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.

Frege's theorem in propositional logic

( P ( Q R )) (( P Q ) ( P R ))
N N
1 2 3 4 5 6 7 8 9 10 11 12 13

In propositional logic, Frege's theorems refers to this tautology:

(P → (QR)) → ((PQ) → (PR))

The truth table to the right gives a 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.