title: Théorème de Frege
text: # Théorème de Frege
  
  En métalogique et en métamathématique, le théorème de Frege est un métathéorème qui affirme que les axiomes de l'arithmétique de Peano sont dérivables en logique du second ordre à partir du principe de Hume. Il a d'abord été prouvé, de manière informelle, par Gottlob Frege dans son Die Grundlagen der Arithmetik (Les Fondements de l'arithmétique), publié en 1884, et prouvé plus formellement dans ses Grundgesetze der Arithmetik (Lois fondamentales de l'arithmétique), publiées en deux volumes, en 1893 et 1903. Ce 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 connues sous le nom néo-logicisme.
  
  ## Théorème de Frege en logique propositionnelle
  
  En logique propositionnelle, Le théorème de Frege se réfère à cette tautologie :
  
      (P → (Q→R)) → ((P→Q) → (P→R))
  
  La table de vérité à droite donne une preuve. Pour toutes les attributions possibles de faux (✗) ou vrai (✓) à P, Q, et R (colonnes 1, 3, 5), chaque sous-formule est évaluée selon les règles de l'implication, le résultat étant présenté ci-dessous son opérateur principal. La colonne 6 indique que la formule entière est évaluée vrai, peu importe les valeurs de vérité attribuées, celle-ci est alors une tautologie. En effet, son antécédent (colonne 2) et son conséquent (colonne 10) sont équivalents.
  
  