théorème de Gödel

[invite9bf717fa]

Bonjour tout le monde.

Je ne suis qu'un esprit curieux sans grande compétence scientifique. Cela ne va donc pas vous surprendre que le théorème de Gödel me casse la tête.
En revanche, la raison est je le crois inhabituelle puisque je n'ai vu pour l'instant personne en parler.

En fait, ce que j'ai du mal à accepter, c'est que Gödel avait une intention qu'il a intrinsèquement introduit dans son théorème. Je ne rejette pas l'idée d'intention, car au fond tous les scientifiques ont des intentions en émettant des théorèmes. Mais ce qui est différent dans ce théorème c'est qu'il porte en lui même une intention, c'est à dire quelque chose d'a priori humain (avec sans doute quelques grands singes). En effet, il a inventé une formule qui dit d'elle même qu'elle est indémontrable (si je résume très grotesquement). Une telle formule a-t-elle une réelle puissance, scientifiquement parlant ? Car la science décrit des phénomènes déterminés et déterminants, pas de place donc pour l'intention qui touche finalement à l'humain et même au libre arbitre. Peut-on donc vraiment conclure quelque chose de ce théorème ? Autrement dit, peut-on en déduire quelque chose, a-t-il une valeur déterminatrice ?

Merci à tous ceux qui voudront bien avoir la gratuité de me répondre.
-----

[lou_ibmix_xi]

Bonjour.

Je ne comprends pas, qu'entends tu par:

Mais ce qui est différent dans ce théorème c'est qu'il porte en lui même une intention

En ce qui concerne le theoreme de Godel, je pense que tu n'as pas compris ce qu'il disait, car ce theoreme est demontre et est donc vrai c'est du beton, tu peux sans probleme construire quelque chose avec.

[invite9bf717fa]

Ce que je veux dire c'est que j'ai l'impression que ce théorème tient plus de l'idéologie que de la science. Car il ne sert à se prouver lui même et ce qui lui est similaire : par exemple la phrase "tous les Crêtois sont des menteurs, c'est un Crêtois qui le dit". Or il n'y a pas lieu de se demander si la phrase est vraie ou fausse puisque la situation est impossible. En effet, soit ce n'est pas un crêtois qui le dit, soit tous les crêtois ne sont pas des menteurs. Il suffirait d'une machine capable de remettre les questions qu'on lui pose (sorte de conscience) pour qu'elle la déjoue en répondant que la situation exposée est impossible et que la question de la valeur de vérité de la phrase n'a pas lieu d'être. Trouver la valeur de vérité d'une formule (créée artificiellement, avec la volonté de la créer) qui n'en a pas est finalement absurde.

[invite9bf717fa]

rectification : "il ne sert qu'à se prouver lui-même et tout ce qui lui est similaire"

[A voir en vidéo sur Futura]

[invite8ef897e4]

Bonjour,

je crois qu'il te faudrait te replacer dans le contexte historique. Hilbert (le grand) avait une vision mecaniste des mathematiques. Le théorème de Gödel prouve qu'un ordinateur seul ne peut recreer l'oeuvre mathématique. Il existe une part de creation artistique dans l'entreprise mathematique.

En effet, chaque fois que l'on rencontre une proposition vraie, non-démontrable, et importante, il est justifié de construire un pan de mathématique basé sur cette proposition, alors prise comme nouvel axiome (ou postulat). Le théorème de Gödel montre qu'un ordinateur ne pourrait pas réaliser l'importance d'une telle proposition.

Je suis certain que cela a déjà été discuté. C'est typiquement un sujet fleuve...

[invite79d10163]

Bonjour tout le monde.

Je ne suis qu'un esprit curieux sans grande compétence scientifique.

Le theoreme de godel est un des concepts les plus compliqués du point de vue logique. Une vulgarisation de ce concept sera de toute façon tres loin de la vérité et de la profondeur logique de ce theoreme.

[invité576543]

Ce que je veux dire c'est que j'ai l'impression que ce théorème tient plus de l'idéologie que de la science.

Bonjour,

Pour continuer dans le sens de SkyDancer, le théorème de Gödel est un théorème mathématique, portant sur les systèmes formels, qui sont des objets aussi bien mathématisés que les entiers de l'arithmétique ou autre. Il n'est pas plus pas moins de l'idéologie ou de la science que le théorème de Pythagore!

Les discussions philosophiques relatives au théorème de Gödel porte en fait sur le problème plus général du rapport entre systèmes formels et "connaissances" ou "vérités", ce qui peut se voir comme une application d'un modèle proposé par les mathématiques. Malheureusement, la vulgarisation présente souvent le théorème de Gödel hors contexte, et parle peu des systèmes formels...

Cordialement,

[invite9bf717fa]

Alors au final, peut-on en conclure qu'il y a des choses indémontrables en terme de physique, c'est-à-dire dans ce bas monde réel, autres bien sur que les formules absurdes du type "tous les crêtois sont des menteurs, c'est un crêtois qui le dit" ?

[invité576543]

Alors au final, peut-on en conclure qu'il y a des choses indémontrables en terme de physique, c'est-à-dire dans ce bas monde réel, autres bien sur que les formules absurdes du type "tous les crêtois sont des menteurs, c'est un crêtois qui le dit" ?

Le théorème de Gödel dit que pour un système formel suffisamment compliqué, il y a nécessairement des expressions valides mais qui ne peuvent pas, à l'intérieur du système formel, être démontrées vraies ou fausses. C'est une sorte de négation du tiers exclus si on considère comme notion de "vérité" le fait de pouvoir être démontré.

La notion de "démonstration" en physique reste à définir! Le problème philosophique est quelque part dans la question si les "choses en termes de physique" sont réductibles à un système formel ou non. Et même alors, il reste à discuter si la notion de "vérité" comme équivalente à "démontrable dans le système formel" est adaptée...

Une fois de plus le problème n'est pas le théorème de Gödel, mais la relation entre systèmes formels d'un côté et physique, monde réel, vérité de l'autre.


Sinon, la phrase choisie ne reflète pas vraiment le point du théorème de Gödel. Je te propose plutôt "treborliryc ne peut pas accepter que cette phrase est vraie". Tu arriveras à te convaincre qu'il est évident pour tout le monde, sauf toi, que cette phrase est vraie: à mon sens à moi, elle n'est source d'aucune contradiction. Alors que dans ton système de vérité, la phrase ne peut pas être vraie ou fausse sans introduire une contradiction.

L'exemple que tu prends est une simple indétermination pour tout le monde. La nuance est importante, parce que l'exemple que je prends peut clairement avoir (et a!) une valeur de vérité qui a un sens...

Cordialement,

[edpiste]

Contrairement au théorème de Gödel, ta dernière question est, elle, idéologique. Tu veux savoir si le modèle (la logique formelle) permet de répondre à une question concrète (qui échappe précisément à ce système formel).
C'est donc une question de point de vue ou d'intime conviction. La réponse dépend du contexte.
Je te propose l'exemple classique suivant, appelé syllogisme :

"Tous les hommes sont mortels. Tous les grecs sont des hommes. Socrate est un grec donc Socrate est mortel."

On peut formaliser (modéliser) cet énoncé en posant

a="être grec"
b="être un homme"
c="être mortel"

L'énoncé se formalise alors ainsi


Cet énoncé formel est lui toujours vrai et, dans ce cas précis, on peut se dire que la modélisation choisie rend bien compte du problème "réel" (l'énoncé en français est lui aussi toujours vrai).

Reprend la même démarche, en posant cette fois

a="être bon marché"
b="être rare"
c="être cher"

et applique la même formalisation à l'énoncé suivant :
"Tout ce qui est rare est cher. Un cheval bon marché est rare. Donc un cheval bon marché est cher."

Cet énoncé "réel" est absurde : le choix du modèle (le syllogisme) est donc dans ce cas mauvais. C'est comme ça : le langage courant est plein d'ambiguités (voir les notions de signifiant/signifié chez Saussure ou les travaux de Freud et Lacan). Le langage formel lui n'en souffre aucune. C'est donc normal qu'on ne puisse pas faire correspondre l'un à l'autre.

[Médiat]

Bien que d'accord avec mmy à 99%, j'ai quelques réflexions à ajouter :

Le théorème de Gödel dit que pour un système formel suffisamment compliqué, il y a nécessairement des expressions valides mais qui ne peuvent pas, à l'intérieur du système formel, être démontrées vraies ou fausses

Le mot "démontrées" me gène un peu car il laisse imaginer qu'il y a quelqu'un pour faire la démonstration, alors que le théorème de Gödel n'a rien à voir avec les capacités des mathématiciens, mais bien avec la nature intrinsèque des systèmes formels (dans lesquels on peut définir l'arithmétique), le mot correct est "proposition indécidable" (une notion à la fois plus simple et plus complexe (grâce à Gödel) qu'il n'y paraît).

C'est une sorte de négation du tiers exclus si on considère comme notion de "vérité" le fait de pouvoir être démontré.

Cette phrase me fait plus penser à la théorie de la preuve et à la logique intuitionniste qu'à Gödel.

[invité576543]

Bonsoir,

Le mot "démontrées" me gène un peu car il laisse imaginer qu'il y a quelqu'un pour faire la démonstration, alors que le théorème de Gödel n'a rien à voir avec les capacités des mathématiciens, mais bien avec la nature intrinsèque des systèmes formels (dans lesquels on peut définir l'arithmétique), le mot correct est "proposition indécidable" (une notion à la fois plus simple et plus complexe (grâce à Gödel) qu'il n'y paraît).

Tout à fait d'accord du point de vue rigueur. Toute la difficulté est de choisir entre vocabulaire incorrect mais compréhensible par beaucoup, et vocabulaire rigoureux, mais demandant beaucoup d'explications si on ne veut pas s'adresser à une minorité! Employer "indécidable", est mieux, mais maintenant faut le définir en restant à la portée des lecteurs putatifs...

Cordialement,

[Médiat]

Employer "indécidable", est mieux, mais maintenant faut le définir en restant à la portée des lecteurs putatifs...

J'essaye :

Une proposition p est indécidable dans une théorie (supposée consistante) si elle n'est pas conséquence des axiomes de cette théorie, et sa négation non plus. Une conséquence intéressante, c'est que l'on peut compléter la théorie soit avec la proposition p soit avec non p, et obtenir deux extensions consistantes de la théorie de départ.

Un exemple très simple, la théorie des groupes est l'ensemble des propositions qui se déduisent des axiomes définissant les groupes et que tout le monde connaît, dans cette théorie, la commutativité est indécidable (sinon, tous les groupes seraient commutatifs, ou bien à l'opposé, aucun), je peux donc créer deux théories : les groupes abéliens, et les groupes non commutatifs. On a rendu la théorie de départ un peu plus complète en ajoutant p, ou bien en ajoutant non p (mais pas les deux en même temps ). Le théorème de Gödel affirme que l'on peut ajouter tous les axiomes que l'on veut à l'arithmétique, le résultat ne sera toujours pas complet (= il restera des propositions indécidables).

[invitea77054e9]

Salut,

Un exemple très simple, la théorie des groupes est l'ensemble des propositions qui se déduisent des axiomes définissant les groupes et que tout le monde connaît, dans cette théorie, la commutativité est indécidable

Qu'entends-tu par "la commutativité est indécidable"? Est-ce une proposition?

On a rendu la théorie de départ un peu plus complète en ajoutant p, ou bien en ajoutant non p (mais pas les deux en même temps ).

Plus complète dans quel sens?

Merci pour toute réponse.

[invité576543]

Bonjour,

Je ne suis pas trop convaincu que l'exemple soit pertinent. J'ai du mal à voir comment la commutativité peut être une proposition indécidable, simplement parce que je ne vois pas de quelle proposition on parle. Si c'est "tout groupe est commutatif", ou "il existe au moins un groupe commutatif", c'est tout à fait décidable. La théorie des groupes abéliens n'est qu'une sous-partie de la théorie des groupes.

Les exemples classiques sont le 5ème axiome d'Euclide en géométrie, ou l'axiome du choix, ou l'axiome du continu, sf erreur de ma part.

Le premier est le plus simple, puisqu'il amène effectivement à des géométrie différentes. Et la géométrie hyperbolique, par exemple, n'est pas une sous-partie de la géométrie euclidienne.


Sinon, pour la définition, le mot "conséquence" ne me paraît guère mieux que "démontrer". D'un point de vue purement linguistique, il est plus "passif", ce qui évite la connotation d'un agent que l'on peut percevoir sous "démontrer", mais il ne capture pas plus la notion bien spécifique de dérivation formelle qui permet de construire la classe d'équivalence des propositions "vraies" dans un système formel.

Cordialement,

[Médiat]

Par commutativité, j'entends la proposition :


La proposition "Tout groupe est commutatif", n'est pas (sous cette forme) une proposition du premier ordre et n'appartient pas à la théorie des groupes.

Plus complète veut dire qu'il y a moins de propositions indécidables (ce n'est pas une définition formelle, bien sur), qu'on se rapproche de la complétude. Pour fabriquer une théorie complète à partir de la théorie des groupes, il suffit d'ajouter un axiome (c'est un peu caricatural, mais cela marche) :

axiome qui assure que le groupe n'a qu'un seul élément, théorie dont la complétude est évidente (tous les modèles sont isomorphes donc, a fortiori, élémentairement équivalent).

ce qui évite la connotation d'un agent

Et c'est très exactement ce que je voulais éviter.

Quant à "conséquence", j'aurais peut-être dû préciser "conséquence logique", mais Jean Louis Krivine utilise souvent le mot "conséquence" seul, et je crois qu'on peut lui faire confiance .

[invité576543]

Par commutativité, j'entends la proposition :

La proposition n'est pas valide, les domaines des quantificateurs universels ne sont pas précisés, ni explicitement, ni implicitement.

"Tout groupe est commutatif" est tout autant, ou mieux, une proposition valide (), le domaine de G restant à définir, mais l'axiomatique de la théorie des groupes définit la notion de groupe. Le "quelque soit G" s'entend alors comme quelque soit l'objet mathématique répondant à la définition de groupe selon la théorie (e.g., un doublet (E, .), E un ensemble, . une opération binaire interne à E ayant telles et telles propriétés...).

Cordialement,

[invité576543]

Quant à "conséquence", j'aurais peut-être dû préciser "conséquence logique", mais Jean Louis Krivine utilise souvent le mot "conséquence" seul, et je crois qu'on peut lui faire confiance .

Ce n'est pas là le problème. Le problème est que ça ne couvre pas mieux pas pire la notion "dérivation formelle", bien particulière aux systèmes formels, que le mot "démonstration" couramment trouvé dans les définitions vulgarisées de "décidable". Les mots "conséquence" et "logique" ont aussi des connations qui s'éloigne du côté formel (dérivation basée sur la forme, sur la simple structure syntaxique, sans aucun présupposé de "signification) des systèmes formels.

Or c'est bien cette confusion, entre d'un côté les notions intuitives de signification, de "vrai", de démonstration, de conséquence, et de l'autre le côté mécanique, syntaxique, complètement non-sémantique, des systèmes formels (et donc du contexte du théorème de Gödel) qui est à l'origine de la réflexion présentée dans le premier message de ce fil.

Cordialement,

[invité576543]

La proposition "Tout groupe est commutatif", n'est pas (sous cette forme) une proposition du premier ordre et n'appartient pas à la théorie des groupes.

Pour continuer, la divergence porte peut-être sur "théorie des groupes".

On peut imaginer une notion très restrictive de la notion de "système formel comprenant la notion de groupe" comme un système formel dont les propositions partent de symboles muets "a", "b", etc. et d'un symbole ".", syntactiquement un opérateur binaire infixe, etc. Auquel cas effectivement, on a un premier système formel général, un deuxième plus particulier en ajoutant l'axiome de commutation, ou plus généralement des "théories" particulières en ajoutant tel ou tel autre axiome de contrainte, comme a.a=1, etc.

Mais à mon sens cela n'est pas la "théorie des groupes", qui dans mon vocabulaire couvre les propisitions portant sur les objets mathématiques appelés "groupes", ce qui n'est pas vraiment la même chose.

Cordialement,

[Médiat]

La proposition n'est pas valide, les domaines des quantificateurs universels ne sont pas précisés, ni explicitement, ni implicitement.

Je n'ai pas à le faire puisque je parle d'une théorie et que, par défaut il n'y a qu'un seul univers.

"Tout groupe est commutatif" est tout autant, ou mieux, une proposition valide

Je n'ai pas dit que ce n'était pas valide, j'ai dit, et je maintiens, que ce n'est pas une proposition du premier ordre.

Les mots "conséquence" et "logique" ont aussi des connations qui s'éloigne du côté formel (dérivation basée sur la forme, sur la simple structure syntaxique, sans aucun présupposé de "signification) des systèmes formels.

Tu es sur ? Parce que si le mot "logique" s'éloigne des systèmes formels, je ne sais plus de quoi on parle.

Pour continuer, la divergence porte peut-être sur "théorie des groupes".

C'est bien possible, puisque pour moi, je mot Théorie désigne l'ensemble des propositions conséquences (par les règles d'inférences de la logique adoptée) d'un système d'axiomes (Cet ensemble est souvent noté Th(A), où A est l'ensemble des axiomes).

[invité576543]

Tu es sur ? Parce que si le mot "logique" s'éloigne des systèmes formels, je ne sais plus de quoi on parle.

Bonjour,

Ce n'est pas une question "d'être sûr", c'est que le mot logique à des connotations bien particulières. Par exemple, à la fin du XIXème, quand Russell (je crois) propose que (faux => vrai) ~ vrai, au sein de la construction de la logique formelle, il choque pas mal de monde. Le mot "logique" jusqu'alors avait un sens différent de celui de logique formelle. Il y a pas mal de restes de la logique "à l'ancienne" dans le vocabulaire courant.

Pour moi, même la logique formelle, qui est à la fois un système formel et partie prenante de la définition même de système formel, reste purement syntaxique, vide de sens par elle-même. Ce sont des règles de ré-écriture basées uniquement sur la forme, la structure syntaxique. Le sens est quelque chose que nous, humains, rajoutons aux systèmes formels, y compris la logique formelle. On peut construire un système formel strictement équivalent à la logique formelle en remplaçant "vrai" par "faux", "faux" par "pomme", "=>" par "<", etc. Je défie alors un humain d'y voir la logique! Genre (pomme < faux) ~ faux.

C'est bien possible, puisque pour moi, je mot Théorie désigne l'ensemble des propositions conséquences (par les règles d'inférences de la logique adoptée) d'un système d'axiomes (Cet ensemble est souvent noté Th(A), où A est l'ensemble des axiomes).

D'accord, mais alors la "théorie des groupes" est un système basé sur des axiomes parlant de groupes, d'éléments de groupes, d'opérations de groupes, etc. Alors que la proposition de commutativité sans domaine de quantification de a ou b parle d'expressions respectant les règles syntactiques d'un groupe. Je suis bien d'accord que la seconde est une théorie. Mon problème est que ce sont deux théories complètement distinctes, et, pour moi, appeler "théorie des groupes" la seconde me semble entraîner une confusion néfaste. La divergence semble se confirmer n'être qu'un problème de vocabulaire.

Cordialement,

[Médiat]

Le sens est quelque chose que nous, humains, rajoutons aux systèmes formels, y compris la logique formelle.

Je ne pense pas avoir donné un quelconque "sens" à mes définitions qui sont justement formelles, par contre ce sont bien les règles d'inférence définies dans la "logique" qui permettent de créer des théorèmes à partir des axiomes.

Mon problème est que ce sont deux théories complètement distinctes, et, pour moi, appeler "théorie des groupes" la seconde me semble entraîner une confusion néfaste.

D'un autre côté, utiliser le langage de la logique formelle dans le cadre d'une question portant sur les systèmes formels définis à l'aide de cette même logique ne me paraît pas outrancier

Je t'accorde que le 5ième axiome (ou postulat ? je ne sais plus) de la géométrie d'Euclide est un exemple assez classique, mais je voulais l'exemple le plus simple possible ; quant à AC et HC ce ne sont pas exemples à utiliser dans le cadre d'une "vulgarisation", me semble-t-il.

[invité576543]

par contre ce sont bien les règles d'inférence définies dans la "logique" qui permettent de créer des théorèmes à partir des axiomes.

Je ne dis pas le contraire, je dis simplement que les "règles d'inférence" sont formelles, syntaxiques. C'est distinct de la notion de syllogisme, par exemple, dans la logique "traditionnelle", pour lequel le sens des mots importent.

quant à AC et HC ce ne sont pas exemples à utiliser dans le cadre d'une "vulgarisation", me semble-t-il.

Bien d'accord. Resterait alors comme exemple "moyen" (je continue à penser que l'exemple type groupe, s'il illustre la notion d'indécidabilité, est trop "formel" pour la vulgarisation) le 5ème axiome d'Euclide!

Cordialement,

[pedro_cristian]

J'essaye :

Une proposition p est indécidable dans une théorie (supposée consistante) si elle n'est pas conséquence des axiomes de cette théorie, et sa négation non plus. Une conséquence intéressante, c'est que l'on peut compléter la théorie soit avec la proposition p soit avec non p, et obtenir deux extensions consistantes de la théorie de départ.

Un exemple très simple, la théorie des groupes est l'ensemble des propositions qui se déduisent des axiomes définissant les groupes et que tout le monde connaît, dans cette théorie, la commutativité est indécidable (sinon, tous les groupes seraient commutatifs, ou bien à l'opposé, aucun), je peux donc créer deux théories : les groupes abéliens, et les groupes non commutatifs. On a rendu la théorie de départ un peu plus complète en ajoutant p, ou bien en ajoutant non p (mais pas les deux en même temps ). Le théorème de Gödel affirme que l'on peut ajouter tous les axiomes que l'on veut à l'arithmétique, le résultat ne sera toujours pas complet (= il restera des propositions indécidables).

l'exemple cité faux.

Avec les definitions de la théorie des groupes on peut exposer des groupes commutatifs et des groupes non commutatifs.

Les exemples plus parlant sont:
Axiome de choix (on a prouvé son indécidabilité (Godel/Cohen) : on peut construire un théorie avec ou sans).
l'Hypothese de continu (pas d'ensemble ayant strictement moins d'element que les reels (le continu) et plus (strictement) que les entiers.)
http://fr.wikipedia.org/wiki/Hypoth%C3%A8se_du_continu

[Médiat]

l'exemple cité faux.

Je ne pense pas, pour prouver tes dires tu devrais montrer que la commutativité (ou son contraire) se démontre à partir des seuls axiomes de groupes, et je ne pense pas que tu y arrives. C'est justement parce qu'il existe des groupes commutatifs et des groupes non-commutatifs que cette propriété est indécidable dans la théorie (dans le sens "logique" énoncé plus haut) des groupes.

Si tu avais tout lu, tu aurais vu que je n'ai volontairement pas pris AC et HC comme exemples ceux-ci étant bien trop compliqué pour une "vulgarisation". Je ne me vois pas faisant un cours complet sur les cardinaux pour arriver à l'hypothèse du continu (que je préfère énoncer )

[invite636fa06b]

l'exemple cité faux.
Avec les definitions de la théorie des groupes on peut exposer des groupes commutatifs et des groupes non commutatifs.

Bonjour,

Oui tout comme à partir des axiomes de la géométrie (sans le postulat d'Euclide), on peut construire des géométries euclidiennes et des géométries non euclidiennes.

Incontestablement, la commutativité est "indécidable" avec les axiomes habituels de définition des groupes.

L'exemple choque parce que l'on sait que c'est l'introduction des nombres qui conduit au théoreme de Gödel.

Son champ d'application est donc en dehors de la théorie des groupes.

PS croisement avec Mediat

[invité576543]

à partir des seuls axiomes de groupes

Bonsoir,

Entre autres pour vérifier que ce que je pense, ça m'intéresserait que tu indiques le système formel correspondant...

Cordialement,

[Médiat]

Il existe un élément neutre
Tous les éléments ont un symétrique
Associativité

Je ne connais pas assez Latex pour que l'écriture de ces axiome ne me prenne un temps inutile, chacun connaît ces axiomes (à tout hasard, je les aurais écrits sans préciser le domaine de mes quantifications (puisque c'est l'univers tout entier), pour ceux qui douteraient encore de la validité de cette écriture, je les renvoie vers les articles de Jean Louis Krivine, en particulier "Théorie axiomatique des ensembles")

[invité576543]

Il existe un élément neutre
Tous les éléments ont un symétrique
Associativité

Je ne connais pas assez Latex pour que l'écriture de ces axiome ne me prenne un temps inutile, chacun connaît ces axiomes (à tout hasard, je les aurais écrits sans préciser le domaine de mes quantifications (puisque c'est l'univers tout entier), pour ceux qui douteraient encore de la validité de cette écriture, je les renvoie vers les articles de Jean Louis Krivine, en particulier "Théorie axiomatique des ensembles")

C'est pas un système formel, ça. Un système formel part d'un ensemble fini de symboles, continue avec la définition du sous-ensemble des propositions valides (bien formées) dans le monoïde libre basé sur l'ensemble des symboles, etc. (règles de ré-écritures, axiomes, etc.)

(Suffit de chercher "système formel" sur Google pour trouver moults sites qui expliquent ça bien mieux que je pourrais faire dans un message dans un forum. Si Krivine a une approche de la notion de système formel qui n'est pas celle qu'on trouve couramment, ça pose un problème dans la discussion!)

Désolé de le présenter comme cela, mais il y a une différence entre une présentation axiomatisée d'une théorie, et un système formel.

Or la non perception de cette différence participe à la confusion qui amène des manières de voir le théorème de Gödel telle que celle du premier message de cette discussion. Parce que, dans ce que je comprends, le théorème de Gödel s'applique strictement aux systèmes formels, pas aux théories axiomatisées.

Cordialement,

[invité576543]

Parmi les liens, celui-ci me paraît intéressant pour le sujet. Je pointe directement sur la définition d'un système formel, mais tout le site est pertinent.

http://www.insa-lyon.fr/Departements...rmel.html#haut

Cordialement,