Publicité
+ Répondre à la discussion
Page 3 sur 9 PremièrePremière 1234567 ... DernièreDernière
Affichage des résultats 41 à 60 sur 165
  1. #41
    alex_pi
    Invité(e)

    Par défaut

    Citation Envoyé par DrTopos Voir le message
    Question 8. Un énoncé de la forme E => F, qui n'est donc qu'une abbréviation pour ?x:W(E) F, est bien formé même si F a des occurrences libres de x. Autrement-dit, l'implication peut être dépendante. Pouvez-vous donner un exemple réaliste (c'est à dire non tiré par les cheveux) d'une telle dépendance dans la langue naturelle et dans les mathématiques élémentaires ?
    J'avais pensé à quelque chose comme E => (E => F) => F qui s'exprime par ?x:W(E) ?y: ( (x:W(E)) -> W(F) ) F, mais je ne suis pas convaincu.

    Et pour ce qui est de la langue naturelle, là...

  2. #42
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Citation Envoyé par alex_pi Voir le message
    J'avais pensé à quelque chose comme E => (E => F) => F qui s'exprime par ?x:W(E) ?y: ( (x:W(E)) -> W(F) ) F, mais je ne suis pas convaincu.
    Ton exemple n'est pas dépendant, car x est déclaré deux fois de suite. Il s'agit donc de deux x différents, ou si tu préfères, ?y: ( (x:W(E)) -> W(F) ) F ne dépend pas de x puisque c'est une variable liée dans cette expression.

    Trouver un exemple dans le langage décrit ici est assez facile. L'un des plus simples est le suivant:

    ?x:W(E) ?q:W(E) -> O q(x)

    La prémisse est E, et la conclusion ?q:W(E) -> O q(x), qui dépend notoirement de x. Quant-à savoir quel est le sens de cet énoncé est une autre affaire (mais ce n'est pas difficile).

    Toutefois, la question 8 ne porte pas sur ce langage formel. Elle porte sur la langue naturelle (le Français par exemple, mais pas obligatoirement), et le langage des mathématiques élémentaires (tel qu'on l'enseigne au lycée ou à la fac).

  3. #43
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    Par défaut

    J'ai édité mon post #21 pour détailler l'approche syntaxique (dans laquelle j'ai échoué) à comparer avec l'approche sémantique (avec laquelle alex_pi a brillamment réussi).

  4. #44
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    J'ai édité mon post #21 pour détailler l'approche syntaxique (dans laquelle j'ai échoué) à comparer avec l'approche sémantique (avec laquelle alex_pi a brillamment réussi).
    Ta méthodologie est intéressante en ce qu'elle semble être automatisable. Toutefois, la réponse ne pouvait pas être complètement syntaxique, car il fallait quand même partir de définitions de la négation et de l'implication, deux choses qui n'étaient pas données d'avance, et qui dans ce cadre étaient plutôt de nature ``culturelle''.

  5. #45
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    La question 8 n'est pas résolue pour le moment, mais il est vrai qu'elle est d'un genre particulier. Afin de vous donner plus de grain à moudre, voici les trois suivantes.

    Vous avez trouvé les définitions attendues pour la négation et l'implication. Il nous reste encore trois connecteurs logiques à définir, et je procède comme pour la négation et l'implication.

    Question 9. Soient E et F deux énoncés. Donnez une définition de leur disjonction (OU logique) qui sera notée E | F. La disjonction peut-elle être dépendante ?

    Question 10. Soient E et F deux énoncés. Donnez une définition de leur conjonction (ET logique) qui sera notée E & F. La conjonction peut-elle être dépendante ?

    Question 11. Soit T un type, x une variable de type T, et E un énoncé pouvant contenir des occurrences libres de x. Donnez une définition de !x:T E, qu'on lira: ``il existe x dans T tel que E''.

  6. #46
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    Par défaut

    Question 9:

    On possède les types sommes donc un témoin de l'énoncé demandé est:

    (x:W(E)+W(F)) -> W(E | F))

    La sémantique de Heyting donne alors un type plus direct de ce témoin:

    W(?x: (W(E)+W(F)) (E | F))

    L'énoncé recherché est donc:

    ?x: (W(E)+W(F)) (E | F)

    Mais je n'ai pas répondu à toute la question.


    Question 10:

    On possède les types produits donc un témoin de l'énoncé demandé est:

    (x:W(E)*W(F)) -> W(E & F))

    La sémantique de Heyting donne alors un type plus direct de ce témoin:

    W(?x: (W(E)*W(F)) (E & F))

    L'énoncé recherché est donc:

    ?x: (W(E)*W(F)) (E & F)

    Mais encore une fois je n'ai pas répondu à toute la question.


    Question 11:

    ~ (?x:T ~E)

    ~ (?x:T ?q:O ?y:W(E) q)

    ?p:O ?w:W(?x:T ?q:O ?y:W(E) q) p

  7. #47
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    D'abord une remarque. J'aimerai qu'on note la somme de types avec le signe +, plutôt qu'avec le signe | qu'on réservera pour la disjonction.

    Citation Envoyé par SpiceGuid Voir le message
    Question 9:

    On possède les types sommes, donc un témoin de l'énoncé demandé est:

    (x:W(E)) -> (y:W(F)) -> (W(E) | W(F))
    Non, car je peux facilement démontrer l'énoncé ci--dessus, par exemple comme ceci:

    (x:W(E)) |-> (y:W(F)) |-> i_1(x)

    où l'application i_1 de W(E) vers W(E) + W(F) est l'inclusion canonique. Cet énoncé est donc toujours vrai indépendamment de E et de F. Il ne signifie donc certainement pas ``E ou F''.


    Citation Envoyé par SpiceGuid Voir le message
    Question 10:

    On possède les types produits, donc un témoin de l'énoncé demandé est:

    (x:W(E)) -> (y:W(F)) -> (W(E) * W(F))
    Même remarque. Je peux démontrer cet énoncé comme ceci:

    (x:W(E)) |-> (y:W(F)) |-> (x,y)

    qui est donc vrai indépendamment de E et F.


    Citation Envoyé par SpiceGuid Voir le message
    Question 11:

    ~ (?x:T ~E)

    Il faut développer?
    C'est une définition possible, mais ce n'est pas celle que j'attends. Celle que j'attends est constructive, alors que celle-ci ne l'est pas. Elles ne sont donc pas équivalentes. Je recommande d'oublier les règles à la ``De Morgan'', qui sont toutes non constructives, et surtout de raisonner sans la négation.

  8. #48
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut


    Un conseil: Evitez d'éditer vos post en remplaçant du texte. Ajoutez-en seulement.

    Il vient de se passer que j'ai cité et commenté un texte qui a disparu. Ceci risque de rendre le fil incompréhensible. Alors, n'allez pas trop vite, et surtout ne supprimez rien. Assumez vos écrits.

  9. #49
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    Par défaut

    Désolé, j'étais en train de le corriger pendant que vous écriviez votre commentaire (il suffit de regarder l'heure), mais c'est certain que j'aurai du ajouter au lieu de modifier.

    Ma compréhension des choses est beaucoup trop syntaxique.

  10. #50
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    Question 9:
    ?x: (W(E)+W(F)) (E | F)
    Autrement dit: E | F = ?x: (W(E)+W(F)) (E | F). C'est une définition (cyclique) incorrecte, car on ne peut pas définir E | F en fonction de lui même.

    Citation Envoyé par SpiceGuid Voir le message
    Question 10:
    ?x: (W(E)*W(F)) (E & F)
    Même remarque.

    Citation Envoyé par SpiceGuid Voir le message
    Question 11:

    ~ (?x:T ~E)

    ~ (?x:T ?q:O ?y:W(E) q)

    ?p:O ?w:W(?x:T ?q:O ?y:W(E) q) p
    Voir ma réponse sur cette question dans le post #47 ci-dessus.

  11. #51
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    Par défaut

    Pour l'historique, de mémoire, voici l'ancienne ânerie que j'ai spontanément remplacée par une nouvelle:

    Question 9:

    On possède les types sommes donc un témoin de l'énoncé demandé est:

    (x:W(E)) -> (y:W(F)) -> (W(E) | W(F))

    La sémantique de Heyting donne alors un type plus direct de ce témoin:

    W(?x:W(E) ?y:W(F) (E | F))

    L'énoncé recherché est donc:

    ?x:W(E) ?y:W(F) (E | F)

    Mais je n'ai pas répondu à toute la question.


    Question 10:

    On possède les types produits donc un témoin de l'énoncé demandé est:

    (x:W(E)) -> (y:W(F)) -> (W(E) * W(F))

    La sémantique de Heyting donne alors un type plus direct de ce témoin:

    W(?x:W(E) ?y:W(F) (E & F))

    L'énoncé recherché est donc:

    ?x:W(E) ?y:W(F) (E & F)

    Mais encore une fois je n'ai pas répondu à toute la question.

  12. #52
    Expert Confirmé Sénior
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    avril 2003
    Messages
    6 172
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : avril 2003
    Messages : 6 172
    Points : 7 668
    Points
    7 668

    Par défaut

    Houla, il s'en est passé des choses depuis que j'ai vu ce sujet pour la dernière fois (je m'étais abstenu de répondre vu que j'avais déjà vu les réponses dans la version que nous avait envoyé DrTopos).
    Question 9 :
    La disjonction classique est ~F => E
    Ce qu'on traduit directement avec les définitions précédentes.

    Question 10 :
    ?x:W(E) ?y:W(F) (x,y)

    Question 11: SpiceGuid a déjà répondu

    --
    Jedaï

  13. #53
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    Par défaut

    @jedaï

    (x,y) n'est pas un élément de O donc ta réponse à la question 10 est mal typée.

  14. #54
    Expert Confirmé Sénior
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    avril 2003
    Messages
    6 172
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : avril 2003
    Messages : 6 172
    Points : 7 668
    Points
    7 668

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    @jedaï

    (x,y) n'est pas un élément de O donc ta réponse à la question 10 est mal typée.

    Exact, j'ai répondu trop vite (j'ai essayé d'utiliser deux méthodes différentes, mais la syntaxique ne me réussit pas apparemment), la bonne réponse s'appuie également sur la logique classique où E et F se traduit par : ~ (F => ~E)

    Par ailleurs je viens de relire la réponse de DrTopos et il semble ne pas vouloir du genre de réponse que j'ai donné...

    --
    Jedaï

  15. #55
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    @jedaï

    (x,y) n'est pas un élément de O donc ta réponse à la question 10 est mal typée.
    Bravo !

  16. #56
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Citation Envoyé par Jedai Voir le message
    Question 9 :
    La disjonction classique est ~F => E
    Ce qu'on traduit directement avec les définitions précédentes.
    Certes, mais il s'agit d'une définition classique non constructive, strictement moins forte que celle que j'attends, qui est constructive. En fait, c'est la même remarque que pour la réponse à la question 11 faite par SpiceGuid, et je te renvoie à mes commentaires à la fin du post #47.

    Citation Envoyé par Jedai Voir le message
    Question 10 :
    ?x:W(E) ?y:W(F) (x,y)
    Cette expression est mal formée, car (x,y) n'est pas de type O.

    Citation Envoyé par Jedai Voir le message
    Question 11: SpiceGuid a déjà répondu
    Idem. Ce n'est pas constructif. Voir la fin du post #47.


    Evidemment, je me rends bien compte que ces questions sont troublantes pour des personnes qui pensent exclusivement en logique classique, et dans un contexte où le mot ``constructif'' n'a pas été défini. Je vais donc donner quelques explications, et expliquer (et non pas démontrer car cela nécessiterait des moyens hors de portée de ce fil) pourquoi la définition proposée par Jédai n'est pas constructive.

    L'un des principes énoncés par Brouwer (le maître de Heyting) dès 1912, et admis par la suite par tous les constructivistes comme une exigence de base, est que si on a une démonstration de E | F (dans le contexte vide), alors on doit pouvoir extraire mécaniquement de cette démonstration soit une démonstration de E, soit une démonstration de F. Attention, il ne s'agit pas ici de témoins, mais de démonstrations (preuves).

    Il résulte de cette exigence et du théorème d'incomplétude de Gödel (en supposant le système consistant, et ayant des types infinis comme par exemple des types récursifs), que l'énoncé ?q:O ~q | q, qu'on appelle ``tiers exclu'' n'est pas démontrable dans un système constructif. En effet, s'il l'était, on aurait un terme f représentant une fonction dépendante de type (q:O) -> W(~q | q). Le théorème de Gödel nous fournit un énoncé I qui n'est pas démontrable et dont la négation n'est pas non plus démontrable. Le terme f(I) est alors de type W(~I | I). Si le système est constructif, on peut extraire de ce terme, soit un terme de type W(~I), soit un terme de type W(I), ce qui contredit le fait que I est indécidable.

    Reprenons donc la définition proposée par Jédai pour E | F, soit ~F => E. Je peux facilement démontrer le tiers exclu avec sa définition:

    (q:O) |-> (x:W(~q)) |-> x :W(?q:O ~q | q)

    On voit donc que la définition donnée par Jédai est incompatible avec l'exigence d'être constructif.


    Il va donc falloir trouver autre chose ...



    Quelques conseils:

    • Oubliez la logique classique, les tables de vérité booléennes et les lois à la ``de Morgan'', qui sont des concepts non constructifs.
    • Pour les questions 9, 10 et 11, pensez à la façon dont on utilise normalement ces énoncés quand ce sont des hypothèses.
    • N'oubliez pas la question 8, qui a son intérêt aussi, même si elle est plus ``littéraire''. Elle est surtout utile pour comprendre la notion de dépendance dans l'implication. Elle permettra de montrer que cette notion n'a rien d'esotérique, mais est au contraire parfaitement naturelle.


  17. #57
    alex_pi
    Invité(e)

    Par défaut

    Citation Envoyé par DrTopos Voir le message
    Question 9. Soient E et F deux énoncés. Donnez une définition de leur disjonction (OU logique) qui sera notée E | F. La disjonction peut-elle être dépendante ?
    Bon, je triche un peu, j'ai quelques notions de lambda calcul.

    Le but d'un "ou" en constructiviste est de dire "si j'ai une démo de E => G et une démo de F => G alors G. (on remarque qu'il n'y a pas de disjonction de cas). Donc E | F va s'écrire
    ?G:O (E =>G) => (F=>G) => G Ce qui se transpose en (là je sens que je vais me planter)
    ?G:O ?x_eg:W(?x:W(E) G) ?x_fg:W(?x:W(F) G) G

    Pour l'histoire de la dépendance, franchement je n'ai pas encore compris ce que ça voulais vraiment dire.

    Question 10. Soient E et F deux énoncés. Donnez une définition de leur conjonction (ET logique) qui sera notée E & F. La conjonction peut-elle être dépendante ?

    On doit pouvoir utiliser le précédant avec
    ((E => G) | (F => G)) => G que j'ai un peu la flemme de réécrire pour être franc :-) Mais il y a plus direct :
    Pour tout G(E => F => G) => G soit
    ?G:O ?x:W(?x_e:W(E) ?x_f:W(F) G) G

  18. #58
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Je ne vais pas répondre tout de suite à la proposition d'alex_pi. Je pense qu'il est plus intéressant de laisser les autres participants la discuter eux-mêmes, d'abord pour savoir si elle est bonne on pas bonne, et s'ils la jugent bonne, pour donner une justification dans l'esprit des conseils que j'ai donnés à la fin du post #56.

    Par ailleurs, il est inutile de faire systématiquement l'expansion de ce qu'on écrit pour ne laisser que des quantificateurs universels. On sait que c'est possible de toute façon. Si on a introduit des notations nouvelles c'est pour s'en servir.

  19. #59
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    Par défaut

    Citation Envoyé par alex_pi
    Le but d'un "ou" en constructiviste est de dire "si j'ai une démo de E => G et une démo de F => G alors G.
    Soit, ça paraît raisonnable. Dans ce cas j'ai envie d'écrire:

    ?G:O ?x:W(E=>G) ?y:W(F=>G) G

    ?G:O ?x:W(u?:W(E) G) ?y:W(?v:W(F) G) G


    Pour la question 10 je comprends que tu puisse utiliser le résultat précédent, car le but d'un "et" en logique constructiviste est de dire "si j'ai une démo de E => G ou une démo de F => G alors G, en tout cas c'est ce que tu formalise par ((E => G) | (F => G)) => G.
    Par contre je ne comprends pas ta méthode alternative.

  20. #60
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Je vous propose un petit test pour confirmer ou infirmer la proposition d'alex_pi (reprise par SpiceGuid) concernant la disjonction.

    Normalement, on peut déduire E | F aussi bien de E que de F. Dans ce système, on devrait donc pouvoir exhiber des fonctions des types suivants:

    W(E) -> W(E | F) et W(F) -> W(E | F)


    Autre exercice amusant: Montrer que les deux propositions d'alex_pi pour la conjonction sont équivalentes, en exhibant deux fonctions (une dans chaque sens) entre

    W(?q:O ((E => q) | (F => q)) => q) et W(?q:O (E => (F => q)) => q)

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •