Démonstration logique

messiLaPulga59
messiLaPulga59
dans Fondements et Logique
Bonjour,
Je cherche à démontrer une formule logique assez instinctive qui est la suivante :

On admet : C -> (A \/ B)
Démontrons alors : (C -> A) \/ (C -> B)

Je dois utiliser pour cela les formules de déduction naturelle.
Ca fait maintenant un boût de temps que je m'y casse les dents, c'est pour cela que je sollicite votre aide et votre talent ;-).
Merci d'avance.

Réponses

  • Foys
    Foys
    Commence par montrer $\neg \left [(C\to A) \vee (C \to B)\right],C \to (A \vee B) \vdash \perp$. (ensuite on conclut par un raisonnement par l'absurde).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • messiLaPulga59
    messiLaPulga59
    Certes mais c'est pour démontrer ça que j'ai des difficultés.
  • christophe c
    christophe c
    assez instinctive

    ????? Bin si tu n'arrives pas à la prouver, qu'entends-tu par "instinctive"? Comme c'est de la logique, ne crois-tu pas que tu pourrais tout simplement "la rejeter" et voir ce que ça entraine?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • messiLaPulga59
    messiLaPulga59
    J'ai finalement trouvé une solution en déduction naturelle, mais elle est très longue et je ne pense pas que ce soit la meilleure solution. Je l'ai implémentée en Coq (voir fichier joint) et ça me donne 100 lignes.
  • christophe c
    christophe c
    De mon téléphone je ne peux pas ouvrir le fichier mais de toute façon je ne connais pas COQ (et il parait que c'est une usine à gaz).

    Mais comme son nom l'indique dans déduction naturelle il y a naturelle. Foys t'a explicitement donné un point de départ précieux. Un cas particulier de ton énonce est le tiers exclus donc si tu manipules COQ tu pouvais te dire qu'il s'agit de réduction naturelle en logique CLASSIQUE (île le RPA suggère par foys est INEVITABLE.

    C'est sur que si tu utilises un système intuitionniste tu vas galérer!! (Ou recevoir un Nobel).

    La fausseté de ce que tu veux prouver entraine C et non A et C et non B, et un axiome puissant et trop peu célèbre t'accorde le droit de dire que C et C , c'est équivalent à C. Je serais très surpris que tu n'aies pas en tête cet axiome de duplication en tête. Ceci étant dit la contraposée de ton truc est donc quasiment une identité quand tu admets que nier X=>Y veut dire affirmer X et nier Y.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Bruno
    Bruno
    Christophe !!! Un Nobel en math. Tu aurais pu parler de prix Abel :-D.

    Bruno
  • Foys
    Foys
    @messiLaPulga59: On peut faire un peu plus court 
    Lemma exo: forall A B C:Prop,  (C -> (A \/ B))-> ~~ ((C -> A)\/ (C -> B)).
Proof.
intro.
intro.
intro.
intro impl_c_or_ab.
intro f.
apply f.
left.
intro c.
apply impl_c_or_ab in c.
destruct c as [a|b].
apply a.
apply False_ind.
apply f.
right.
intro x.
apply b.
Qed.

Lemma reciproque:forall A B C:Prop, ((C -> A)\/ (C -> B))->(C -> (A \/ B)).
Proof.
intro.
intro.
intro.
intro or_impl_ca_impl_cb.
intro c.
destruct or_impl_ca_impl_cb as [ica|icb].
left.
apply ica.
apply c.
right.
apply icb.
apply c.
Qed.

Lemma exo_avec_tiers_exclu: (forall P:Prop, ~~P -> P) ->  
forall A B C:Prop,  (C -> (A \/ B))->  ((C -> A)\/ (C -> B)).
Proof.
intro rpa.
intros.
apply rpa.
apply exo.
assumption.
Qed.

    NB: au lieu de "assert False (...)" utiliser simplement "apply False_ind".
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • GG
    GG
    En déduction naturelle intuitionniste :

    1) $A, C \vdash A$
    2) $A \vdash C \Rightarrow A $
    3) $A \vdash (C \Rightarrow A) \vee (C \Rightarrow B) $
    4) $B, C \vdash B $
    5) $B \vdash C \Rightarrow B $
    6) $B \vdash (C \Rightarrow A) \vee (C \Rightarrow B) $
    7) $A \vee B \vdash (C \Rightarrow A) \vee (C \Rightarrow B) $
    8) $\vdash C \Rightarrow (A \vee B)$ (hyp)
    9) $C \vdash A \vee B $
    10) $C\vdash (C \Rightarrow A) \vee (C \Rightarrow B) $
    11) $\neg C, C \vdash A $
    12) $\neg C \vdash C \Rightarrow A$
    13) $\neg C \vdash (C \Rightarrow A) \vee (C \Rightarrow B) $
    14) $(C \vee \neg C)\vdash (C \Rightarrow A) \vee (C \Rightarrow B) $

    Pour aller plus loin, il faut poser un acte de foi ! :-)
  • GaBuZoMeu
    GaBuZoMeu
    Je n'ai pas vu encore de démonstration du fait que l'implication à démontrer n'est pas un théorème intuitionniste (à part l'affirmation par Christophe du fait que le tiers exclus en est un cas particulier, qu'il pourra toujours étayer).
    En voici une démonstration sémantique, qui repose sur le fait que le treillis des ouverts d'un espace topologique satisfait toutes les règles de déduction du calcul propositionnel intuitionniste. Rappelons que l'implication est interprétée de la manière suivante : $ U\to V$ est le plus grand ouvert dont l'intersection avec $U$ est contenue dans $V$, autrement dit l'intérieur de la réunion de $V$ avec le complémentaire de $U$.
    Plaçons nous dans $\R$ avec sa topologie usuelle. Prenons pour valeur de vérité de $A$ l'ouvert $\R_+^*$, pour valeur de vérité de $B$ l'ouvert $\R_-^*$ et pour valeur de vérité de $C$ l'ouvert $\R^*$.
    Alors la valeur de vérité de $C\to (A\vee B)$ est $\R$, tandis que celle de $(C\to A) \vee(C\to B)$ est $\R^*$.
  • christophe c
    christophe c
    @GG c'est très convaincant humainement mais la tradition est de ne pas faire ton 8 comme ça. L'hypothèse il faut la garder à gauche (peu de modifications sont nécessaires dans ce que tu as écrit)

    @tous: c'est peu scolaire mais je le signale à ttes fins utiles une façon de dire "A ou B" en logique classique consiste à dire (A=>B)=>B
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Je postais de mon téléphone sans avoir vu ton post GBZM. Pardon.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Pardon aussi ça n'entraine pas le RPA (je me trompe à chaque fois faut que je soigne cette compulsion, en plus j'ai encore donné l'exercice récemment de montrer la différence entre le rpa et ci après) mais plutôt (et je ne l'ai pas prouve je vais essayer de le faire***) "pour tout X : X =>Y ou Y=>X " qui NEST PAS EQUIVALENT au rpa mais qui en est proche car par exemple vérifié par tous les anneaux intuitionnistes (île où tout elt est multiple de son carré).

    Ce n'est pas équivalent au rpa car c'est vrai dans tout ordre total (les ouverts étant les segments initiaux). Bon mais je ne veux pas dévier le fil c'était juste un amendement contre mon post d'hier.

    *** pardon l'équivalence entre les deux schémas est évidente, il n'y a rien à "essayer" :-D
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    "équivalence vérifiée par tous les anneaux..."
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    @CC, pour le 8), je n'ai fait que lire la demande de l'intervenant, et en tenir compte ! :-)

    On admet ... et on veut démontrer ...
  • christophe c
    christophe c
    De mon téléphone c'est un peu dur de détailler. Mais ce qu'on admet on le met à gauche du vdash et on le garde jusqu'à la fin et on crie eureka .

    Pour faire dans le très court un "machin vdash truc" ne signifie pas que machin implique truc mais que "ça y est msieurs dames j'ai prouvé que machin implique truc"
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    @CC,
    Si je veux démontrer que B est un théorème dans une théorie qui admet l'axiome A et l'axiome A => B, j'ai le choix :

    Je peux me placer dans un système style Hilbert-Ackermann, Bourbaki et écrire la démonstration :

    A
    A => B
    B

    Je peux aussi travailler en déduction naturelle en admettant la règle qui donne $\vdash$ X pour tout axiome X de la théorie, et montrer $\vdash B $ :

    $\vdash A$
    $\vdash A \Rightarrow B$
    $A \vdash B$
    $\vdash B$

    Il semblerait que tu refuses la règle introduction d'un axiome, et que tu écrirais seulement :

    $A, A \Rightarrow B \vdash A \Rightarrow B$
    $A, A \Rightarrow B, A \vdash B$
    $A, A \Rightarrow B \vdash B $

    Ce qui te permettrait de dire que B est un théorème d'une théorie qui admet A, A => B comme axiomes.
    Est-ce que je me trompe ?
  • christophe c
    christophe c
    Pardon pour le délai. En maths, on ne va pas en prison si on écrit un truc incorrect ou contraire à une convention, mais, les systèmes formels ont souvent des petites origines intentionnelles (dans leurs formes inoffensives) cachées.

    En calcul des séquents, je pense ne pas trahir la pensée des logiciens en t'affirmant la chose suivante:

    $$ A_1;..;A_9\vdash B$$

    est ressenti comme voulant dire :
    Il est prouvé que $(A_1\to (A_2\to (....(A_8\to (A_9\to B)))...)$.

    Donc, si on prend ta proposition de disposition, consistant à dire que tu supposes :

    $$ A\vdash B $$

    Ce sera interprété comme si GG fait l'hypothèse que l'énoncé $A\to B$ est prouvé et non pas comme si GG fait l'hypothèse que $A\to B$ est vrai.

    Or les deux choses n'ont strictement rien à voir (on peut démontrer comme je l'ai dit souvent qu'on ne pourra jamais prouver que l'une implique l'autre, ie qu'être prouvable implique être vrai, ni qu'être vrai implique être prouvable)

    Maintenant, bien entendu, on peut regarder les choses autrement et estimer, comme tu le fais que :

    $$ A_1;..;A_9\vdash B$$

    veut juste dire

    $$(A_1\to (A_2\to (....(A_8\to (A_9\to B)))...)$$

    et que le vdash et les points-virgule sont là pour l'économie d'encre. Mais ça ne me semble pas la lecture usuelle des professionnels du domaine (mais je n'ai téléphoné à personne récemment à ce sujet :-D )


    Ce n'est pas non plus la notation usuelle, mais pour économiser de l'encre, on peut aussi utiliser:

    $$(A_1 + A_2 + .. + A_9) \to B$$

    car c'est ce qui correspond le mieux au ressenti réel des gens. Hélas, cette abréviation n'a jamais été mise en officialité

    En partie à cause de la recherche qui a découvert que c'est exprimé déjà d'avance par

    $$(A_1 \otimes A_2 \otimes .. \otimes A_9) \to B$$

    ce qui fait comme l'effet des ongles frottés sur un tableau si on demande à ces gens qui ont découvert ça d'accepter de changer le signe $\otimes$ en $+$ (ils utilisent déjà le $\oplus$ pour désigner $sup$, ie le $\vee$)

    Quant à l'homme de la rue, il dit:

    $$(A_1 \ et\ A_2 \ et\ .. \ et\ A_9) \to B$$

    Et certains experts du forums ont pris l'habitude de traduire ce "et" en :

    $$(A_1 \wedge A_2 \wedge .. \dots \wedge A_9) \to B$$

    Tu vois :-D la typographie du sujet est riche!! Je pense qu'il n'y a aucun risque de voir un jour $\vdash$ utilisé pour ça (même si moi je le fais souvent, mais volontairement et dans un dessein tout à fait autre).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    A part ça, pour revenir au sujet du fil, j'en profite pour rappeler de quelle manière la logique classique est obtenue en calcul des séquents sans ajouter de fioritures ad hoc: cela consiste à garde exactement les mêmes règles que la logique intuitionnistes, mais d'autoriser une liste à droite aussi de formules (et non pas se limiter à une seule formule à droite. Quand on le fait on fait de l'intuitionnisme).

    La logique classique découle alors de ce qui suit:

    $$ \frac { \frac{A\vdash A}{A \vdash A;B} } {\vdash A; (A\to B)}$$

    qui démontre le théorème classique $[A$ ou $(A\to B)]$ (qui n'est essentiellement rien d'autre que le tiers exclus),
    dès lors qu'on accepte d'interpréter $...\vdash X;Y;..$ comme $...\vdash X\ ou\ Y\ ou\ ..$

    Par contre, attention, ce n'est pas parce que "c'est joli", et "symétrique" sur le plan visuel, que c'est justifié. J'invite donc les lecteurs à "se demander" pourquoi c'est pertinent comme système et à prouver les théorèmes qui fondent cette correction.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    @CC, pour moi,

    $A\vdash B $

    peut être interprété intuitivement par : si A est vrai, en un certain sens à préciser, alors B est vrai.

    En logique classique, "... est vrai" s'exprime en termes de valeurs de vérité, en logique intuitionniste, en termes de prouvabilité :

    Si j'ai une preuve de A, alors j'ai une preuve de B.
  • GaBuZoMeu
    GaBuZoMeu
    C'est confondre la sémantique (valeurs de vérité) et la syntaxe, ou plutôt la déduction (prouvabilité).
    Il y a aussi une sémantique pour l'intuitionnisme : celle que j'ai utilisée plus haut, par exemple.
  • christophe c
    christophe c
    @GG
    @CC, pour moi, ...

    Oui, ça, j'avais bien compris. Mais pas "pour les autres". Ce n'est pas grave, mais tout dépend si tu as envie de te faire comprendre par ceux qui entendent $\vdash$ de la manière habituelle (et non comme le "implique" que tu décris).
    En logique classique, "... est vrai" [...] , en logique intuitionniste, en termes de prouvabilité :

    Oula non !!

    Quelle que soit la logique, on applique un principe simple: les valeurs de phrases ne sont pas a priori leur statut en tant que chaines de caractères. La prouvabilité d'une phrase est en fait une propriété qui s'appelle à la chaine de caractères qui sert à l'écrire.

    On a aussi coutume de dire que la valeur de vérité d'une phrase varie dans un ensemble bien précis qu'on a choisi AVANT. Disons que certains appellent ça la séparation entre la syntaxe et la sémantique.

    Comme te le dit GBZM, dans le monde intuitionniste, les gens choisissent une topologie (la donnée d'une topologie fixe l'espace sur laquelle elle est une topologie) et ce sont les ouverts qui sont les valeurs de vérité. Et on n'a pas besoin de savoir ce qu'est une phrase pour calculer dedans. Comme tu sais, en logique classique, c'est encore plus simple, puisque l'ensemble des valeurs de vérité usuel est $\{0;1\}$ et il est doté de $\leq$ tel que $0<1$, des opérations sup et inf, ainsi que de $non$ et de tout plein d'autres (enfin 16 binaires et 4 unaires, dont 2 sans intérêt).

    Si tu veux VRAIMENT continuer de faire comme tu le dis, tout en respectant les usages, tu n'as quasiment aucun effort à faire: juste à remplacer le point virgule par "et" ou par "+" (le "+" c'est de mon cru, c'est peu usuel), préciser des règles conventionnelles de placement automatique des parenthèses invisibles, et remplacer $\vdash$ par $\to$).

    Au post suivant, je vais copier-coller ton post et remplacer.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    [large]
    Attention: la suite est un copié-collé d'un post de GG:
    [/large]

    Conventions: A et B et C veut dire (A et B) et C
    A=>B=>C veut dire A=>(B=>C)
    A=>B ou C veut dire A=>(B ou C)
    "ou" est écrit $\vee$




    GG a écrit:
    [size=medium]En déduction naturelle intuitionniste :

    1) $A\ et\ C \Rightarrow A$
    2) $A \Rightarrow C \Rightarrow A $
    3) $A \Rightarrow (C \Rightarrow A) \vee (C \Rightarrow B) $
    4) $B\ et\ C \Rightarrow B $
    5) $B \Rightarrow C \Rightarrow B $
    6) $B \Rightarrow (C \Rightarrow A) \vee (C \Rightarrow B) $
    7) $A \vee B \Rightarrow (C \Rightarrow A) \vee (C \Rightarrow B) $
    8) $ C \Rightarrow (A \vee B)$ (hyp)
    9) $C \Rightarrow A \vee B $
    10) $C \Rightarrow (C \Rightarrow A) \vee (C \Rightarrow B) $
    11) $\neg C\ et\ C \Rightarrow A $
    12) $\neg C \Rightarrow C \Rightarrow A$
    13) $\neg C \Rightarrow (C \Rightarrow A) \vee (C \Rightarrow B) $
    14) $(C \vee \neg C) \Rightarrow (C \Rightarrow A) \vee (C \Rightarrow B) $

    Pour aller plus loin il faut poser un acte de foi
    ! :-)[/size]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    A part ça, pour info, comme je l'ai déjà dit, les deux énoncés suivants sont équivalents:

    $$(1) \ \forall X,Y: [(X\to Y) \vee (Y\to X) ] $$

    $$(2) \ \forall X,Y,Z: [(Z\to (X\vee Y))\to ((Z\to X)\vee (Z\to Y)) ] $$

    il suffit de prendre $Z:=(X\vee Y)$ comme cas particulier pour voir que (2) => (1), par exemple, etc

    Aucun des deux n'est "donc plus facile à prouver que l'autre", mais le (1) est ultraconnu comme "étant proche" (mais un peu plus faible) de la logique classique qui est dû à l'axiome :

    $$ (3) \ \forall X,Y: [Y \vee (Y\to X) ] $$

    Peut-être viens-je de me répéter, je ne sais si je l'ai déjà dit.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    @GG si tu veux te faire comprendre et éviter le $\vdash$ (extrême opposée de ce que tu as fait), même pour prouver, je te traduis les règles des séquents, sans qu'il n'y ait besoin du $\vdash$.

    1) Tu peux déduire $(H_1+H_2+..+H_n + K_1+...+K_p + (A\to B)) \to C$ dès lors que tu as prouvé les deux choses suivantes:

    1.1/ $(H_1+..+H_n)\to A$
    1.2/ $(K_1+..+K_p) \to (B\to C)$



    2) Tu peux permuter les hypothèses, ie par exemple déduire $(H_1+..+H_n)\to X$ après preuve de $(H_4+H_7+H_2+...+H_3+H_1)\to X$

    3) Tu peux déduire $A\to B$ dès lors que tu as prouvé $(A+A)\to B$

    4) Tu peux déduire $(A+X)\to B$ dès lors que tu as prouvé $A\to B$

    5) Règle de coupure: tu peux déduire $X\to Y$ dès lors que tu as prouvé $(X+(Z\to Z))\to Y$

    Ma présentation n'est pas tout à faite standard, mais je la pense plus pertinente que les présentations habituelles. Elle donne les mêmes théorèmes. Par ailleurs, attention, $+$ n'est pas une opération, mais juste une commodité "dans ce post pour te parler", en ce sens que:

    $$(X_1+X_2+...+X_n)\to A$$

    est juste une abréviation de:

    $$(X_1\to (X_2\to (....\to (X_n\to A)...)$$

    Les axiomes sont les $X\to X$.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Précision: j'ai modifié le post, car du fait que $+$ n'est qu'une abréviation locale, l'habituelle règle:

    $$ \frac{\Gamma + A\vdash B}{\Gamma \vdash (A\to B)} $$

    utile quand on utilise vdash devient redondante ici, puisque (3) la couvre.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    OK, CC, ta présentation me convient.
  • GG
    GG
    @GBZM,
    Il me semblait que j'avais pris la précaution de mettre "intuitivement" en italique pour en souligner l'importance et éviter les quiproquo. Peine perdue !

    "Le point aveugle", tome 1, Jean-Yves Girard, éd. Hermann, 2006, p. 47 :

    << Un séquent est écrit avec des énoncés, le symbole "thèse" $\vdash $, ainsi que des virgules. La signification intuitive du séquent $\Gamma \vdash \Delta$ est "si tous les éléments de $\Gamma$ sont vrais, alors un des éléments de $\Delta $ est vrai". On voit donc que:

    - La virgule gauche signifie "et".
    - La virgule droite signifie "ou" ; elle n'est pas utilisée dans le cadre intuitionniste (voir chapitre suivant).
    - Le signe $\vdash $ signifie "implique".

    One remarquera que je n'ai pas utilisé les symboles logiques pour la conjonction, la disjonction, l'implication. En effet, cette explication n'est pas limitée à la logique classique ou intuitionniste ; elle fonctionne aussi en logique linéaire, [ ...] >>

    Girard confond-il aussi sémantique et syntaxe ?!

    Bon, je plaisante, faut-il le préciser ! :-)
  • GaBuZoMeu
    GaBuZoMeu
    Il ne mélange pas, comme tu le fais, "valeurs de vérité" et "prouvabilité".
  • GG
    GG
    Il dit :

    La signification intuitive du séquent $\Gamma \vdash \Delta$ est "si tous les éléments de $\Gamma$ sont vrais, alors un des éléments de $\Delta $ est vrai".

    À ton avis, à quoi fait-il allusion lorsqu'il dit : "intuitivement, l'élément ... est vrai"

    d'une part en logique classique,
    et d'autre part en logique intuitionniste ? (l'explication est donnée pour les deux logiques)
  • GaBuZoMeu
    GaBuZoMeu
    "Vrai" fait référence à une sémantique.
    "Prouvable" fait référence à un système de déduction.
    Je répète puisque tu as l'air de bloquer là-dessus, tu mélangeais les deux dans ton message.
    Je ne vois nulle part que Girard affirme que "en logique intuitionniste, "vrai" s'exprime en termes de prouvabilité", comme tu l'as écrit. C'est ce que tu lis chez Girard ?
  • GG
    GG
    Et ma question ? Pour autant que tu lui trouves un sens, naturellement ..
  • christophe c
    christophe c
    De mon téléphone : @GG , attention l'un des grands buts officiels et assumés de JYG est justement de créer un système où syntaxe et sémantique ne font plus qu'un. C'est un euphémisme de dire que ce n'est pas la meilleure référence classique pour les exactitudes de vocabulaire de base (si en plus on ajoute à ça sa volonté de provoquer). Par ailleurs quand on écrit des milliers de pages, on ne dit pas forcément t à chaque ligne tous les mots nécessaires. Il ne visait pas forcément le point qu'on discute en écrivant rapidement ce que tu cités mais probablement avait-il juste en tête de signaler que les points virgule à droite du vdash sont des "ou" et rien de plus (comptant sur la suite pour évacuer les imprécisions de perception)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    OK, merci CC.
  • christophe c
    christophe c
    @GG, avant de me déconnecter, je te laisse quelques chtites précisions sloganiques qui t'aideront peut-être.

    Dans une extrapolation de ce qui se passe avec la logique classique où :

    la sémantique est $F_2:= \Z/2\Z$ muni de ses opérations habituelles et où la syntaxe est l'ensemble des phrases vues comme suites de caractères pour laquelle on recherche (et a trouvé) des règles "pour enfants" de déduction permettant d'assurer la complétude (ie une phrase est prouvable ssi sa négation n'a pas de modèle, un modèle étant un morphisme dans la 'ensemble structuré des phrases dans $F_2$;

    des couples (Une sémantique, Une logique qui va avec) se sont développés.

    Effectivement le plus vieux couple né après le couple $(F_2, LogiqueClassique)$, est le couple $(SemantiqueDeLintutionnisme, LogiqueIntuitionniste)$.

    Comme te l'a signalé GBZM, Comme $SemantiqueDeLintutionnisme$ on peut prendre certaines topologies qui marchent bien à elles toutes seules ou même "la topologie en général". Un modèle intuitionniste est simplement un morphisme de l'ensemble des phrases vers une topologie (avec ses opération d'union, etc)

    D'une manière générale, un truc caché qui pollue les deux paradigmes précédents est que l'on veut voir l'implication comme adjointe de la borne inférieure dans un ordre, ie on veut que l'opération $\to$ ait comme propriété que:

    $$ \forall x,y,z: [(x\leq (y\to z)) \iff ((inf(x,y))\leq z)]$$

    ce qui a conduit à ne découvrir que très tard (JYG est un grand acteur de la découverte et la promotion en question) que c'était une mauvaise idée. En gros le côté "ordre" (ou catégorie, si tu veux, ce qui revient au même) pose un problème. Sur google en tapant Stone et en fouillant un peu tu verras que tout ce paradigme repose sur le fait que la notion d'ordre nous habite très profondément: un ordre étant (à isomorphisme près), une partie de $P(X)$ que l'on considère comme ordonnée d'office par l'inclusion, en prenant:

    1/ la topologie engendrée, tu obtiens une sémantique intuitionniste (on appelle ça une algèbre de Heyting, et on pourrait s'mauser à créer un néologisme disant qu'on a Stono-Heytingisé l'ordre)

    2/ En virant de plus, les ouverts qui ne sont pas l'intérieur de leur adhérence, on obtient une sémantique pour la logique classique (une algèbre .. de Boole, ie un truc non intègre dont tous les quotient intègres deviennent des $F_2$). Et avec le même jeu de noélogismes, on pourrait dire qu'on a Stono-booleanisé l'ordre.

    Remarque: c'est (2) ci-dessus qui a permis de faire exploser les astuces de forcing (menant à la découverte d'une foison d'indécidables non soupçonnables si on s'était tenu aux techniques autoréférentes de Godel).

    Plus récemment, j'en ai parlé dans d'autres fils, on a découvert un truc bien plus conforme à nos démarches de recensement de tout ce qu'on suppose quand on fait de la science. Pour ça faut renoncer à Stono-quelquechosifier un ordre.

    A l'arrivée (il faudrait écrire des centaines de pages), on obtient la petit structure générale que j'ai déjà postée sur le forum, qui peut servir de sémantique très générale (qui est disons à mi-chemin entre syntaxe et sémantique si on veut prononcer des mots snobs), je te le redonne:

    Un triplet $(E,\leq, \phi,1)$ avec $\phi: E^2\to E$ et $\leq$ un ordre sur $E$ tel que, pour tous $x,y,z$ dans $E$:

    1/ $\phi$ est décroissante à gauche et croissante à droite
    2/ $\phi(1,x) = x$
    3/ $\phi(x,\phi(y,z)) = \phi(y,\phi(x,z))$
    4/ $x\leq y$ si et seulement si $1\leq \phi(x,y)$

    Puis il te suffit de noter $x\Rightarrow y$ (ou $x\to y$ ou $x\multimap y$) à la place de $\phi(x,y)$ et de chercher à prouver des théorèmes de la forme $1\leq expression$ pour t'amuser à faire de la "bonne logique" :-D

    Faire de la logique intuitionniste ou classique c'est "essentiellement" ajouter le très violent :

    $$ \forall x,y\in E: \phi(x,y) = \phi(x,\phi(x,y)) $$

    voir aller jusqu'à demander $x\leq \phi(y,x)$

    aux propriétés demandées 1 à 4.

    Attention: "sortir de la sémantique pour aller vers la syntaxe" consiste en une essentielle seule chose: renoncer à la propriété (2) (même si ce n'est pas la seule qui empêche la liberté (au sens groupe libre) de la structure.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 20

CidrolinGGLucasbiguine_equationjean-éricjelobreuilodile0502 +13 Invités