En metalógica y metamatemática , el teorema de Frege es un metateorema que establece que los axiomas de Peano de la aritmética pueden derivarse en lógica de segundo orden a partir del principio de Hume . Fue demostrado por primera vez, de manera informal, por Gottlob Frege en su Die Grundlagen der Arithmetik ( Los fundamentos de la aritmética ) de 1884 [1] y demostrado de manera más formal en su Grundgesetze der Arithmetik I ( Leyes básicas de la aritmética I) de 1893. [2] El teorema fue redescubierto por Crispin Wright a principios de la década de 1980 y desde entonces ha sido el foco de un trabajo significativo. Está en el núcleo de la filosofía de las matemáticas conocida como neologicismo (al menos de la variedad de la Escuela Escocesa ).
En Fundamentos de la aritmética (1884) y, más tarde, en Leyes básicas de la aritmética (vol. 1, 1893; vol. 2, 1903), Frege intentó derivar todas las leyes de la aritmética a partir de axiomas que afirmaba que eran lógicos (véase logicismo ). La mayoría de estos axiomas fueron tomados de su Begriffsschrift ; el único principio verdaderamente nuevo fue uno que llamó Ley básica V [2] (ahora conocido como el esquema axiomático de comprensión irrestricta ): [3] el "rango de valores" de la función f ( x ) es el mismo que el "rango de valores" de la función g ( x ) si y solo si ∀ x [ f ( x ) = g ( x )]. Sin embargo, no solo la Ley básica V no logró ser una proposición lógica, sino que el sistema resultante demostró ser inconsistente, porque estaba sujeto a la paradoja de Russell . [4]
La inconsistencia de los Grundgesetze de Frege eclipsó el logro de Frege: según Edward Zalta , los Grundgesetze "contienen todos los pasos esenciales de una prueba válida (en lógica de segundo orden ) de las proposiciones fundamentales de la aritmética a partir de un único principio consistente". [4] Este logro se ha conocido como el teorema de Frege. [4] [5]
En lógica proposicional , el teorema de Frege se refiere a esta tautología :
El teorema ya se cumple en una de las lógicas más débiles imaginables, el cálculo implicacional constructivo . La prueba bajo la interpretación de Brouwer–Heyting–Kolmogorov dice : “Sea f una razón por la que P implica que Q implica R. Y sea g una razón por la que P implica Q. Entonces, dada una f , luego dada una g , luego dada una razón p para P , sabemos que tanto Q se cumple por g como que Q implica que R se cumple por f . Por lo tanto, R se cumple”.
La tabla de verdad de la derecha proporciona una prueba semántica. Para todas las posibles asignaciones de falso ( ✗ ) o verdadero ( ✓ ) a P , Q y R (columnas 1, 3, 5), cada subfórmula se evalúa de acuerdo con las reglas para el condicional material , y el resultado se muestra debajo de su operador principal. La columna 6 muestra que la fórmula completa se evalúa como verdadera en todos los casos, es decir, que es una tautología. De hecho, su antecedente (columna 2) y su consecuente (columna 10) son incluso equivalentes.
El sorprendente descubrimiento de Frege, del que puede o no haber sido plenamente consciente y que se ha perdido de vista desde el descubrimiento de la paradoja de Russell, fue que la aritmética puede derivarse en un sistema puramente lógico como el de su Begriffsschrift a partir de este principio consistente y solo de él.
