Vision platonicienne des mathématiques ?

Et de toute façon la phrase que tu as misé entre guillemets avant d'écrire "est une injure",

Elle existe bien

Elle est bien célèbre

C'est bien un théorème de maths

Et tous les logiciens la comprennent de la même manière et j'ajouterai même que tous les mathématiciens la comprennent de la même manière

c'est d'ailleurs la raison pour laquelle j'ai entamé cette discussion avec toi puisque tu sembles faire figure d'exception en considérant cette phrase comme disant

Si pas de preuve standard de non CG pas dentier du tout ni standard ni non standard voire même très infini témoin de non CG

Qui est fausse et ça tu as raison de le dire mais qui est surtout une interprétation complètement asymétrique et pas la bonne de la phrase célèbre

[EDIT : J'avais posté ce message dans un autre fil, mais il semble avoir été incorporé à celui-ci. La première phrase n'a donc plus de sens, alors je la barre.]

Suite à un post parallèle où une vive discussion a lieu, et en me disant que ledit post risque de fermer et qu'en posant ma question après, je risque de me faire gronder, j'en profite.

Je ne suis pas au point avec cette affaire de "si Goldbach n'est pas réfutable, alors elle est vraie", alors je voudrais essayer de tout décortiquer.

1) Goldbach est l'énoncé : $\forall n \in 2\mathbb{N}\cap [3,+\infty[,\ \exists p,q \in \mathcal{P},\quad n = p+q$.

2) Soit $G(n)$ l'énoncé à une variable libre $n$ suivant : "$\exists p,q \in \mathcal{P},\quad n = p+q$". Alors il y a un algorithme (ici, il est évident !) dont on peut démontrer qu'il termine sur toute entrée, qui prend en argument un entier $n$ et qui, au terme de son exécution, a écrit une démonstration de $G(n)$ ou une démonstration de $\neg G(n)$.

3) Je pense que pour cette histoire, la conjecture de Golbach peut être remplacée par tout énoncé de la forme $\forall n, \ G(n)$ où $G$ vérifie la propriété mise en exergue dans 2).

4) Soit donc $G(n)$ un énoncé à une variable libre $n$ tel qu'il existe un algorithme dont on peut démontrer qu'il termine sur toute entrée, qui prend en argument un entier $n$ et qui, au terme de son exécution, a écrit une démonstration de $G(n)$ ou une démonstration de $\neg G(n)$).

5) Supposons que $\neg (\forall n,\ G(n))$ n'est pas démontrable. Alors, pour tout $n \in \mathbb{N}$, $G(n)$ est démontrable. En effet : soit $n \in \mathbb{N}$. L'algorithme, lancé sur $n$, termine. S'il a écrit une démonstration de $\neg G(n)$, alors on en tire une démonstration de $\exists n, \neg G(n)$, et donc on en tire une démonstration de $\neg (\forall n,\ G(n))$, ce qui entre en contradiction avec l'hypothèse. Et donc, c'est que l'algorithme a écrit une démonstration de $G(n)$.

----

J'ai bon ? Qu'est-ce que c'est que cette histoire de modèles premiers ?

@Médiat, dans le cadre de l'arithmétique, un (le ?) modèle premier, c'est N, le modèle standard ?

OK, merci Martial.

@Christophe : d'accord avec toi. Je n'avais jamais envisagé qu'on puisse parler de "modèle premier" dans ce cadre. Mais au final, la terminologie proposée par Médiat tient la route.