[Quizz] Fonctions et démonstrations.

Envoyé par DrTopos

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à...

[DrTopos]

Envoyé par alex_pi

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).

[SpiceGuid]

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).

[DrTopos]

Envoyé par SpiceGuid

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''.

[DrTopos]

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''.

[SpiceGuid]

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

[DrTopos]

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.

Envoyé par SpiceGuid

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''.

Envoyé par SpiceGuid

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.

Envoyé par SpiceGuid

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.

[DrTopos]

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.

[SpiceGuid]

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.

[DrTopos]

Envoyé par SpiceGuid

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.

Envoyé par SpiceGuid

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

Même remarque.

Envoyé par SpiceGuid

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.

[SpiceGuid]

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.

[Jedai]

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ï

[SpiceGuid]

@jedaï

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

[Jedai]

Envoyé par SpiceGuid

@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ï

[DrTopos]

Envoyé par SpiceGuid

@jedaï

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

Bravo !

[DrTopos]

Envoyé par Jedai

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.

Envoyé par Jedai

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.

Envoyé par Jedai

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.
  
  

Envoyé par DrTopos

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

[DrTopos]

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.

[SpiceGuid]

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.

[DrTopos]

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)