Loi de l'exportation

Pierrreg · October 2017

Bonjour

La loi de l'exportation (Exportation logique ), nous dit : $$ (P\Rightarrow(Q\Rightarrow R)) \Leftrightarrow (P\wedge Q\Rightarrow R)
$$ À-toi maintenant : $$
(P\Rightarrow(Q_1\Rightarrow R_1 \wedge Q_2\Rightarrow R_2)) \Leftrightarrow (P\wedge Q_1\Rightarrow R_1)\wedge (P\wedge Q_2\Rightarrow R_2)$$
[Activation du lien. AD]

Foys · October 2017

Quelques remarques: si $X$ est un énoncé et si $\Gamma$ est un ensemble (au sens intuitif, on pourrait aussi prendre une liste, etc) d 'énoncés, $\Gamma \vdash X$ se lit "$X$ est prouvable sous les hypothèses $\Gamma$ (si $\Gamma$ est vide, $X$ est alors un théorème de logique, et "$\vdash X$" est l'abréviation de $\emptyset \vdash X$).

On fixe un ensemble d'énoncés $\Gamma$ dans le paragraphe qui suit et $X,Y$ des énoncés quelconques:
-$\Gamma\cup \{X \} \vdash Y$ si et seulement si $\Gamma \vdash X\to Y$.
-si $\Gamma \vdash X'$ et $\Gamma \vdash X'\to Y'$ alors $\Gamma \vdash Y'$.
-$\Gamma \vdash X$ et $\Gamma \vdash Y$ si et seulement si $\Gamma \vdash X\wedge Y$.
-$X\wedge Y\vdash X$ et $X\wedge Y \vdash Y$.

Enfin, $X\leftrightarrow Y$ est l'abréviation de $(X\to Y) \wedge (Y \to X)$.

Avec ça tu as tous les ingrédients en main pour établir que :
$$\vdash (P \to ((Q_1 \to R_1) \wedge (Q_2 \to R_2))) \leftrightarrow (((P\wedge Q_1) \to R_1)\wedge ((P \wedge Q_2 )\to R_2))$$

pldx1 · October 2017

On part de
$$exo2:= (P\Rightarrow(Q_1\Rightarrow R_1 \wedge Q_2\Rightarrow R_2)) \Leftrightarrow (P\wedge Q_1\Rightarrow R_1)\wedge (P\wedge Q_2\Rightarrow R_2)$$
Et on applique

SubstituteAll(exo2, "Rightarrow","&ply"): 
SubstituteAll(%, "wedge","&xet");
SubstituteAll(%, "Leftrightarrow","&equi");
SubstituteAll(%, "Q_1","Q1"): 
SubstituteAll(%, "Q_2","Q2"):
SubstituteAll(%, "R_1","R1"): 
exo3:= SubstituteAll(%, "R_2","R2");

On obtient un truc foireux... parce que l'expression initiale est mal parenthésée. On fait donc de son mieux, conduisant à

$$exo2:= (P\Rightarrow((Q_1\Rightarrow R_1) \wedge (Q_2\Rightarrow R_2))) \Leftrightarrow ((P\wedge Q_1\Rightarrow R_1)\wedge (P\wedge Q_2\Rightarrow R_2))$$ et à:

exo3= "(P&ply((Q1&ply R1) &xet (Q2&ply R2))) &equi ((P&xet Q1&ply R1)&xet (P&xet Q2&ply R2))"

On prononce alors les mots magiques:

(rul@eval@parse)(exo3);

Et on obtient $1$ comme résultat (les fonctions ply, xet, equi, rul ont été définies dans un fil précédent).

Ben voilà, c'est fini.

Cordialement, Pierre.

Pierrreg · October 2017

Merci pour les réponses!
(Je ne sais pourquoi, mais dans chrome, je vois des barres verticales sur les formules à droite, quand c'est écrit en latex. Ca rend la lecture pénible)

Rescassol · October 2017

Bonjour
Sur une expression en $\LaTeX$, Bouton de droite, Math Settings, Maths Renderer, SVG.
Cordialement,
Rescassol
http://www.les-mathematiques.net/phorum/read.php?32,1204455,1209141#msg-1209141

pldx1 · October 2017

A propos des barres noires.
http://www.les-mathematiques.net/phorum/read.php?8,766530,766766#msg-766766
Autrement dit: lorsqu'un site est sous-administré, son administration s'en ressent. Et il est rare qu'il y ait une amélioration spontanée.
Cordialement, Pierre.

[Lorsqu'un intervenant est acariâtre, il est rare qu'il y ait une amélioration spontanée. Cordialement, AD]

Pierrreg · October 2017

Donc, si j'ai:
$(p\Rightarrow (q\Rightarrow r))=((p\wedge q)\Rightarrow r)= ((q\wedge p)\Rightarrow r)=(q\Rightarrow (p\Rightarrow r))$

on a donc: $p\Rightarrow (q\Rightarrow r)=q\Rightarrow (p\Rightarrow r)$

mais on n'a pas:

$q\Rightarrow (p\Rightarrow r)=(q\Rightarrow p)\Rightarrow r$

Loi de l'exportation

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 17