Démontrer que racine de 2 n'est pas rationnel

christophe c · September 2020

Pardon GG, je me connecte peu (et la canicule n'arrange rien, je suis tout le temps dehors ou sur twitter ou insta, chasse une addiction, une autre prend la place)

En intuitionnisme arithmétique:

1/ Il est facile de prouver par récurrence que $\forall a,b: (a=b$ ou $a\neq b)$.

2/ Si pour tout $x: non(non(R(x)))\to R(x)$, alors $non(non(A))\to A$ pour la phrase $A:=\forall xR(x)$.

3/ Si $non(non(B)) \to B$ alors $non(non(A))\to A$ pour la phrase $C\to B$

Conclusion: il y a équivalence entre Peano intuitionniste et Peano classique pour toutes les phrases écrites avec des opérations, le quantificateur $\forall$ et le connecteur "implique".

Je te laisse en exercice de prouver 1-2-3

Et un gros bisous à Mattar que je suis heureux de revoir sur le forum.

GG · September 2020

Merci CC, mais je ne vois pas le rapport avec ma question qui était de démontrer $\forall n (P(n) \vee \neg P(n))$ avec "$n $ $ est $ $ premier$" comme définition de $P(n)$.
La preuve que la réponse n'allait pas de soi est que l'énoncé similaire $\forall n (J(n) \vee \neg J(n))$ avec " $ \forall $ $ k > n $ $ (k $ $ n'est $ $ pas $ $premier \vee k+2 $ $ n'est $ $ pas $ $ premier) $" comme définition de $J(n)$ n'est pas démontrable sauf erreur (puisque l'on ne sait pas à ce jour si les nombres premiers jumeaux sont en nombre fini).

christophe c · September 2020

Tout dépend comment tu écris "être premier". est-ce que tu utilises le quantificateur $\exists$?

Le point essentiel quand tu t'intéresses à ces questions est de définir les choses avec précision car des choses qui étaient classiquement équivalentes ne le sont plus forcément intuitionnistement. Les connecteurs "ou" et $\exists$" sont pathologiques en logique intuitionniste.

Comme les axiomes de Peano ne les contiennent pas, par exemple, tout théorème de la forme
$$
Peano\vdash_{LI} (A\vee

$$ est tel que

$Peano\vdash_{LI} A$ ou $Peano\vdash_{LI} B$.

Or tu vois bien que si tu ne connais pas $n$, tu n'as pas :

$Peano\vdash_{LI} Premier(n)$ ou $Peano\vdash_{LI} non(Premier(n))$.

Donc sans autre précision, te répondre précisément n'est pas possible. Or la présente réponse que je te fais ne peut pas "être intellectuellement honnête" sauf à faire semblant de ne pas te connaitre, donc ne pas capter ce que tu cherches.

christophe c · September 2020

ERRATUM DE MON TÉLÉPHONE.

Je t'ai raconté n'importe quoi à la fin. Bien sûr que si si Peano contient des axiomes avec exists et où :+X

christophe c · September 2020

Et du coup route propriété écrite avec des quantificateurs bornes se comporte de manière classique (même récurrence que pour égal)

Foys · September 2020

On peut écrire toutes les formules en logique classique avec non, implique et pour tous et donc tout théorème classique de
Peano est classiquement équivalent à un théorème intuitionniste avec ces considérations.

Ca se rapproche des traductions comme Kuroda, ou Gentzen-Gödel.

GG · September 2020

Tout dépend comment tu écris "être premier".

Bin, comme je l'ai défini voici trois messages :

$ \neg (n = 1) \wedge \forall k $ $ (k \mid n \Rightarrow (k = 1 \vee k =n)) $

Le point essentiel quand tu t'intéresses à ces questions est de définir les choses avec précision ...

Il me semble que c'est ce que j'ai fait ! :-)
Mais tu peux laisser tomber, Mattar a parfaitement répondu à mon attente !

gai requin · September 2020

$\neg(n=1)\wedge\forall a\forall b\;(n=ab\rightarrow(a=1\vee b=1))$.

GG · September 2020

@gai requin, oui, tu as raison, c'est mieux que de devoir introduire $k \mid n$ par $\exists x $ $ n = kx $ ou bien par $\neg $ $ \forall x $ $ \neg $ $ n = kx $

christophe c · September 2020

@GG pardon je n'avais pas vu ta précision. Mais réponse ne change pas. Quantificateurs bornes => classique = intuitionniste même s'il ya des connecteurs existentiels et des "ou"

dido · October 2020

df écrivait : http://www.les-mathematiques.net/phorum/read.php?3,2089942,2093196#msg-2093196
[Inutile de recopier un message présent sur le forum. Un lien suffit. AD]

Merci pour cette trouvaille ! Par contre, je n'arrive pas à comprendre la signification du triangle à la fin ?