Théorème de Frege - Frege's theorem

En métalogie et métamathématique , le théorème de Frege est un métathéorème qui déclare que les axiomes de l' arithmétique de Peano peuvent être dérivés en logique du second ordre du principe de Hume . Il a d'abord été prouvé, de manière informelle, par Gottlob Frege dans son 1884 Die Grundlagen der Arithmetik ( Les fondements de l'arithmétique ) et plus formellement prouvé dans son 1893 Grundgesetze der Arithmetik I ( Lois fondamentales de l'arithmétique I). Le théorème a été redécouvert par Crispin Wright au début des années 1980 et a depuis fait l'objet de travaux importants. Il est au cœur de la philosophie des mathématiques connue sous le nom de néo-logicisme (du moins de la variété Scottish School ).

Aperçu

Dans The Foundations of Arithmetic (1884), et plus tard, dans Basic Laws of Arithmetic (vol. 1, 1893; vol. 2, 1903), Frege a tenté de dériver toutes les lois de l'arithmétique à partir d'axiomes qu'il affirmait comme logiques (voir logicisme ). La plupart de ces axiomes ont été repris de son Begriffsschrift ; le seul principe vraiment nouveau était celui qu'il appelait la Loi fondamentale V (maintenant connue sous le nom de schéma axiome de la compréhension illimitée ): la "plage de valeurs" de la fonction f ( x ) est la même que la "plage de valeurs" du fonction g ( x ) si et seulement si ∀ x [ f ( x ) = g ( x )]. Cependant, non seulement la Loi fondamentale V n'a pas été une proposition logique, mais le système qui en a résulté s'est avéré incohérent, parce qu'il était soumis au paradoxe de Russell .

L'incohérence dans le Grundgesetze de Frege éclipsa la réalisation de Frege: selon Edward Zalta , le Grundgesetze «contient toutes les étapes essentielles d'une preuve valide (en logique du second ordre ) des propositions fondamentales de l'arithmétique à partir d'un seul principe cohérent». Cette réalisation est devenue connue sous le nom de théorème de Frege.

Théorème de Frege en logique propositionnelle

( P → ( Q → R )) → (( P → Q ) → ( P → R ))
Non Tique verteOui Non ✓ Non Tique verteOui ✗ ✓ ✗ Tique verteOui ✗ ✓ ✗
Non Tique verteOui Non ✓ Oui Tique verteOui ✗ ✓ ✗ Tique verteOui ✗ ✓ ✓
Non Tique verteOui Oui ✗ Non Tique verteOui ✗ ✓ ✓ Tique verteOui ✗ ✓ ✗
Non Tique verteOui Oui ✓ Oui Tique verteOui ✗ ✓ ✓ Tique verteOui ✗ ✓ ✓
Oui Tique verteOui Non ✓ Non Tique verteOui ✓ ✗ ✗ Tique verteOui ✓ ✗ ✗
Oui Tique verteOui Non ✓ Oui Tique verteOui ✓ ✗ ✗ Tique verteOui ✓ ✓ ✓
Oui X rougeN Oui ✗ Non Tique verteOui ✓ ✓ ✓ X rougeN ✓ ✗ ✗
Oui Tique verteOui Oui ✓ Oui Tique verteOui ✓ ✓ ✓ Tique verteOui ✓ ✓ ✓
1 2 3 4 5 6 7 8 9 dix 11 12 13

En logique propositionnelle , les théorèmes de Frege se réfèrent à cette tautologie :

( P → ( Q → R )) → (( P → Q ) → ( P → R ))

Le théorème tient déjà dans l'une des logiques les plus faibles imaginables, le calcul implicatif constructif . La preuve sous l' interprétation Brouwer-Heyting-Kolmogorov lit . En mots: «Soit f une raison pour laquelle P implique que Q implique R. Et soit g désigne une raison pour laquelle P implique Q. Alors étant donné un f , puis étant donné un g , puis étant donné une raison p pour P , nous savons que les deux Q est vrai par g et que Q implique que R est vrai par f . Donc R est vrai. "

La table de vérité à droite donne une preuve sémantique. Pour toutes les affectations possibles de faux ( ✗ ) ou vrai ( ✓ ) à P , Q et R (colonnes 1, 3, 5), chaque sous-formule est évaluée selon les règles du conditionnel matériel , le résultat étant affiché sous son opérateur principal . La colonne 6 montre que l'ensemble de la formule est évalué à vrai dans tous les cas, c'est-à-dire qu'il s'agit d'une tautologie. En fait, son antécédent (colonne 2) et son conséquent (colonne 10) sont même équivalents.

Remarques

Les références