question sur l'existentiation

Bonjour,

A l'époque où je faisais des maths pour mes études, j'avais pour habitude lorsque j'étais en présence d'une quantification existentielle dans une démonstration (par exemple en déduisant "il existe v telle que F" (v une variable et F une formule) :

d'écrire :

soit v telle que F
je ne pouvais plus généraliser v, mais en contrepartie, je déduisais F
implicitement je considérais v comme une fonction des variables libres de la formule F (moins v)

Maintenant que je me suis "initié" à la logique (en lisant le Cori-Lascar), je ne comprends plus vraiment ce que je faisais. je pense aux formes de Skolem, mais ce n'est pas clair du tout. même écrire n appartient à grand N dans une démonstration me semble cacher des choses (notament à la généralisation)

J'ai l'impression que "le méta langage que j'utilisais en prépa modifie la règle de généralisation des formules".

Quelqu'un pourrait il m'aider à débrouiller tout ça?

D'avance merci,

Yomgui.

Réponses

  • Je n'ai pas trop compris ton "soit v tel que F" "pour prouver" qu'il existe v tel que F" dis-tu?

    Sinon, les axiomes admis sont:

    quand tu viens de prouver F (sous-entendu F(a)), et que tu dis "donc il existe v tel que F (sous-entendu F(v))" personne ne conteste

    quand tu viens de prouver F(x) sans rien supposer à propos de x, pas même dans les hypothèses, tout le monde accepte que tu enchaines par "donc pour tout x F(x)"

    Ce que tu évoques peut-être est que si sans rien supposer sur un (ou des) symboles fonctionnels f (pas même dans les hypothèses) tu arrives à prouver que qu'il existe un a tel que R(a,f(a)), tu as le droit (en logique classique) d'enchainer par un "donc il existe x tel que pour tout y R(x,y)", et c'est peut-être l'aspect déroutant entre today et tes souvenirs, mais je n'en sais rien en fait.

    C'est ça la Skolémisation: remplacer les $\forall x_i \exists yR(x,y)$ par des $\forall x_i: R(x,f(x))$ en choisissant "fresh" le symbole f (ci-dessus c'est la version duale, et le fire "correctement" après chaque alternance $\forall/\exists$)

    Si tu veux en savoir plus, peut-être pourras-tu donner un exemple pour préciser ton sentiement ou ta question?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Je me place dans le cas ou je viens de montrer :

    il existe v tel que F
    j'écrivais soit v telle que F est vérifié.

    je trouvais tout à fait normal d'avoir exhiber v satisfaisant F. ou en quelque sorte v est une "fonction" des variable libres de F. (en tout cas on ne pouvait pas faire n'importe quoi.

    En quelque sorte, la question que je me pose, c'est comment écrire dans un langage du premier ordre : "soit v telle que F est vérifié" (ou comment s'en passer eventuellement)
  • la question que je me pose, c'est comment écrire dans un langage du premier ordre : "soit v telle que F est vérifié" (ou comment s'en passer eventuellement)

    Bin tu l'écris (??????--->La logique est pas si censurante!!!)

    Tu peux par exemple avoir écrit:

    $\forall x_1...x_n \exists y blabla$

    Et puis tu veux continuer, et bien tu écris par exemple:

    Soit $(x_1...)$ (ou tu gardes ceux pour lesquels tu as déjà dit "soit"). Soit t tel que $OK(x_1,...;t)$

    Et tu continues, et c'est tout.

    Dans ta tête $t(x_1...x_n)$, tu le ressens comme une fonction*, ça c'est une chose, mais formellement, la feuille ne lit pas dans les pensées :D, donc pas la peine de se compliquer la tache. (*D'ailleurs, ça nécessiterait vaguement l'axiome du choix, une existence assumée de f par exemple, ajoutée imprudemment avec un schéma de compréhension ou substitution)

    A la fin tu as prouvé:

    1) $\forall ...\exists t:Ok(x;t)$

    2) $\forall ...\forall t: Ok(x;t)\to superok(x;t)$

    en 2 étapes et tu conclus "donc $\forall x..\exists t : superok(x;t)$ (par exemple).

    Maintenant qu'est-ce que tu veux exactement savoir, parce que si tu veux une réponse tendant vers "axiomes minimaux", là c'est du "sport" (on peut se passer de presque tout, et prouver qu'on ne perd rien, mais au prix de rallonger les preuves)

    En gros, je ne sais si je comprends bien ce que tu veux, mais il n'y a pas de "restriction" ou de censure "logique". Tu écris tout ce que tu veux, et la logique permet de voir TOUT ce que tu supposes (et d'ailleurs sans se prendre la tête, dès qu'il n'ya autre chose que $A\to A$, on le considère comme supposé par l'auteur.

    Ta question concerne-t-elle plutôt les problèmes de variabels liées?

    Tu as le droit aussi d'écrire "soit $f$ telle que $\forall x_1...:Ok(x...;f(x...))$ après avoir prouvé 1), mais c'est à toi de voir ensuite comment tu gères tes habitudes. Le symbole f doit être "fresh" (cadire nouveau, et ne doit apparaitre nulle part avant,même pas dans les hypothèses, ni les axiomes tacites, sinon, on entre en théorie des ensembles et c'est différent (parce que tu risques de parler de l'image de f, etc, voir de sa dim ou de ses limites, etc, et dans ce cas faudra l'assumer (en affirmant un truc du genre "axiome du choix" en gros)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • dans le Cori-Lascar, la notion de démonstration formelle dans un langage du premier ordre est définie comme une suite de formule telle que chaque nouvelle formule est soit un des axiomes ou un théorème, soit issu de l'usage licite d'une des règles de déductions (le modus ponens, la règle de substitution de formule équivalente a une sous formule dans une formule, et la règle de généralisation : avoir déduit la formule $F$ permet de déduire $\forall v F$)

    Parmi les axiomes des champs de quantificateurs : $(\forall v F)\longrightarrow F_{t/v}$ ou $t$ est un terme dont aucune des variables ne sont parmi celles dont le champ de quantification contient une occurrence libre de $v$, notamment en prenant $t=v$, on a $(\forall v F)\longrightarrow F$.
    Je vois donc que je peux "empiler et dépiler" les quantifications universelles dans un langage du premier ordre.

    Quand j'écris dans une démonstration soit $x$ dans $E$, j'ajoute à ma démonstration formelle $x\in E$, je poursuis mes raisonnements, j'aboutis à la formule G, dont $x$ est une des variables libres. Au moment ou je généralise $G$ par $x$, j'utilise $G \longleftrightarrow (x\in E\longrightarrow G)$ et le MP pour ne pas oublier que $x$ est dans $E$, j'ai l'impression de devoir modifier l'axiome de généralisation pour rester sur des rails...
    Mon impression quand je déclare $x\in E$ c'est de faire une hypothèse qui fait qu'il ne faut pas oublier cette formule au moment ou on universalise par rapport à $x$, et j'ai l'impression que c'est encore plus flagrant quand on regarde $\exists v F$. sauf que là je ne vois même pas de façon simple de s'adapter. clairement, je vais écrire des formules avec $v$, sauf qu'il n'est plus question d'universaliser avec $v$ (et d'autres problèmes, pourtant je n'ai rien dans ma définition de la démonstration formelle qui me permette de l'interdire (j'ai peut être pas tout compris non plus).

    Je glisse vers les écritures de la théorie ZFC, et je m'en rend compte si ça se trouve ce n'est plus un langage du premier ordre, j'ai l'impression qu'il va falloir que je rajoute des éléments à la notion de démonstration formelle pour pouvoir exhiber simplement $v$, et j'aimerai bien comprendre si j'ai compris, ou alors qu'on m'explique...

    Merci,

    YomGui.
  • soit issu de l'usage licite d'une des règles de déductions (le modus ponens, la règle de substitution de formule équivalente a une sous formule dans une formule, et la règle de généralisation : avoir déduit la formule $F$ permet de déduire $\forall v F$) (1)


    $(\forall v F)\longrightarrow F_{t/v}$ ou $t$ est un terme dont aucune des variables ne sont parmi celles dont le champ de quantification contient une occurrence libre de $v$, notamment en prenant $t=v$, on a $(\forall v F)\longrightarrow F$.
    Je vois donc que je peux... (2)

    Je ne comprends pas trop la phrase que j'ai mise en rouge de ta part: il n'y a pas à ma connaissance de "champ de quantification DANS un terme". Qu'est-ce que le champ de quantification d'une variable, si on ne précise pas un endroit précis dans une formule?

    Concernant (1), tu as peut-être fait une erreur de frappe, car, à ma connaissance, l'axiome $\forall xR(x)\to R(cekonveut)$ ne nécessite pas de restriction particulière à première vue. J'essaie d'interpreter quand cet axiome pourrait être faux, même avec un terme: on aurait alors $\forall R(x)$, mais pas $R(f(x))$, à cause d'une erreur syntaxique sur les problème de variables liées? alors voyons voir... $(\forall x: R(a,x))\to R(a;f(a,x))$, non ça, ça va. En fait je pense que tu parles "informatiquement", ie $\forall x\exists yR(x,y)\to \exists yR(y,y)$ (qui est faux!) et que donc tu évoques un problème de variables liées et non un problème de logique.

    Ce problème à lui seul nécessite une discussion (sans subtilité) assez longue car les logiciens soucieux de rien laisser au hasard formellement, font même le boulot "informaticien" consistant à "gérer" ce qu'on appelle "le $\alpha$ problème".

    Maintenant, résumer en une seule phrase quelle précaution suffit pour ne pas tomber dans le genre d'invalidité ci-dessus me parait difficile ce matin, personnellement, je sais que quand je programme en Caml j'évite soigneusement la "chierie" consistant à devoir renommer des variables liées en utilisant une technique de logique combinatoire (des combinateurs qui font sauter toute variable liée)

    Mais franchement, tu te poses un problème qui n'est pas important "logiquement" (renommage des variables liées, ou interdictions diverses pour éviter l'exemple ci dessus) parce que tu peux le contourner systématiquement en renommant les variables liées.

    Il faut savoir que le soucis probable de René et Daniel a été de présenter les systèmes formels les plus classiques dans le principal but d'illustrer précisément les théorèmes de complétude, de compacité, et in fine la correspondance syntaxe-sémantique. L'instinct du mathématicien conduit justement à ne jamais faire l'erreur de mal gérer les histoires de variables liées ou libres (il pourrait utiliser systématiquement 2 alphabets disjoints par exemple, avec une correspondance et sorte que l'énoncé ci-dessus deviendrait $\forall x*\exists y*R(x*,y*)\to \exists y* R(y,y*)$ par exemple (avec d'autres problèmes à la clé), bien qu'informatiquement (et donc formellement!!) ce ne soit pas si simple.

    Pour la suite, je ne te suis pas trop

    Oublions un moment l'histoire de "$\in E$" qui rajoute de la th des ens. Tu parles du principe de "généralisation", mais en fait ça n'a rien à voir avec le reste (ci-dessus), puisque généraliser consiste à passer de $R(x)$ à $\forall xR(x)$ (sous certaines conditions) et non l'inverse.
    Les 2 difficultés n'ont pas grand chose à voir en ce sens que ton précédent problème est un "$\alpha$-problème" alors que là tu évoques un profond principe de logique et de mathématique, qui en gros (les $\alpha$ problèmes afférents étant supposés réglés) consiste à considérer que si on arrive à prouver que toto est orange, sans rien supposer sur toto, même pas dans les hypothèses, ie on fait bien valoir à l'assistance qu'on a utilisé le mot "toto" comme un nom sans plus, alors on a vraiment que tout, absolument tout est orange.

    Ca tend à entrer en conflit (l'idée générale) avec l'esprit du théorème de Godel en ce que c'est une règle d'inférence "prétentieuse" (tout à fait officielle et constamment usitée, certes) qui transforme, sur le principe, une "fonction" de Var dans Preuves en une preuve (à chaque "valeur" e de toto, je pourrais in the real life, associer une preuve f(e) de l'orangité de toto..)


    Le discours avec "il existe" est dual, je ne te le fais pas.

    Concernant la fin, si ZF, ZFC, etc sont du premier ordre, là n'est pas la question, par exemple, il n'y a pas, à proprement parler de quantificateurs du genre $\forall x\in E : P$, c'est juste une abréviation de $\forall x : x \in E \to P $ (et dualement pour "il existe").

    Tu aurais certainement beaucoup à gagner, en logique, à essayer de l'inventer toi-même, très simplement, sans chercher à compliquer, et à te référer aux livres dans un esprit d'interaction (ie vérifier si ton intuition formel est en accord avec eux): dans tout ce que tu dis là, j'ai l'impression que tu te noies dans le "$\alpha$-problème. Je n'ai pas lu les COri-Lascar, mais à priori, je ne pense pas qu'ils ont développé sur des dizaines de pages ce sujet (que l'on trouve plutôt regardé dans les livres d'informatique, et encore..lol ça n'intéresse personne)

    Je vais réfléchir à une présentation simple et formelle de comment régler une bonne fois pour toutes ce $\alpha $ problème (mais comme tu ne m'a cité qu'un passage, Cori-Lascar l'a peut-être fait dans un paragraphe, je n'en sais rien, en fait.. ) pour les gens qui veulent lire de la logique.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Pour en revenir à ta phrase rouge, je pense que la précaution s'exprime ainsi:

    $(\forall xP)\to Q$ où $Q$ est obtenue en remplaçant toutes les occurences libres de x dans P par un terme qui ne contient aucune variable liée de P.

    Par contre, j'ignore si elle est suffisante... (à priori, je pense)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • pour pouvoir utiliser l'axiome $(\forall v F)\longrightarrow F_{t/v}$, l'idée c'est qu'il ne faut pas qu'une occurrence libre de $v$ dans $F$ soit sous le champ d'un quantificateur liant une des variables de l'écriture de $t$ (dixit CL). c'est aussi un illustration de l'exemple que tu donnais.

    Ma question porte vraiment sur le fait d'écrire $x \in E$, ou $x \in E: \: F$ dans une démonstration formelle implicitement ça modifie la règle de généralisation (post précédent). je cherche un comportement à adopter pour pouvoir écrire de telles phrases en restant consistant.

    "Toto est orange", le mot clé du paragraphe ou tu utilises cet exemple, est hypothèse si je comprends. Je crois que je n'utilise pas ce mot parce que j'ai un problème avec le lemme de déduction suivant : $F$ et $G$ 2 formules closes, $T$ une théorie alors :
    ($T \bigcup \{F\}$ permet de déduire $G$) si et seulement si ($T$ permet de déduire $F \longrightarrow G$)
    Le fait que les formules doivent être close (obligatoire sinon on démontre la réciproque de $(\forall v F) \longrightarrow F$ et le quantificateur universel ne sert plus à rien) j'ai l'impression d'avoir utiliser le résultat de ce lemme sans clôturer, j'analyse mal le fait que très vraissemblablement je ne l'ai utilisé que licitement.
    J'ai tendance à relier l'utilisation de ce lemme à la notion de paramètre, et je me pose la question de travailler dans un langage (et sa réalisation, où tous les éléments de l'ensemble de base sont associés à un symbole de constante (distinct de tous les autres)) qui permet(rait) de "constantiser" les variables. Cependant je ne comprends pas bien la notion de paramètre.

    Tu peux m'éclairer sur les conditions qu'il y a pour pouvoir déduire $\forall x R(x)$ de $R(x)$?, dans le CL, il n'y en a pas. (ce qui me conforte dans l'idée que nos concepts de bases ne sont peut être pas identiques (mais moi j'ai seulement ceux-là :) )

    Encore merci,

    YomGui
  • christophe chalons écrivait:
    > Pour en revenir à ta phrase rouge, je pense que la
    > précaution s'exprime ainsi:
    >
    > $(\forall xP)\to Q$ où $Q$ est obtenue en
    > remplaçant toutes les occurences libres de x dans
    > P par un terme qui ne contient aucune variable
    > liée de P.
    >
    > Par contre, j'ignore si elle est suffisante... (à
    > priori, je pense)

    la contrainte sur les variables que tu proposes est plus forte que celle qui est donnée dans le CL (et qui est celle que j'ai bien mieux donné dans mon post précédent, je ne ferai plus de logique de mémoire à 2h00 du matin...). Ceci dit l'idée de ne pas se compliquer la vie avec les noms de variables liées me semble excellent.
    Je suis en train de désintuiter ce que je fais quand je prouve un résultat.
  • qu'il y a pour pouvoir déduire $\forall x R(x)$ de $R(x)$?, dans le CL, il n'y en a pas

    ;) je ne sais pas si l'un ou l'autre vient sur ce forum de temps en temps, mais il risque de ne pas être content:D, car ça par contre c'est le truc incontournable...

    Bon pour répondre à tes 2 posts, le mieux c'est peut-être de tout reconstruire pour bien définir les règles à la fin. La reconstruction porte sur l'idée que "n'importe quelle" notion de théorie logique (du 1er ordre) qui marche doit vérifier le théorème de complétude.

    Le point crucial (je ne sais si tu abordes la logique après avoir fait des maths, et comme ça dès le départ) à avoir en tête, c'est le rôle de la logique: opérationnellement, la logique est à toutes les maths ce que sont les polynômes au corps $(\Q,0,1,+,\times)$

    Par conséquent, malgré l'air familier, elle n'enlève ni ne rajoute de trucs "actifs" aux preuves, elle se contente de définir formellement une sorte de "parsing" d'un texte mathématique et garantit la complétude (à savoir que quand on peut pas prouver un truc, il existe un monde (visible à l'oeil nu) où il est faux, et réciproquement)

    S'embourber dans le $\alpha-problème$ est un accident pas grave et résulte des balbutiements probables du début du siècle (sans ordi), où, au fond, fallait à un moment "espérer" ne pas se tromper (je parle avant la découverte cruciale et d'ailleurs bizarroide* du th de complétude).

    * à priori on ne connait des choses ce qu'on y met nous-mêmes, et il faut bien s'avouer qu'on a dû y mettre le théorème de complétude, ce qui nous rend tous un peu suspects, les scientifiques.

    Imaginons une logique où tu n'aies pas le droit aux variables liées (genre les touches quanteurs bugguent, quand tu veux taper un teste)

    Tu seras obligé de procéder autrement, ie par abréviation.

    Tu diras: Notons $S$ le nouveau prédicat $n aire$ tel que $S(x_1,...,x_n)$ signifie que pour tout $y:R(x_1,...,x_n,y)$. Tu dénonceras une triche (avec mon "pourtout"), mais l'avantage est que tu peux réutiliser assez facilement la variable y, t'es juste obligée, (et seulement à cette ligne) de la prendre différente des $x_i$.

    Quand tu écris une preuve, à priori, tu sais d'avance tout ce dont tu veux te servir, ce qui te permet de définir tous tes prédicats à l'avance et ne pas avoir besoin d'en définir "à la volée" pendant la preuve.

    Bien sûr, tu as bcp de constantes dans ton langage et pour souscrire à ta demande de crééer un "monde" "générique" où les modèles ne contiennent que les valeurs des constantes dans ton ensemble base, il y a une définition très simple de notion de preuve (il faut avoir un ensemble inanalysé de constantes sur lesquelles on n'a rien supposé!) qui passe par un jeu.

    Tu prends ensuite des axiomes propositionnels (resp tu fais du calcul des séquents, peu importe), et les 2 (resp3) règles sont:

    1) le modus ponens
    2) la généralisation (j'y reviens ensuite)
    (resp 3) l'abstration le truc qui t'effraie, dont tu as parlé)

    En plus des axiomes propositionnels, tu as les axiomes de la forme $S(u_1,...,u_n)\to R(u_1,...,u_n,t)$ pour tous les termes $u_i,t$

    Et là (par un raisonnement de jeu) tu as un théorème de complétude parfait.

    Qu'est-ce que (2)? Et bien, voyons la correspondance "jeu":

    1) le modus ponens, se traduit par la règle du jeu:

    "Nous en sommes à ce que je veux te prouver P, et je t'affirme que c'est dû au fait qu'on a d'un part $A\to P$ et d'autre part $A$. Je ne t'accorde que d'exiger que je t'en prouve qu'une seule des 2 évoquées. Tu es le "sceptique" tu choisis et la partie continue ainsi. Elle s'arrête (et je gagne) si on tombe sur un axiome.

    (resp 3) dans ce cas, il y a un contexte (de choses que le sceptique a admises et on en est au stade où je veux te prouver $U\to V$. Et bien j'ai le droit de dire "je prends $U$ dans mon "panier" de choses admises et je vais te prouver $V$". Et la partie continue.. et ne s'arrête (et je gagne) que quand on tombe sur un axiome ou une chose admise en position "à prouver"

    Dans ce paradigme, (2) est le droit suivant "nous en sommes à ce que je veux te prouver $S(u_1,...,u_n)$ et mon droit est d'exiger que tu choisisses le terme $t$ que tu veux, et on passe à ce que je dois te prouver $R(u_1,...,u_n,t)$

    Vue à l'endroit (dans une preuve écrite), cette règle du jeu se traduit par "si on a déjà acquis tous les $R(u_1,...,u_n,t)$ pour chaque terme $t$, alors on a le droit de mettre $S(u_1,...,u_n)$ dans les trucs acquis. C'est une règle infinitiste

    Le rôle du réservoir de constantes inanalysées est qu'il suffit d'acquérir "une seule" $R(u_1,...,u_n,c)$ pour "savoir" comment tu ferais pour acquérir toutes les autres $R(u_1,...,u_n,t)$. De là ce jeu qui te parait "infini" devient en fait, un jeu "trivialement" réductible à un arbre à branchement fini, car, tu regardes tes potes et au moment où ils se moquent de toi parce que tu viens d'inférer $S(u_1,...,u_n)$ de $R(u_1,...,u_n,c)$ et qu'ils te font remarquer que tu n'as que prouver le truc pour $c$ te pas pour les autres, tu leur dis "mais si, mais pour que le dessin de l'arbre prenne moins de place, j'ai caché les autres, je ne vous en montre qu'une qui est générique. Si la constante $c$ n'est pas corrompue (problème seulement dans le cas séquents si elle apparait dans les hypothèses admises ou si $c=$ l'une des $u_i$ ) ils seraient de très mauvaise foi de ne pas te croire (ou stupides). Si elle est corrompue, ça "saute aux yeux".

    Je pense qu'avec ce paradigme tu peux "réintuitiver" comme tu dis comment traduire tout ça avec des variables liées ou de la skolémisation. En pratique, il est vrai que les livres (dont les auteurs ont résolu en eux-mêmes le $\alpha$problème) ont réglé la question "informatiquement", mais ça ne témoigne pas de la difficulté, ni en fait de leurs propres longues réflexion qui les a menés à maitriser le problème.

    Le plus simple m'apparait quand-même de renommer systématiquement les variables liées pendant un certain temps, puis une fois entrainé, de s'amuser à écrire des formules qui déstabilisent tout le monde, ne contenant que le minimumu possible de variables liées. Mais ça, c'est juste pour rigoler... On est beaucoup à préférer les renommer (bien que ça ne soit pas nécessaire). C'est pour ça que je t'ai donné une règle plus restrictive que CL, mais elle marche tout aussi bien**.

    Donne-moi des exemples, si tu n'es pas satisfait par ce post, qu'on discute sur pièces

    $\forall xP$ ne parle pas des valeurs des variables liées dans $P$ (qui n'ont en ont pas, qui sont juste là pour se passer d'abréviations)

    Donc, de toute façon, toute apparition de variable dans t (qui va remplacer x dans P, pour donner Q) qui serait liée dans $P$ serait simplement maladroite (mais si le gars y tient, il suffit de renommer les variables liées de $P$ de manière à pouvoir appliquer la règle restrictive que je t'ai proposée, ce qui est faisable avec.. elle-même

    Remarque, si dans le domaine du $\alpha$problème il n'y avait pas de "confort" (par exemple possibilité de changer la règle de CL en la mienne sans perte par exemple), ce serait louche de toute façon. Faut juste éviter les étourderies
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Je crunche sur ce que tu me dis et te reviens,
    pour l'enguelade de la part de CL, je suis tout ouïe :

    $(\forall v F) \longrightarrow F$ combiné avec le MP ne suffit pas pour déduire $F$ de $\forall v in F$?
  • dans le post précédent, j'ai écrit n'importe quoi à la place de $\forall v F$ à la toute fin...
  • Si bien sûr! Mais (??? où est le problème? Aurais-je sous-entendu que non?)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • dans un de tes posts tu expiques que pour génaliser $R(x)$ il faut certaines conditions, et je l'a interprêter à l'envers dans le post précédent.

    Du coup je suis intéressé par ces conditions, (tant elles sont dans ton post précédent, que je n'ai pas encore finit)
  • Merci pour ton post explicatif, abstraction et contexte sont les mots dont j'avais besoins, pour comprendre ce sujet, merci...


    YomGui.
  • De rien.
    pour l'enguelade de la part de CL, je suis tout ouïe :

    En fait, dans un livre qui parle de logique du premier ordre, il y a forcément un moment où formalise comment on prouve des énoncés qui commencent par $\forall$....

    Sinon ce serait la galère (ou hors-sujet par rapport aux maths): quand tu fais un simple calcul avec x, et que tu dis "bon bin pour tout x,..." à la fin, t'imagines bien qu'il y a une formalisation logique de ça. Donc ils doivent en parler quelque part lol

    Les autorisations d'inférence sont les suivantes:

    Après avoir prouvé (dans le contexte C qui est un ensemble d'hypothèses, par exemple) $P$, tu es autorisé à inférer $\forall xP$ quand la variable $x$ n'est libre dans aucune hypothèse de C.

    La variante "à la Hilbert" (qui revient au même en fait): quand tu as déjà prouvé $H_1\to H_2\to ... \to H_n\to P$, tu es autorisé à inférer $H_1\to H_2\to ... \to H_n\to \forall xP$ quand $x$ n'a aucune occurence libre dans aucune des $H_i$.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Priorité à droite des parenthèses dans le post ci-dessus $a\to b\to c$ signifie $a\to (b\to c)$
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.