Propositions indécidables

[Anonyme]

Je me posais une question. Prenons un système axiomatique A et une
proposition indécidable P1. P1 et nonP1 ne contredisent pas A. On peut
donc imaginer de choisir arbitrairement P1 comme vraie et définir un
nouveau système axiomatique A u {P1} qui n'est pas contradictoire.
Le nouveau système axiomatique possède à nouveau des propositions
indécidables. Et puis on en rajoute au fur et à mesure. Pourquoi ne
peut-on pas arriver de cette façon à un système avec une infinité
d'axiomes qui n'ait plus de propositions indécidables et qui soit
cependant consistant?

Je dois avouer que la lecture de la démo du théorème de Gödel m'est
restée très obscure, donc je dois passer à côté de quelque chose, mais
quoi?

--
Nicolas

[Anonyme]

Nicolas Le Roux , dans le message (fr.education.entraide.maths:51496), a
écrit :
> Je me posais une question. Prenons un système axiomatique A et une
> proposition indécidable P1. P1 et nonP1 ne contredisent pas A. On peut
> donc imaginer de choisir arbitrairement P1 comme vraie et définir un
> nouveau système axiomatique A u {P1} qui n'est pas contradictoire.
> Le nouveau système axiomatique possède à nouveau des propositions
> indécidables. Et puis on en rajoute au fur et à mesure. Pourquoi ne
> peut-on pas arriver de cette façon à un système avec une infinité
> d'axiomes qui n'ait plus de propositions indécidables et qui soit
> cependant consistant?

Bah, si on peut.

Godel dit qu'il y a des indecidables quand le systeme d'axiomes est
recursif (ie un ordinateur peut reconnaitre si une proposition est un
axiome ou n'en est pas un). Ce qui se passe, c'est qu'a partir d'un
moment, il n'est plus recursif.

Une grande question (que l'on s'etait posee entre copains a l'ENS il
y a quelques annees) etait de savoir a partir de quel ordinal le systeme
ne devenait plus recursif. Je crois que l'on n'avait pas reussi a parvenir
a une reponse precise.

[Anonyme]

On Fri, 28 Nov 2003 22:06:29 +0000 (UTC),
Nicolas Le Roux wrote:
>Je me posais une question. Prenons un système axiomatique A et une
>proposition indécidable P1. P1 et nonP1 ne contredisent pas A. On peut
>donc imaginer de choisir arbitrairement P1 comme vraie et définir un
>nouveau système axiomatique A u {P1} qui n'est pas contradictoire.
>Le nouveau système axiomatique possède à nouveau des propositions
>indécidables. Et puis on en rajoute au fur et à mesure. Pourquoi ne
>peut-on pas arriver de cette façon à un système avec une infinité
>d'axiomes qui n'ait plus de propositions indécidables et qui soit
>cependant consistant?
>
>Je dois avouer que la lecture de la démo du théorème de Gödel m'est
>restée très obscure, donc je dois passer à côté de quelque chose, mais
>quoi?
Pour completer ce que dit Xavier, il n'y a pas besoin de procéder
comme tu le dis en ajoutant des axiomes au fur et à mesure.
Il suffit de prendre un modèle de ta théorie, puis de prendre comme
nouvelle théorie toutes les formules vraies dans ce modèle.
Alors c'est consistant et on n'a pas de propositions indécidables.

--
Frédéric

[Anonyme]

Le Sat, 29 Nov 2003 02:21:26 +0000 (UTC),
Frederic grava à la saucisse et au marteau:

> Pour completer ce que dit Xavier, il n'y a pas besoin de procéder
> comme tu le dis en ajoutant des axiomes au fur et à mesure.
> Il suffit de prendre un modèle de ta théorie, puis de prendre comme
> nouvelle théorie toutes les formules vraies dans ce modèle.
> Alors c'est consistant et on n'a pas de propositions indécidables.

J'effectuais un processus itératif parce que je n'étais pas sûr
qu'ajouter des axiomes ne modifie pas l'ensemble des propositions
indécidables.

--
Nicolas

[Anonyme]

On Sat, 29 Nov 2003 02:26:42 +0000 (UTC),
Nicolas Le Roux wrote:
>Le Sat, 29 Nov 2003 02:21:26 +0000 (UTC),
>Frederic grava à la saucisse et au marteau:
>[color=green]
>> Pour completer ce que dit Xavier, il n'y a pas besoin de procéder
>> comme tu le dis en ajoutant des axiomes au fur et à mesure.
>> Il suffit de prendre un modèle de ta théorie, puis de prendre comme
>> nouvelle théorie toutes les formules vraies dans ce modèle.
>> Alors c'est consistant et on n'a pas de propositions indécidables.
>
>J'effectuais un processus itératif parce que je n'étais pas sûr
>qu'ajouter des axiomes ne modifie pas l'ensemble des propositions
>indécidables.[/color]
??? Ajouter un axiome non redondant supprime au moins une proposition
indécidable : lui-même (et une floppée d'autres en général...)

--
Frédéric

[Anonyme]

Le Sat, 29 Nov 2003 03:33:39 +0000 (UTC),
Frederic grava à la saucisse et au marteau:
[color=green]
> >J'effectuais un processus itératif parce que je n'étais pas sûr
> >qu'ajouter des axiomes ne modifie pas l'ensemble des propositions
> >indécidables.
> ??? Ajouter un axiome non redondant supprime au moins une proposition
> indécidable : lui-même (et une floppée d'autres en général...)[/color]

Quand je l'ai écrit, je comprenais pas pourquoi j'avais pensé ça à
l'époque, donc dans le doute, je l'ai écrit quand même. Mais en effet,
je suis totalement d'accord avec toi

--
Nicolas

[Anonyme]

Nicolas Le Roux writes:

> Je me posais une question. Prenons un système axiomatique A et une
> proposition indécidable P1. P1 et nonP1 ne contredisent pas A. On peut
> donc imaginer de choisir arbitrairement P1 comme vraie

En pratique, si P1 a une sémantique claire (c'est la cas pour les
propositions fournies par Gödel) le choix ne sera pas arbitraire :
ainsi, on dédaignera sans doute un système cohérent qui prouve sa
propre non-cohérence.

> et définir un
> nouveau système axiomatique A u {P1} qui n'est pas contradictoire.
> Le nouveau système axiomatique possède à nouveau des propositions
> indécidables. Et puis on en rajoute au fur et à mesure. Pourquoi ne
> peut-on pas arriver de cette façon à un système avec une infinité
> d'axiomes qui n'ait plus de propositions indécidables et qui soit
> cependant consistant?

Si tu pousses ta récurrence très très loin c'est peut-être possible,
mais ça sera pas avant le moment où ton système d'axiomes n'est plus
récursif --- sinon, Gödel s'applique toujours.

Ça n'a donc pas grand intérêt.

[Anonyme]

caruso@clipper.ens.fr (Xavier Caruso) writes:

> Une grande question (que l'on s'etait posee entre copains a l'ENS il
> y a quelques annees) etait de savoir a partir de quel ordinal le systeme
> ne devenait plus recursif. Je crois que l'on n'avait pas reussi a parvenir
> a une reponse precise.

Ça me semble lié à la question suivante qui hante mes nuits : « que
sait-on du plus petit ordinal non récursif ? »

Par définition, pas grand chose. Certes.

[Anonyme]

beal@clipper.ens.fr (Frederic) writes:

> Pour completer ce que dit Xavier, il n'y a pas besoin de procéder
> comme tu le dis en ajoutant des axiomes au fur et à mesure.
> Il suffit de prendre un modèle de ta théorie, puis de prendre comme
> nouvelle théorie toutes les formules vraies dans ce modèle.

Encore faut-il savoir ce que veut dire « prendre un modèle de la
théorie ». Pour l'arithmétique je veux bien (mais y a des problèmes
pour être sûr de la sémantique des formules qui alternent trop de
quantificateurs), pour la théorie des ensembles c'est une autre paire
de manches...

> Alors c'est consistant et on n'a pas de propositions indécidables.
>
> --
> Frédéric

[Anonyme]

On 01 Dec 2003 10:38:43 +0100, un.gabacho.sans.pourrier@free.fr
wrote:
>beal@clipper.ens.fr (Frederic) writes:
>[color=green]
>> Pour completer ce que dit Xavier, il n'y a pas besoin de procéder
>> comme tu le dis en ajoutant des axiomes au fur et à mesure.
>> Il suffit de prendre un modèle de ta théorie, puis de prendre comme
>> nouvelle théorie toutes les formules vraies dans ce modèle.
>
>Encore faut-il savoir ce que veut dire « prendre un modèle de la
>théorie ». Pour l'arithmétique je veux bien (mais y a des problèmes
>pour être sûr de la sémantique des formules qui alternent trop de
>quantificateurs), pour la théorie des ensembles c'est une autre paire
>de manches...[/color]

Non, il n'y a aucun problème. Une théorie est consistante si et
seulement si elle admet un modèle. Donc le modèle nous est fourni,
on n'a pas à se préoccuper du sens de notre théorie. Je ne
prétends pas que la theorie des ensembles est consistante, mais si
elle l'est alors on peut construire une extension de ZF dans laquelle
il n'y a pas d'indécidables, et qui soit consistante.

--
Frédéric

[Anonyme]

beal@clipper.ens.fr (Frederic) writes:

> On 01 Dec 2003 10:38:43 +0100, un.gabacho.sans.pourrier@free.fr
> wrote:[color=green]
> >beal@clipper.ens.fr (Frederic) writes:
> >[color=darkred]
> >> Pour completer ce que dit Xavier, il n'y a pas besoin de procéder
> >> comme tu le dis en ajoutant des axiomes au fur et à mesure.
> >> Il suffit de prendre un modèle de ta théorie, puis de prendre comme
> >> nouvelle théorie toutes les formules vraies dans ce modèle.
> >
> >Encore faut-il savoir ce que veut dire « prendre un modèle de la
> >théorie ». Pour l'arithmétique je veux bien (mais y a des problèmes
> >pour être sûr de la sémantique des formules qui alternent trop de
> >quantificateurs), pour la théorie des ensembles c'est une autre paire
> >de manches...[/color]
>
> Non, il n'y a aucun problème.[/color]

Ça dépend sans doute de ta position épistémologique. Pour moi, il y a
un problème.

> Une théorie est consistante si et seulement si elle admet un modèle.

Ça se démontre en théorie des ensembles, ça.(¹)

> Donc le modèle nous est fourni,

Par des ultraproduits ? vache de fourniture. En gros il faut avoir un
modèle de ZFC et *dedans* on a un modèle de notre théorie du 1er ordre.

C'est vrai ; mais à mes yeux le prérequis « il faut avoir un modèle de
ZFC » pose un problème. J'admets que tu penses le contraire, hein, on
est sur des questions de considérations personnelles...

> on n'a pas à se préoccuper du sens de notre théorie. Je ne
> prétends pas que la theorie des ensembles est consistante, mais si
> elle l'est alors on peut construire une extension de ZF dans laquelle
> il n'y a pas d'indécidables, et qui soit consistante.

« construire » ? Pour moi, construire, c'est donner quelque chose
de récursif. Alors pas dans ce sens, non.

Prouver dans ZF l'existence d'une telle chose ? Oui, sans aucun doute,
tu as raison.




(¹) On peut le démontrer par des moyens plus élémentaires, c'est pas
vraiment écrit à plat nulle part à ma connaissance, mais en gros je
prétends et ça ne surprendra personne qu'il suffit du lemme de König
faible --- ce qui est raisonnable mais... non constructif, toutefois.
Le problème subsiste.

[Anonyme]

un.gabacho.sans.pourrier@free.fr, dans le message
(fr.education.entraide.maths:51544), a écrit :
> Ça me semble lié à la question suivante qui hante mes nuits : « que
> sait-on du plus petit ordinal non récursif ? »

Ah ben, pour le coup :

http://boumbo.salle-s.org/xavier/recursif.ps.gz
http://boumbo.salle-s.org/xavier/recursif.pdf

--
Xavier, qui ne sais pas si ça donne une réponse claire, mais bon.

[Anonyme]

caruso@clipper.ens.fr (Xavier Caruso) writes:

> un.gabacho.sans.pourrier@free.fr, dans le message
> (fr.education.entraide.maths:51544), a écrit :[color=green]
> > Ça me semble lié à la question suivante qui hante mes nuits : « que
> > sait-on du plus petit ordinal non récursif ? »
>
> Ah ben, pour le coup :
>
> http://boumbo.salle-s.org/xavier/recursif.ps.gz
> http://boumbo.salle-s.org/xavier/recursif.pdf
>
> --
> Xavier, qui ne sais pas si ça donne une réponse claire, mais bon.[/color]

Merci, ça a l'air très bien écrit. Je le garde sous le coude.
Cependant je crois que je connais à peu près bien tout ce qu'il y a
là-dedans. Ça ne suffit pas à mon appétit...

Mais bon, pour l'instant, mon activité a d'autres urgences. Tu me
comprends... :-/

[Anonyme]

On 01 Dec 2003 11:03:55 +0100, un.gabacho.sans.pourrier@free.fr
wrote:[color=green][color=darkred]
>> >Encore faut-il savoir ce que veut dire « prendre un modèle de la
>> >théorie ». Pour l'arithmétique je veux bien (mais y a des problèmes
>> >pour être sûr de la sémantique des formules qui alternent trop de
>> >quantificateurs), pour la théorie des ensembles c'est une autre paire
>> >de manches...
>>
>> Non, il n'y a aucun problème.[/color]
>
>Ça dépend sans doute de ta position épistémologique. Pour moi, il y a
>un problème.
>
>> Une théorie est consistante si et seulement si elle admet un modèle.
>
>Ça se démontre en théorie des ensembles, ça.(¹)
>
>> Donc le modèle nous est fourni,
>
>Par des ultraproduits ? vache de fourniture. En gros il faut avoir un
>modèle de ZFC et *dedans* on a un modèle de notre théorie du 1er ordre.
>
>C'est vrai ; mais à mes yeux le prérequis « il faut avoir un modèle de
>ZFC » pose un problème. J'admets que tu penses le contraire, hein, on
>est sur des questions de considérations personnelles...[/color]
Non non, mais comme bien des gens, je considères que si ZFC
n'a pas de modèle on est mal barés. Donc je suppose qu'il y en a
un, et si un jour on me dit que ce n'est pas le cas, et bien,
des gens sympathiques me trouveront d'autres axiomes avec lesquels
mes constructions seront toujours valides...
[color=green]
>> on n'a pas à se préoccuper du sens de notre théorie. Je ne
>> prétends pas que la theorie des ensembles est consistante, mais si
>> elle l'est alors on peut construire une extension de ZF dans laquelle
>> il n'y a pas d'indécidables, et qui soit consistante.
>
>« construire » ? Pour moi, construire, c'est donner quelque chose
>de récursif. Alors pas dans ce sens, non.[/color]
Argh ! Oui, j'aurais du dire « prouver l'existence de ». M'enfin,
hein, même si je sais qu'il y a une différence, dans un usage
scientifique courant, en ce qui me concerne, une construction
faisant appel à l'axiome du choix « ou » à des ultraproduits est une
construction.

>Prouver dans ZF l'existence d'une telle chose ? Oui, sans aucun doute,
>tu as raison.
Ah, la voix de la raison

>
>(¹) On peut le démontrer par des moyens plus élémentaires, c'est pas
>vraiment écrit à plat nulle part à ma connaissance, mais en gros je
>prétends et ça ne surprendra personne qu'il suffit du lemme de König
>faible --- ce qui est raisonnable mais... non constructif, toutefois.
>Le problème subsiste.
Problème ?
let troll =
"qui fait des mathématiques constructives ? cela sert-il ? on est
heureux avec nos mathématiques non constructives, non ?"
in (fun x -> 0) troll;;

--
Frédéric, qui aime bien les raisonnements par l'absurde, le lemme de
Zorn, ...

[Anonyme]

beal@clipper.ens.fr (Frederic) writes:

> Non non, mais comme bien des gens, je considères que si ZFC
> n'a pas de modèle on est mal barés.

ZFC n'a pas à ce jour de modèle décrit de manière élémentaire. En fait
le meilleur moyen de décrire des modèles de ZFC c'est de se placer
dans ZFC. Arf.

> Donc je suppose qu'il y en a
> un, et si un jour on me dit que ce n'est pas le cas, et bien,
> des gens sympathiques me trouveront d'autres axiomes avec lesquels
> mes constructions seront toujours valides...

Ce n'est pas la seule position possible. J'ai déjà posté ces deux url
pas mal de fois :

http://moire4.u-strasbg.fr/souv/Int84.htm
http://peccatte.karefil.com/PhiMathsTextes/MathsConstructives.html

> "qui fait des mathématiques constructives ? cela sert-il ? on est
> heureux avec nos mathématiques non constructives, non ?"

Chacun sa voie.

> Frédéric, qui aime bien les raisonnements par l'absurde, le lemme de
> Zorn, ...

J'aime bien aussi. Il serait sot de ma part de nier l'esthétique qu'il
peut y avoir à utiliser ces méthodes.