Consistance et intuitionnisme
Bonjour,
dans mon dictionnaire des mathématiques de Bouvier et al., à la rubrique "intuitionnisme", j'ai eu la surprise de lire ceci :
" [...] Cependant, A. Kolomogorov et K. Gödel ont démontré que la consistance de l'arithmétique intuitionniste est équivalente à celle de l'arithmétique classique".
Connaissez-vous cette démonstration et pouvez-vous me dire où je puis la trouver ?
J'imagine qu'elle est rédigée dans la logique intuitionniste. Si tel est le cas, soit l'arithmétique intuitionniste est cohérente et le théorème montre que la classique l'est aussi, soit elle ne l'est pas, et la classique non plus, puisque plus forte.
(Si elle était rédigée en logique classique, l'arithmétique classique pourrait être contradictoire sans que l'intuitionniste le soit).
Cela m'inspire une seconde question. Bien que cela soit extrêmement improbable, l'arithmétique classique pourrait être contradictoire. Ce théorème signifie-t-il alors que le risque que l'intuitionniste le soit aussi n'est pas moindre ?
Cela me semble étrange.
dans mon dictionnaire des mathématiques de Bouvier et al., à la rubrique "intuitionnisme", j'ai eu la surprise de lire ceci :
" [...] Cependant, A. Kolomogorov et K. Gödel ont démontré que la consistance de l'arithmétique intuitionniste est équivalente à celle de l'arithmétique classique".
Connaissez-vous cette démonstration et pouvez-vous me dire où je puis la trouver ?
J'imagine qu'elle est rédigée dans la logique intuitionniste. Si tel est le cas, soit l'arithmétique intuitionniste est cohérente et le théorème montre que la classique l'est aussi, soit elle ne l'est pas, et la classique non plus, puisque plus forte.
(Si elle était rédigée en logique classique, l'arithmétique classique pourrait être contradictoire sans que l'intuitionniste le soit).
Cela m'inspire une seconde question. Bien que cela soit extrêmement improbable, l'arithmétique classique pourrait être contradictoire. Ce théorème signifie-t-il alors que le risque que l'intuitionniste le soit aussi n'est pas moindre ?
Cela me semble étrange.
Réponses
-
Bonjour,
Vous pouvez regarder la"non-non traduction" de GödelIl ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse -
Merci Médiat. Et pour ma seconde question ?
-
@GG idem pour ta seconde question. L'arithmétique intuitionniste "contient" la classique au sens où tout ce qui est écrit avec implique, et ainsi que quelque soit est indifféremment prouvable classiquement ou intuitionnistiquement.
L'intuitionniste ENRICHIT la classique en ajoutant "il existe" et "ou" qui ne sont pas gérables intuitionnistiquement comme équivalents à des abréviations faites à partir des autres alors que classiquement si si.
En résumé, en exagérant à peine on pourrait surtout plus craindre une contradiction de l'intuitionniste que de la classique (vue de l'esprit) sauf qu'effectivement, cet enrichissement est prouvablement inoffensif de ce point de vue.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Les énoncés suivants sont des théorèmes intuitionnistes ($T$ étant un type/une sorte et $\Phi,A,B$ des énoncés).$(\neg \neg \perp) \to \perp$$((\neg \neg B ) \to B ) \to (\neg \neg (A \to B ) \to (A \to B ))$$ ((\neg \neg A) \to A ) \to ((\neg \neg B ) \to B ) \to (\neg \neg (A \wedge B ) \to (A \wedge B ))$$(\forall x:T, ((\neg \neg \Phi) \to \Phi)) \to (\neg \neg (\forall x:T, \Phi) \to \forall x:T, \Phi)$.Donc par induction sur la taille des formules envisagées, si une théorie prouve (intuitionnistiquement) $(\neg \neg P) \to P$ (*)pour toutes ses formules atomiques $P$, elle entraîne (intuitionnistiquement) le tiers exclu pour toutes ses formules écrites avec $\to,\wedge,\forall,\perp$.Une condition suffisante pour (*) est d'avoir une preuve de $P \vee \neg P$ (on dit que $P$ est décidable).C'est le cas de l'arithmétique où les seules formules atomiques sont des égalités ou des inégalités et sont décidables (algorithmiquement).
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Merci CC et Foys. CC, je ne comprends pas ta remarque. Tous les théorèmes de l'intuitionniste étant des théorèmes de la classique, comment pourrait-on craindre la contradiction de la première plus que celle la seconde ?
-
Non c'était une vue de l'esprit. Comme dit, c'est équivalent.
Mais la classique in fine est INCLUSE dans l'intuitioniste si on restreint le langage. Ce n'est pas la vision habituelle certes, mais je répondais à TA DEUXIEME question de façon SPÉCIFIQUE.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.1K Toutes les catégories
- 7 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 52 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 62 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 312 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 772 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 25
+16 Invités