Réponses
-
@Neknek G est une formule non prouvable de la forme $\neg (\exists z) P(z)$. On prouve que, pour tout entier naturel $n$, on n'a pas $P(n)$. Il n'y a pas moyen d'en dé…
-
@Neknek Tu écris "aucun entier naturel n n’est le code d’une démonstration de la formule G dans la théorie T". Comment en déduis-tu que "aucun entier non-standard n n’…
-
@Neknek "Car G n'étant pas démontrable (...) G est vraie". Je n'ai pas compris ta démonstration de "G est vraie dans tout modèle". G est une proposition vraie dans N e…
-
Marcel Berger utilise lui aussi la notation $\Theta$.
-
@Cyrano: Par exemple, les tables de multiplication sont vues dès l'école primaire, ce sont des exemples de fonctions de l'ensemble des entiers naturels dans l'ensemble…@Mathurin : Ce n'est pas parce qu'on ne pourrait pas faire de mathématiques sans formalisme qu'un concept s'identifierait avec une de ses nombreuses formalisations. …@f_g: Le texte de Girard auquel tu fais allusion et le texte et Prouté ne sont pas de même nature. Je n'ai pas regardé en détail, mais il n'y a peut-être rien dans le con…C'est pénible qu'un intervenant de mauvaise foi vienne accuser les autres d'être de mauvaise foi. Ignorons ce troll!
@GG: Je n'ai pas trouvé où, dans ce livre, …@GG : Tu fais référence à quel livre? Dans The Joy of cats par Adamek, Herrlich et Strecker, on a la définition habituelle : "Observe that condition (c) guarantees …@f_g : Je vais essayer de reformuler ce que GaBuZoMeu et moi-même avons écrit ci-dessus. Les textes de Prouté sont très intéressants mais ils sont hors-sujet et après les…f_g : Bonjour, Girard s'intéresse à la théorie des démonstrations, c'est-à-dire qu'il ne s'intéresse pas tant à la prouvabilité d'un énoncé qu'à ses preuves et souhaite p…@GG: La notion de protocategory (je laisse le mot en anglais car je ne sais pas s'il a été utilisé en français) permet qu'un protomorphisme ait plusieurs domaines e…@Foys : Parce que j'espérais te faire prendre conscience du ridicule d'écrire "ça ne veut rien dire". Peine perdue!@Foys : Je n'ai jamais demandé ce qu'était un couple.@GG: Ceci étant, c'est précisément ainsi que Lawvere et Schanuel, dans leur livre qu'ils prétendent accessible aux lycéens, définissent un "point of a set $X$" : c'est une…@GG : Il n'y a pas plus de raison d'être insatisfait de la réponse "c'est juste la donnée d'un ensemble de départ, d'un ensemble d'arrivée et d'un élément de l'ensemble d'…@Foys :Une fonction, c'est juste la donnée d'un ensemble de départ 𝐴, d'un ensemble d'arrivée 𝐵 et de la donnée d'un élément 𝑓(𝑥) de…@Foys : Non, aucune complication cachée. La notion de fonction est indépendante de celle de lambda-terme : on peut très bien apprendre la notion de fonction et ensuite v…@lourran : Je ne comprends pas où tu veux en venir. C'est quoi, "la fonction 𝑓 de 𝑅 dans 𝑁, définie par 𝑓(𝑥)=3𝑥" ?
@Foys: "Question: 𝑥∈{1,2,3,4}↦5−𝑥∈{1,2,3,4} et 𝑥∈{1,2,3,4}↦7−(2+𝑥)∈{1,2,3,4} sont-elles égales (NB: il ne s'agit pas du même lambda-terme)?"
La réponse est oui. Des…Bonsoir,
Je reconnais ne pas avoir lu tous les messages, mais j'ai vu que certains ne font pas de différence entre une fonction et son graphe. Cela n'oblige-t-il pas de renoncer à la notion (essentielle selon moi) de "ensemble d'arrivée" d'une …Si tu tiens à ne considérer que des longueurs qui soient des carrés $n^2$ (pour une raison qui m'est obscure - dans le lien que tu donnes, ils donnent en exemple une longueur $4$, mais je crois que le fait que $4$ soit un carré est un hasard), alors…Bonjour
@questionneur. "On considère une grille de départ non vide, partiellement remplie, de côté de longueur $𝑛^2$, où $𝑛 \in \mathbb{N}^\ast$". Je trouve…@damien09: Si ça t'aide, tu peux supposer $\mathbb{N} = \omega$ (et supposer que tu fais des mathématiques dans un modèle de ZFC, même si rien ne t'y oblige).
Q…Bonjour
Pour tout entier $p$, le singleton $\{ (S^p O)^{\mathfrak{M}} \}$ est un ensemble, non? Alors $\bigcup_{p \in \mathbb{N}} \{ (S^p O)^{\mathfrak{M}} \}$ est un ensemble."sachant que des programmes en langages impératifs on été utilisé pour démontrer la conjecture des quatre couleurs" : @AlainLyon, pourrais-tu donner une source?@AlainLyon. Merci Alain, de tenter, au contraire des messages précédents, de me répondre. Tu as le mérite d'avoir parfaitement compris ma question.
Cependant, …@Poirot : Je m'en doute. En fait, j'aurais voulu qu'Alain, si c'est bien le cas (sinon, il peut pointer l'endroit où il utilise l'hypothèse AF), se rende compte qu'il …Il faut beaucoup de mauvaise foi pour essayer de faire croire que ma question "en quoi cette preuve, si elle est une preuve de ce que ZF+AF+AC est incohérente, n'est-elle pas une preuve de ce que ZF+AC est incohérente?" est équivalente à la question…@Mediat_Suprême : Comme si je ne le savais pas... Ça ne répond toujours pas à ma question.@Congru: Ma question initiale n'est pas différente de ma soi-disant nouvelle question. Si tu ne la comprends pas, ignore-la, peut-être quelqu'un d'autre (Alain?) voudr…Ça ne répond pas à ma question : en quoi cette preuve, si elle est une preuve de ce que ZF+AF+AC est incohérente, n'est-elle pas une preuve de ce que ZF+AC est incohérente?@Congru : Moi, je lis qu'il affirme que ZF + AF + AC, et non ZFC, est incohérente.Bonjour,
Je ne veux pas troubler la discussion au sujet de la négation de $G_\beta \subset \mathbb{Q}$, mais, en parallèle, j'aimerais savoir où AF est supposé intervenir.
La théorie des topos avec un objet des entiers naturels (laquelle est finiment axiomatisable) ne démontre-t-elle pas la consistance de l'arithmétique de Peano au second ordre?
Est-ce que tu veux bien détailler le passage suivant?(Quote)Pourquoi? Es-tu en train d'affirmer que $T \vdash \neg Cons(PA)$ implique $T \vdash \neg Cons(PA + \neg Cons(PA))$?
Pourquoi ne veux-tu pas de $Cons(T)$? L'argumentation de Martial était peut-être maladroite, mais on a bien que $T \nvdash \neg Cons(T)$.
Bonjour!
Qui est en ligne 5
+3 Invités