Consistance et intuitionnisme — Les-mathematiques.net The most powerful custom community solution in the world

Consistance et intuitionnisme

GGGG
Modifié (December 2021) dans Fondements et Logique
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.

Réponses

  • Bonjour,

    Vous pouvez regarder la"non-non traduction" de Gödel
    504, c'est trop !
  • 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
  • Modifié (December 2021)
    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).

  • GGGG
    Modifié (December 2021)
    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.
Success message!