La contradiction d'une déclaration vraie est-elle toujours prouvable?

Question

J'ai eu beaucoup de mal à prouver la contrapositive d'un simple énoncé élémentaire de la théorie des nombres, et plus j'y pense, plus je pense que cela pourrait ne pas être prouvable de cette façon en utilisant des techniques de preuve (que nous acceptons comme valides). Je sais qu'il y a de vraies déclarations qui ne sont pas prouvables, mais je ne sais pas à quel point cela se rapporte à cela. J'ai entendu parler de quelque chose sur les modèles, ou disons, un modèle de théorie des nombres: NT. Y a-t-il des généralisations de types d'énoncés vrais que nous pouvons prouver dans la théorie des nombres de certaines manières mais pas dans d'autres?

Answer 1

Comme d'autres l'ont noté dans les commentaires, l'utilisation de l'adjectif true ouvre une boîte de vers: la vérité a une définition technique dans la sémantique, et elle se heurte presque certainement à la question que vous voulez poser. En particulier, les choses vraies n'ont pas besoin d'être prouvables, point final.

Au lieu de cela, laissez-moi poser une question de théorie de la preuve qui (je pense) se rapproche de celle que vous avez l'intention de poser:

J'ai réussi à prouver une implication $A \rightarrow B$, mais je ne pourrais le faire qu'en prenant le contrapositif $\neg B \rightarrow \neg A$, et le prouvant. Dans une telle situation, puis-je toujours trouver une preuve plus directe de$A \rightarrow B$ cela n'implique pas de prendre des contrapositifs?

Sur la base de votre question, votre instinct vous dit que ce n'est pas nécessairement le cas et votre instinct est correct. Parfois, chaque preuve d'une déclaration vous oblige à prendre des contrapositifs.

Avant d'expliquer pourquoi, je dois expliquer certaines choses concernant la terminologie de la théorie de la preuve. Pour enquêter rigoureusement sur les preuves, nous devons d'abord définir ce que nous entendons par preuve. Il existe une grande variété de définitions de ce type, appelées systèmes de preuve (systèmes déductifs).

Certains systèmes de preuve définissent des formes de raisonnement obscures ou extrêmement contraintes, telles que le raisonnement pédagogique, où vous devez donner des exemples explicites avant d'introduire des concepts abstraits; ou raisonnement éthique, où vous devez faire la distinction entre les déclarations autorisées et interdites. Différents systèmes de preuve peuvent prouver différents théorèmes. Mais même deux systèmes de preuve qui prouvent les mêmes théorèmes peuvent différer considérablement l'un de l'autre: un théorème peut avoir plusieurs preuves dans un système, mais une seule preuve dans un autre système. Les théoriciens de la preuve peuvent créer de nouveaux systèmes déductifs à la demande , de la même manière qu'un théoricien des groupes construirait de nouveaux groupes pour illustrer des situations techniques ou pour fournir des (contre) exemples à des conjectures et des questions mathématiques.

Avec ces différences à l'esprit, il devrait être clair que nous devrons réparer un système de preuve à l'avance pour dire quelque chose de sensé. À partir de là, je me concentrerai sur un système de preuve spécifique: la déduction naturelle de Gentzen et Prawitz. La déduction naturelle fournit un substrat rigoureux au type de preuve qui vous intéresse: une preuve mathématique du type qui serait acceptée dans un manuel de mathématiques ordinaire ou un article de journal.

II. Rédiger une introduction approfondie à la déduction naturelle, sans parler de celle qui correspond à une réponse Math.SE, est un défi considérable, à tel point que je n'essaierai même pas. Si vous savez lire et écrire des preuves mathématiques, vous êtes équipé pour comprendre la déduction naturelle. Vous pourrez peut-être comprendre comment cela fonctionne en vous basant uniquement sur ce qui est écrit ci-dessous, mais si vous souhaitez apprendre toutes les règles et les comprendre plus en profondeur, il existe de nombreux tutoriels, vidéos YouTube et des myriades de manuels sur le sujet. Je recommande personnellement les trois premiers chapitres des Elements of Logical Reasoning de Jan von Plato .

La déduction naturelle a de nombreuses règles d'inférence, toutes familières au mathématicien qui travaille. Ces règles d'inférence vous indiquent comment construire de nouvelles preuves à partir de preuves existantes. Chaque connectif (conjonction$\wedge$, disjonction $\vee$, implication $\rightarrow$, négation $\neg$) et quantificateur (universel $\forall$, existentiel $\exists$) est équipé d'une ou plusieurs règles dites d'introduction et d'une règle d'élimination. Exemples:

1. Si vous avez une preuve de $A$ et vous avez une preuve de $A \rightarrow B$, alors tu as réussi à prouver que $B$ tient (élimination d'implication).
2. Si vous avez une preuve que $A \wedge B$ ($A$ et $B$) tient, alors vous avez réussi à prouver que $B$ tient (élimination de conjonction, à droite).
3. Si vous avez une preuve que $A \wedge B$ tient, alors vous avez réussi à prouver que $A$ tient (élimination de conjonction, à gauche).
4. Si vous avez une preuve que $A$ tient, et vous avez la preuve que $B$ tient, alors vous avez réussi à prouver que $A \wedge B$ tient (introduction de conjonction).
5. Si vous avez une preuve qui commence par "Suppose $A$... "et se termine par" ... donc $B$", alors vous avez réussi à prouver la déclaration conditionnelle $A \rightarrow B$ (introduction d'implication).
6. Si vous avez une preuve qui commence par "Suppose $A$... "et se termine par" qui est une contradiction ", alors vous avez réussi à prouver la négation $\neg A$ (introduction de négation).
7. etc...

Au-delà de ces règles ordinaires, il existe également trois règles spéciales:

1. Si vous avez une preuve que $\neg\neg A$ tient, alors vous avez réussi à prouver que $A$ tient (élimination de la double négation).
2. Vous avez toujours une preuve de $A \vee \neg A$ (loi du milieu exclu).
3. Si vous avez une preuve que $\neg B \rightarrow \neg A$, alors tu as réussi à prouver que $A \rightarrow B$ (preuve par contre-positif).

Si vous ajoutez l'une de ces règles aux règles ordinaires de déduction naturelle, vous pouvez prouver les deux autres. Par exemple, si vous ajoutez la loi du milieu exclu comme règle d'inférence, vous pouvez prouver chaque instance d'élimination de la double négation. Plus important encore pour nous, vous pouvez utiliser la preuve par contre-positif pour prouver chaque instance d'élimination de la double négation. Nous pouvons utiliser cette preuve auxiliaire:

1. Supposer que $\neg A$ tient.
2. Supposer que $\neg\neg A$ tient.
3. De 1 et 2, nous avons une contradiction.
4. De 2-3 nous avons $\neg\neg\neg A$ par introduction de négation.
5. De 1 à 4, nous avons $\neg A \rightarrow \neg\neg\neg A$ par introduction implicite.
6. A partir de 5 nous avons $\neg\neg A \rightarrow A$ par contrapositive.

Maintenant, imaginez que nous ayons une preuve de $\neg\neg A$. Notre preuve auxiliaire nous donne$\neg\neg A \rightarrow A$, donc l'élimination d'implication nous donne une preuve de $A$. Ainsi, comme je l'ai affirmé, vous pouvez utiliser la règle de preuve par inférence contrapositive, avec les règles ordinaires, pour prouver chaque instance d'élimination de la double négation.

Le système de preuve de déduction naturelle qui a toutes les règles d'introduction et d'élimination ordinaires, mais aucune des trois règles spéciales, est appelé déduction naturelle intuitionniste ou constructive. Nous appelons parfois le système qui comprend également l'une des règles spéciales (le plus souvent l'élimination de la double négation, pour des raisons techniques) Déduction naturelle classique . C'est un fait bien connu que$\neg\neg A \rightarrow A$n'est pas prouvable dans la déduction naturelle intuitionniste. Donc dans un sens très réel,$\neg\neg A \rightarrow A$ n'est pas prouvable sans prendre des contrapositifs, ou l'une des deux autres règles d'inférence qui lui équivalent.

III. Si vous mettez les axiomes de la théorie élémentaire des nombres dans un système de preuve par déduction naturelle intuitionniste, vous vous retrouvez avec une théorie mathématique appelée Heyting Arithmetic . Gardez à l'esprit: ce n'est pas parce qu'un principe logique général n'est pas prouvable sans prendre des contrapositifs qu'il ne s'ensuit pas qu'aucune instance n'est prouvable sans prendre des contrapositifs! Par exemple, l'arithmétique de Heyting prouve$\neg\neg t = 0 \rightarrow t = 0$ pour n'importe quel nombre $t$.

Cependant, Heyting Arithmetic diffère de l'arithmétique élémentaire habituelle (Peano) de plusieurs manières. En particulier, Heyting Arithmetic ne prouve pas ce qui suit:

Pour chaque polynôme $P$ avec des coefficients entiers, il y a des entiers $n$ tel que pour tous $x$, $|P(n)| \leq |P(x)|$. [2]

Cela fournit une réponse à l'une des formulations les plus faibles de votre question: chaque preuve du théorème ci-dessus vous oblige à prendre des contrapositifs (ou à utiliser un principe équivalent) quelque part dans sa preuve .

Je n'entrerai pas dans les détails, mais un résultat de la théorie de la preuve de De Jongh [1] nous permet de répondre à une formulation plus forte: nous pouvons également obtenir des énoncés explicites de la théorie des nombres $A,B$ telle que l'arithmétique de Heyting prouve l'implication $\neg B \rightarrow \neg A$, mais pas l'implication $A \rightarrow B$.

Vous pourriez poser une question encore plus forte: trouver des énoncés explicites de la théorie des nombres $A,B$ telle que toute preuve (suffisamment normalisée) de $A \rightarrow B$ contient une preuve de $\neg B \rightarrow \neg A$lui-même comme sous-épreuve. Bonne chance avec ça: ça semble très très difficile :)

---

[1] De Jongh, DHJ: La maximalité du calcul intuitionniste des prédicats par rapport à l'arithmétique de Heyting, tech. rep., Réunion de l'Association for Symbolic Logic, Manchester UK, 1969

[2] Friedman, H.: Arithmétique classique / constructive , liste de diffusion FOM, 18 mars 2006