Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les logiques : notes en vrac
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Sam 2 Mai 2020 17:48
Message Re: Les logiques : notes en vrac
Le sujet est sur les logiques, sur ce thème en particulier. Pourtant, dans certains précédents messages et peut‑être d’autres à venir, j’ai parlé de choses mathématiques plus en générale et sans directement de rapport avec les logiques. Il y a à cela, trois raisons. La première est que la manière la plus courante de donner une sémantique à une théorie logique, passe par des interprétations et des modèles, les interprétations étant mathématiquement définies et les modèles, typiquement aussi, même si ce n’est pas une obligation (c’est quand‑même alors moins commode et moins fiable). La seconde raison est que les interprétations et modèles nécessitent par leur nature, d’aborder les objets mathématiques en générale. La troisième raison relie les deux précédentes et le sujet des logiques en générale : il existe une notion dans les mathématiques, nommée structures, qui est une manière d’aborder les objets mathématiques avec des définitions initiales explicites et un ensemble d’axiomes, une approche formellement logique. Les structures peuvent être utiles autant pour aborder les interprétations et modèles qui donnent un sens à une logique, que pour avoir une approche vraiment logique des mathématiques. Il faut quand‑même noter que les structures sont plus un concept qu’un objet totalement défini ; ce sont plutôt les types de structures, chacun en particulier, qui ont des définitions entièrement posées.

Pour une introduction aux structures, voir cette page, par exemple : Mathematical structures (abstractmath.org).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Dim 3 Mai 2020 00:36
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Une subtilité à ne pas perdre de vue avec les fonctions.

f : A → B doit être lu comme « le domaine de f est égal à A, le codomaine de f est inclus dans B ».

Personnellement, je l’avais oublié, j’avais tendance à le lire comme «  …, le codomaine de f est égal à B ».

Les anglophones font une distinction bien venue, qu’on ne fait pas en français : ils distinguent codomain et range. Le codomain, c’est le codomaine en français, c’est à dire l’ensemble d’arrivé déclaré pour la fonction, et le range, c’est l’ensemble d’arrivé effectif. Malheureusement, il n’y a pas de traduction appropriée de ce terme en français. Le mot se traduirait habituellement par interval, mais l’interval est un ensemble continue entre deux bornes (incluses ou exclues), ce que n’est pas nécessairement l’ensemble d’arrivé effectif d’une fonction. En fait, en Anglais, range peut désigner deux choses différentes : l’ensemble d’arrivé effectif d’une fonction, et un ensemble de valeurs continues entre deux bornes, l’interval en français ; le contexte résous normalement l’ambiguïté et la notation encore plus sûrement.

Plus que de ne pas avoir de bonne traduction en français, il semble que dans le monde francophone, le distinction n’est même pas faite du tout, que personne ne remarque que l’ensemble d’arrivé déclaré n’est pas nécessairement l’ensemble d’arrivé effectif, celui‑ci pouvant pourtant être plus restreint.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Dim 3 Mai 2020 15:04
Message Re: Les logiques : notes en vrac

Différences entre → , ↦ et ⇒


Enfin une réponse assez certaine à la question de la différence entre → et ↦ et ⇒, et aussi à propos de ↔ et ⇔. Malheureusement, le symbole ⇒ en particulier, devra toujours être sujet à précaution, même après ces clarifications. Les symboles ⊢ et ⊨ , seront le sujet d’un autre message.

Ce message est long, verbeux ; je suis conscient que la verbosité ne facilite pas la lecture, mais il n’est pas possible de faire autrement pour lever toutes ambiguïtés au sujet de ces notations : si nécessaire, relire plusieurs fois, sans se laisser stresser.

Ce qui est dit dans ce message, est conforme à l’usage courant et au standard ISO 80000-2. Ce standard ISO, qui est à propos des poids et mesures, mais qui par nécessité standardise certaines notations mathématiques plus générales, ne dit rien de → pour les logiques et ne mentionne pas du tout ↔ ; il n’en dit rien, ce qui ne doit pas être compris autrement.

→ a deux utilisations concernant les logiques [1] : dans la définition du type d’une fonction et dans une expression comme connecteur, c’est à dire comme opérateur. Ex. dans la définition du type d’une fonction : ℕ → ℕ. Ex. dans une expression logique, comme opérateur : a → b où l’évaluation ne produit pas nécessairement la valeur vraie.

Ne pas oublier que la proposition ou la formule P → Q peut être vraie ou fausse (⊤ ou ⊥) ; en particulier, avoir posé P → Q ne permet pas automatiquement d’en conclure quelque chose (sinon il suffirait d’écrire une proposition pour la démontrer et on pourrait démontrer comme vraie, n’importe quelle proposition, en une seule étape, y compris des propositions fausses). Par « ne permet pas automatiquement », il ne faut pas non‑plus comprendre « ne permet pas », mais c’est alors sous condition que P → Q soit toujours vraie.

↦ n’a qu’une utilisation : dans la définition de la correspondance d’une fonction, ce qui est différent de la définition du type de la fonction. Ex. x ↦ x + x.

Concernant les fonctions, pour ne pas oublier la différence entre les deux : f: D → C et f: x ↦ t(x). Un exemple de domaine D serait ℕ, un exemple de codomaine C serait ℝ, un exemple de terme t serait x + x. Pour décrire le rôle de t dans f: x ↦ t(x), la formulation en Anglais est “ defining term denoting the value of f for the argument x ”. En résumé, → est utilisé pour noter le type de la fonction, tandis que ↦ est utilisé pour noter la valeur de la fonction. À moins que t ne soit un constructeur de type (ignorez si vous ne comprenez pas), c’est une erreur d’écrire f: x → t(x) ; on peut le voir parfois, mais c’est une erreur quand‑même, la présence ou pas de la petite barre verticale sur le bout gauche de la flèche, distingue les deux symboles qui ne sont pas interchangeables.

⇒ n’est utilisé qu’en logiques pour ce que j’en ai vu ; c’est au minimum une erreur de l’utiliser pour noter le type ou la correspondance d’une fonction, mais ce n’est pas une erreur de l’utiliser pour noter une propriété ou une contrainte d’une fonction, ce qui n’est pas la même chose. Un exemple du dernier cas, serait f(x) = y ⇒ x = g(y), qui signifie que g est la réciproque de f (pour dire que g est la réciproque de f et que f est le réciproque de g, il faudrait écrire f(x) = y ⇔ x = g(y) ), Cet usage est conforme au standard ISO, il faut le noter pour comprendre ce qui suit.

Le symbole logique ⇒ est malheureusement moins standardisé que →. Il est tantôt utilisé à la place de →, tantôt utilisé avec et distinctement de →. C’est le contexte qui permet de dire comment ⇒ est utilisé, si il l’est.

Quand le symbole ⇒ est utilisé à la place de →, alors → n’est pas utilisé  ou alors pour autre chose que les propositions, par exemple pour noter des types de fonctions comme décrit précédemment.

Quand le symbole ⇒ est utilisé avec et distinctement du symbole → (comme symbole logique, ici), il est une proposition sur une proposition : P ⇒ Q se lit alors comme P → Q est toujours vraie, inconditionnellement vraie, ce qui doit être produit par une démonstration.

Le second cas est préférable au premier, vu l’usage qui est fait de ce symbole dans le standard ISO 80000, où P ⇒ Q doit se lire comme toujours vraie. Bien qu’en usage occasionnel, le premier cas, où ⇒ est un synonyme de → , c’est à dire où P ⇒ Q n’est pas nécessairement vraie, est à éviter pour éviter les mauvaises interprétations.

Quand le symbole logique → est utilisé seul, sans que le symbole ⇒ n’apparaisse jamais, il est utilisé comme décrit précédemment ; en soulignant en particulier que quand par exemple P → Q apparaît comme prémisse d’une dérivation (comme prémisse, et non‑pas seulement dans une prémisse), ça signifie qu’on se place dans un contexte où P → Q est toujours vraies, mais, et pour répéter ce qui a été dit précédemment, quand P → Q apparaît comme une proposition, elle peut être vraie ou fausse.

Dans tous les cas, que ⇒ soit utilisé seul ou avec et distinctement de → , il est préférable de définir son interprétation au préalable et bien explicitement. Par exemple poser que A ⇒ B signifie que A → B est inconditionnellement vraie (ce qui ne se pose pas arbitrairement [3]). Écrire A ⇒ B ≝ (A → B) = ⊤, ne suffirait pas, la proposition qu’est le terme de droite, pouvant toujours être vraie ou fausse : à moins que ce ne soit une tautologie, on ne peut pas forcer une proposition à être vraie, on peut seulement éventuellement démontrer qu’elle est vraie. Le symbole ≝ signifie « égale par définition  », conformément à un usage courant et au standard ISO 80000-2.

Dans tous les cas, le symbole ⇔ doit devoir se comprendre comme dans cette égalité : A ⇔ B = (A ⇒ B ∧ B ⇒ A), c’est à dire A → B ∧ B → A est inconditionnellement vraie (ce qui, là aussi, ne se pose pas arbitrairement [3]). Dans tous les cas, le symbole ↔ doit devoir se comprendre comme dans cette égalité : A ↔ B = (A → B ∧ B → A). Ceci (les deux phrases), que ce soit par définition ou par dérivation [2]. Le symbole ∧ apparaissant dans les deux premières phrases, signifie et, à ne pas confondre avec le symbole ∨ qui signifie ou inclusif.


Codes Unicode des symboles définis dans ce message :

  • → est U+2192
  • ↦ est U+21A6,
  • ⇒ est U+21D2
  • ↔ est U+2194
  • ⇔ est U+21D4
  • ≝ est U+225D
  • ∧ est U+2227
  • ∨ est U+2228


[1] Concernant les mathématiques en général, d’après le standard ISO 80000-2, → a au moins ces autres usages : pour dire qu’une valeur tend vers une autre, pour dire qu’une fonction est appliquée, et dans ce cas là, le nom de la fonction est écrit un peu au dessus du trait horizontal de la flèche, puis pour les vecteurs, et dans ce cas là, la flèche est écrite au dessus de la valeur du vecteur, qui peut être un nom ou une expression. Mais ces usages peuvent être oubliés quand on ne s’intéresse qu’aux logiques. Pour rappel, le standard ISO ne dit rien sur l’utilisation de → en logiques.

[2] ⇔ et/ou ↔ peuvent être posés par définition ou par une table de vérité qui permettrait de conclure l’égalité mentionnée. Le résultat doit être le même dans les deux cas, l’égalité mentionnée dans le paragraphe, doit toujours être vraie, sans quoi l’écriture utilisée sera probablement mal lue.

[3] À moins qu’on ne pose un axiome, mais poser un axiome est une option risquée qui doit rester exceptionnelle — hors cas particuliers.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Dim 3 Mai 2020 22:55
Message Re: Les logiques : notes en vrac

Différence entre algèbre de Bool et logique des propositions


Note № 1 : logique des propositions et calcul des propositions, sont synonymes, mais je préfère l’appeler logique des propositions, comme le propos ici est de souligner la différence entre calculs en générale et démonstrations en particulier.

Note № 2 : le symbole normalement utilisé pour la négation logique, est mal rendu par la police de caractères du forum, il a donc été remplacé par, juste “ not ”, mais il ne faut pas le prendre pour une écriture standard.

La logique des propositions, souvent assimilée à la logique classique [1], donc considérée comme élémentaire et donc simple, par effet du vocabulaire, est parfois confondue avec l’algèbre de Bool, vraiment plus « simple » ; de même par contamination, la notion de proposition est parfois confondue avec celle d’expression Booléenne.

Il y a de bonnes mauvaises‑raisons à cette confusion : on y retrouve les mêmes opérateurs, les deux ont des domaines d’interprétation « équivalents » : vrai et faux, quelque soit la représentation symbolique de vrai et faux. On peut dire que l’algèbre de Bool est un modèle de la logique des propositions, c’est à dire que l’algèbre de Bool peut être une interprétation de la logique des propositions : ce qui est valable dans la logique des propositions, l’est toujours dans l’algèbre de Bool et on peut représenter une expression Booléenne par une proposition.

L’algèbre de Bool pouvant évaluer une expression en appliquant des calculs simples à réaliser, même si souvent fastidieux, on peut légitimement se demander pourquoi distinguer les deux, pourquoi faire compliqué quand on pourrait faire simple.

La différence tient dans ce qu’est un calcul et ce qu’est une démonstration. Une démonstration (qui produit une preuve) est un calcul, mais les calculs ne sont pas toujours des démonstrations et surtout, leurs résultats pas toujours des preuves.

Considérons qu’on tient l’algèbre de Bool pour la même chose que la logique des propositions. Prenons un cas en apparence trivial comme (not a ∨ a). Si on a lit comme il se doit, « soit non a soit a », cette expression est évidemment toujours vraie. Comment démontrer ça dans l’algèbre de Bool ? Une idée serait de dire (not a ∨ a) = true. Le seul problème pour le moment, qui n’est rien en comparaison du suivant, c’est qu’il n’y a pas d’opérateur = dans l’algèbre de Bool. Mais il y a le ↔ , qui est équivalent. Soit, alors posons (not a ∨ a) ↔ true. Ça a déjà moins d’allure, l’expression a déjà moins l’air d’avoir un status spécial, parce que en effet, cette expression n’a rien de spécial, pas plus d’ailleurs que (not a ∨ a) = true. On sait que b ↔ c est équivalent à (b → c) ∧ (c → b) qui se réduit à (not b ∧ not c) ∨ (b ∧ c). Remplaçons donc b par (not a ∨ a) et b par true, pour appliquer l’égalité souhaité plus haut, à cette représentation de l’égalité :  (not (not a ∨ a) ∧ not true) ∨ ((not a ∨ a) ∧ true), soit (not (not a ∨ a) ∧ false) ∨ ((not a ∨ a) ∧ true), soit false ∨ ((not a ∨ a)), soit (not a ∨ a), on est revenu au point de départ. On a pas avancé, on a rien démontré. Pourtant l’application de la table de vérité à (not a ∨ a), dit bien que cette expression vaut toujours true. Le mieux qu’on puisse faire, est de la remplacer alors par true ; nous ne sommes par revenu au point de départ, mais notre expression d’origine n’est plus, elle s’est évanoui, disparue, ce qui est un problème peut‑être encore plus grave. Car que signifie ce true qui ne se distingue pas de n’importe quel autre true ? Il ne signifie rien d’autre que lui‑même; il est juste la valeur de notre expression, notre expression d’origine, qui est toujours vraie, n’est en fait qu’une représentation de true, et ce true n’est pas une représentation du fait que (not a ∨ a) est toujours vraie. On souhaiterait plutôt en fait, noter que cette expression est toujours vraie, et en le disant, on comprend déjà que cette opération, n’est pas une opération Booléenne, que cette opération se fait au delà de l’algèbre de Bool ; nous y reviendrons avant la fin.

Posons cette expression Booléenne comme une proposition, elle aura toujours la même écriture, (not a ∨ a), et là, ça va aller vite : si on se place dans le contexte de la logique classique des propositions, nous disposons de la règle de dérivation qu’est le tiers exclu qui n’a même pas besoin de prémisse pour prouver notre expression, en une phrase :

∴ (not a ∨ a)

Ici, le ∴ représente la même chose que le grand trait horizontal qu’on retrouve dans les preuves. Si on avait eu besoin d’une prémisse, elle aurait été écrite avant le ∴ , ce qui aurait été comme l’écrire au dessus du grand trait horizontal dans l’écriture plus courante.

Où est la différence ? Dans le fait que ∴ (not a ∨ a) n’est pas une expression Booléenne ni même une proposition, c’est une conclusion. N’étant ni expression Booléenne ni une proposition, cette représentation n’a pas de valeur true ou false, elle s’interprète comme toujours vraie. N’étant pas une expression, elle ne peut pas être utilisée dans un calcul, on ne peut pas écrire par exemple (∴ (not a ∨ a) ↔ true), qui ne serait pas une proposition valide, ni non‑plus une expression Booléenne valide. La phrase ∴ (not a ∨ a) ne représente pas une valeur parmi {false, true}, elle représente une conclusion, elle est tout‑court, ce qui compte, c’est par quels tuyaux elle a put passer.

Si x et y sont deux nombres, l’éventuelle preuve que x > y est toujours vrai, n’est pas un nombre. De même, si P est une proposition dont la valeur est Booléenne, la preuve que P que P est toujours vraie, n’est pas un Booléen, malgré que le même mot s’utilise pour désigner le vrai Booléen (au sens de qui est Booléen) et le vrai de la preuve.

Une expression d’un calcul, ne se réduit qu’à une expression du domaine du calcul, une expression qui peut être la plus simple, comme true ou false ou un nombre. Si l’expression se réduit à ça, alors c’est ce qu’elle représente. De même que 1 - 1 est une représentation de zéro, mais n’est pas une preuve que 1 - 1 = 0, parce que cette preuve, qui doit évidemment exister, n’est pas un nombre, et ce 0 n’a pas un status différent du false ou true de l’algèbre de Bool.

Avec les nombres, la confusion n’est pas faite, parce qu’il est évident qu’une preuve et un nombre ne sont pas du même type. Mais avec les proposition, surtout quand existe l’algèbre de Bool, la confusion est facile à faire, comme le domaine des deux semble similaire, par une apparence trompeuse, celle que le vrai de l’un est égale au vrai de l’autre, mais ça n’est pas plus correcte que de croire que vrai est un nombre, même s’il existe une interprétation du vrai et faux Booléen comme des nombres (canoniquement, le fameux true = 1, false = 0). Dans la logique des proposition, le vrai d’une proposition n’est pas plus du même type que le vrai d’une preuve, qu’un nombre n’est du même type que le vrai d’une preuve. Malgré les même noms, il existe justement des symboles distincts pour les distinguer. Le vrai d’une preuve, se note ⊤, le faux d’une preuve se note ⊥, ils appartiennent à l’ensemble {⊥, ⊤}, qui ne se confond pas avec un autre, même on peut faire des correspondance avec {false, true} ou {0, 1} (oui, là aussi), ça n’en fait pas des choses du même type, même si on peut parfois interpréter l’une comme l’autre. Et il ne faut surtout pas utiliser ces symboles ⊥ ⊤ dans l’algèbre de Bool !

La confusion serait moins fréquente, si ⊤ et ⊥ étant plus souvent utilisés au lieux de true et false ou vrai et faux, pour les preuves ; mais ça n’empêcherait pas la confusion non‑plus.

Une autre raison de la confusion, est que pour faire la preuve d’une chose, il faut que cette chose soit toujours vraie. C’est aussi le cas de 5 > 4, qui est vrai, mais c’est un vrai du type Booléen, là aussi (la relation d’ordre sur les entiers naturels est une fonction du type ℕ → B, le domaine et le codomaine sont très différents, ça peut surprendre, mais c’est normal).

Il faut comprendre par là, qu’il est souvent facile de prouver P , si P peut se réduire à true Booléen, mais comme le true des preuves n’est pas le true Booléen, ça n’est pas automatique. Il faut plus que pouvoir réduire P à true Booléen façon algèbre de Bool, il faut que P soit tenue pour vraie façon preuve. Et il se trouve que les règles de l’algèbre de Boole et des preuves, ne sont pas toujours les mêmes, même si elles se ressemblent beaucoup, ce qui favorise encore la confusion.

Je disais plus haut, que not a ∨ a est en apparence trivial à prouver. Oui dans la logique classique des propositions, mais pas dans la logique intuitionniste des proposition, qui est justement célèbre pour ne pas inclure le tiers‑exclus (excluded‑middle, en Anglais).

Un long épilogue, parce qu’en de plus résumer l’essentiel, il y a encore beaucoup à expliquer et à développer.

En résumé (si besoin, relire plusieurs fois ce qui précède, plus tard) : les démonstrations sont des calculs, mais les calculs ne sont pas toujours des démonstrations. Un calcul se fait sur des termes qui ont une valeur dans le domaine du calcul. Parfois, les termes d’un calcul se réduisent à une valeur littérale du domaine du calcul, comme un nombre, un Booléen, ou même autre chose (le monde des objets mathématiques est vaste, ils inventent de ces étrangetés …). Une démonstration est un calcul qui se fait dans le domaine {⊥, ⊤}, le domaine des preuves (on peut dire que ces deux symboles sont du type preuve). On ne peut pas faire passer true ou 1 pour ⊤, aucune démonstration ne pourra en faire quelque chose (ou pas directement). Bien qu’une démonstration soit un calcul, sémantiquement, elle ne réduit pas vraiment une expression à ⊥ ou ⊤, sa sémantique est plutôt d’attacher cette valeur comme propriété d’une expression, et cette expression est conservée, … pour ne pas perdre le sens qu’elle porte ! Si la valeur ⊥ est attachée comme propriété à une expression, comme aboutissement d’un calcul de démonstration, alors l’expression est interprétées comme irréalisable ou impossible ou incohérente, selon la logique. Si la valeur ⊤ est attachée à une expression, comme aboutissement d’un calcul de démonstration, alors l’expression est interprétée comme réalisable, possible, ou cohérente, selon la logique. Chaque logique à son interprétation de ⊥ et ⊤, qui sont du type propre à leur logique, on ne peut pas les inter‑changer non‑plus. Chaque logique a ses propres règles de calcul [2], souvent plus restreintes que les règles de l’algèbre Booléen, parce que l’interprétation de ces logiques portent sur des choses soit différentes, soit plus concrètes et que certaines réalités, celles du monde ou d’autres objets mathématiques, ne sont pas toujours vraie quand pourtant une expression Booléenne qui pourrait les représenter est vraie dans le calcul Booléen (comme le tiers exclus, déchus en logique intuitionniste, un exemple célèbre, mais pas le seul) : les démonstrations dans ces logiques peuvent être exigeantes sur les faits ou les faits sont plus complexes et nécessitent des règles d’inférence spécifiques. Ex. la notion de fonction renvoyant une fonction, ne peut pas être exprimée d’une quelconque manière dans la logique classique des propositions ou dans une logique comparable à l’algèbre de Bool. C’est précisément parce que les règles du calcul des deux ne sont pas les mêmes, que les interprétations ne sont pas les mêmes, que le résultat de ces calculs ne sont pas interchangeables, que le vrai et le faux de la preuve dans une logique donnée, n’est pas nécessairement équivalent au vrai et au faux Booléen.


Une nécessité de précaution avec les axiomes, découle de ce qui a été expliqué ici : ajouter un axiome à une logique, est équivalent à modifier les règles du calcul des preuves dans cette logique, et donc à en faire une autre logique, et donc probablement à modifier aussi la bonne interprétation des preuves qu’elle produit. En reprenant le vocabulaire utilisé précédemment, c’est courir le risque de prendre un ⊤ d’un certain type, pour un ⊤ d’un autre type.


[1] En notant qu’un calcul des propositions, n’est pas toujours une logique classique. La logique intuitionniste est une logique des propositions, mais n’est pas une logique classique.

[2] Qui sont des règles d’inférence ou des axiomes ou les deux. Il est toujours possible d’ajouter des axiomes à une logique, mais c’est dangereux, parce que c’est courir le risque de lui faire perdre ses propriétés sémantiques. Par exemple, on peut réintroduire le tiers‑exclus par mégarde, dans la logique intuitionniste, en ajoutant un axiome dont on ne sait pas qu’il implique le tiers‑exclus (la loi de Pierce en fait partie, raison pour laquelle elle n’est jamais être ajoutée comme axiome en logique intuitionniste).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Lun 4 Mai 2020 01:05
Message Re: Les logiques : notes en vrac

Les axiomes de la logique intuitionniste et de la logique classique


Note № 1 : formellement, il faut lire « logique intuitionniste des propositions » et « logique classique des propositions ».

Note № 2 : comme dans le précédent message, le symbole ∴ est utilisé en lieu et place du grand trait du séquent.

D’après Propositional Intuitionistic Logic (mi-ras.ru) [PDF], Stepan Kuznetsov, 2012.

Les dix règles d’inférence de la logique intuitionniste des propositions :

∴ ⊥ → A
∴ (A ∧ B) → A
∴ (A ∧ B) → B
∴ A → (A ∨ B)
∴ B → (A ∨ B)
∴ A → (B → A)
∴ A → (B → (A ∧ B))
∴ (A → (B → C)) → ((A → B) → (A → C))
∴ (A → C) → ((B → C) → ((A ∨ B) → C))
A, (A → B) ∴ B

Pour obtenir la logique classique des propositions, il suffit d’ajouter une onzième règle d’inférence, qui change l’interprétation, donc le type des preuves [1] :

∴ A ∨ not A


[1] Une conclusion de la logique intuitionniste, peut être utilisée (en la posant comme axiome par exemple) en logique classique, mais l’inverse ne devrait pas être fait.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Mer 6 Mai 2020 16:06
Message Re: Les logiques : notes en vrac

Le monde des mathématiques et son problème de communication


Un problème que les mathématique sont seuls à connaitre, ce problème n’existant pas avec la biologie, la chimie, la physique, l’histoire, etc.

Non‑seulement le sens des mots en mathématiques est typiquement trop loin de leurs sens courants, ce qui induit inévitablement en erreur pendant longtemps, en plus, la plupart des mots, en dehors des plus élémentaires, n’ont souvent en fait simplement pas de définition claire, mécaniquement vérifiable ; soit qu’il n’en existe pas de définition formelle ou que le sens varie trop selon les branches des mathématiques (si encore on parviens à y trouver les définitions en question, surtout que plus c’est spécialisé, plus c’est étanche et fermé).

C’est pénible, c’est usant, de tourner en rond pendant des jours pour ne même pas trouver une définition claire et unanime et non‑équivoque, d’une notion pourtant élémentaire, comme “ syntax ” par exemple. Le monde des mathématiques a un sérieux problème avec la communication ; je crois qu’il se moque d’être compris du reste du monde autant qu’il se moque d’essayer de le comprendre.

Mais comme il faut bien faire avec, voici plus loin, quelques liens qui pourront donner des définitions ou des pistes de définitions d’assez nombreux termes.

Ce message est piquant plus haut, et j’en rajoute avec trois suggestions personnelles, justifiées par l’existence des problèmes mentionnés plus haut :

  • Se poser des limites au mal qu’on se donne à essayer de comprendre le langage de gens qui, eux, ne font aucun ou peu d’effort pour que leur langage soit compréhensible, mises à part quelques exceptions, la plupart se complaisant dans un monde étanche quand encore il n’est pas élitiste derrière l’apparence du contraire.
  • Les mots dans le contexte des mathématiques ayant des sens tellement en contradiction avec leur sens courant et ayant des sens de plus même pas toujours clairement définis (un comble pour des gens revendiquent appliquer des formalisme), il me semble inévitable sous peine de ne pas pouvoir avancer, de devoir poser les définitions en défaut, soi‑même, ce qui signifie par exemple, un dictionnaire personnel, éventuellement destiné à être communiqué aux gens dont on souhaite qu’ils puissent comprendre ce qu’on écrit.
  • Le sens des mots dans les mathématiques est déjà un problème assez lourd comme ça, pour qu’il soit préférable de s’épargner d’en rajouter avec des problèmes de traductions d’une langue à une autre ; je crois que en dehors des cas où on reste informel, il préférable de s’en tenir au vocabulaire en Anglais, sans essayer de le traduire en français par exemple, des traductions qui parfois créent leurs propres ambiguïtés ou ne préservent pas toujours les connotations ou ne semblent pas naturelles (de toutes manières, en dehors des « sciences humaines », la langue de la plupart de la plupart des sciences, c’est Anglais, n’en déplaise à certains).

Pour ne quand‑même pas définir sa propre terminologie de manière trop fantaisiste, voici une liste de ressources en ligne à consulter, chaque fois qu’on pense devoir créer un terme, pour vérifier si par chance il n’en existe pas déjà un convenable. En cas d’échec, si rien de suffisamment précisément défini ou de n’induisant pas trop en erreur ou de pas trop variable, ne ressort, alors il n’y pas d’autre choix que de définir ses propres termes sur la base des mots du langage courant qui en sont les plus proches, en n’omettant pas de justifier la création de chaque terme.


Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Mer 6 Mai 2020 16:52
Message Re: Les logiques : notes en vrac
Séparément, en marge du précédent message, je voudrais souligner l’importance des symboles en mathématiques, et souligner que le problème de communication est surtout dans les mots pour les expliquer.

Ces symboles semblent obscurs au premier abord, mais au moins ils n’entrent pas en conflit avec le sens des mots ou des idiomes du langage courant (quoi qu’ils sont sujet aussi sujet à des interprétations trop variables, mais moins que les mots). Je suggérais plus haut de ne pas se priver si la nécessité est vraiment justifiée, de poser soi‑même la définition de ses propres termes, mais il faut autant que possible éviter de le faire avec les symboles.

Le problème est surtout dans l’usage du langage courant. Les symboles doivent être expliqués, ce qui ne peut se faire initialement qu’avec le langage courant. Il semble exister dans le milieux des mathématiques, une tradition de traiter les mots du langage courant comme des symboles mathématiques, qu’ils ne sont pourtant pas, une tradition de nier les problèmes de compréhension que cela pose de donner aux mots du langage courant, des sens déroutants qui leur font perdre leur capacité à communiquer utilement.

Ce que je veux dire, c’est que la liberté de définir ses propres termes (pour remédier à une imprécision ou à une ambiguïté, pour être conforme à un déplacement de point de vue, etc), doit avoir pour finalité de rendre compréhensible le sens de symboles dont le sens ne doit pas être modifié. Autant le monde des mathématiques n’a aucune légitimité à modifier le sens des mots du langage courant, autant le monde qui n’est pas à l’origine des symboles mathématiques n’a de légitimité à en modifier le sens. Les seconds sont naturellement méfiants avec ça, les premiers, beaucoup moins, c’est là qu’est le problème.

Le sens des symboles mathématiques, appartient aux mathématiques (quand leur sens est clair, ce qui n’est pas toujours le cas), mais comment intialement introduire leur sens avec le langage naturel, ça n’appartient pas aux mathématiques.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Mer 6 Mai 2020 19:56
Message Re: Les logiques : notes en vrac
Dans le précédent message, je mentionnais entre parenthèses, que même les symboles ne sont pas toujours clairs. Dans le message encore précédent, je proposais une liste de sites à consulter pour se renseigner sur les usages d’un terme avant d’en faire usage soi‑même ou de décider d’en définir un nouveau.

Il se trouve qu’un des sites est un exemple d’induction en erreur. Le site http://www.encyclopediaofmath.org fait usage du symbole ⊃ pour signifier l’implication. Non seulement l’usage de ce symbole est incompréhensible quand il existe déjà deux symboles dont l’usage est bien plus répandu, ⇒ et → [1], mais en plus l’usage de ⊃ s’apparente à une contradiction quand ont sait que quand A → B est vérifiée, les cas où A est vraie sont inclus dans les cas où B est vraie [2]. Ors, regardez de quoi cette implication a l’air quand elle est notée avec ce symbole d’inclusion ensembliste : A ⊃ B ; cette notation suggère que l’ensemble des cas où B est vraie, est inclus dans l’ensemble des cas où A est vraie [3], c’est à dire l’inverse de ce que signifie l’implication, qui est que l’ensemble des cas où A est vraie, est inclus dans l’ensemble des cas où B est vraie.

On croirait qu’ils le font exprès ! Et c’est un site de référence, chapeauté par deux organisations réputées …


[1] qui sont déjà a eux seuls une source d’induction en erreur à cause de ⇒ dont la signification est variable, comme décrit dans un précédent message

[2] Table de vérité de A → B :

A B A → B
0 0 1
1 0 0
0 1 1
1 1 1

On parle du cas où A → B est vérifiée, on ne tient pas compte de la seconde ligne, il ne reste que :

A B A → B
0 0 1
0 1 1
1 1 1

Les cas où A est vraie sont inclus dans les cas où B est vraie. Ce qui est cohérent avec l’explication de l’implication en langage courant : si A est vraie mais que B est fausse, alors l’implication n’est pas vérifiée, ce qui signifie que B peut être vraie quand A est fausse, mais que A ne peut pas être vraie quand B est fausse, donc que l’ensemble des cas où A est vraie sont inclus dans l’ensemble des cas où B est vraie.

[3] ce symbol s’utilise plus habituellement dans l’autre sens, A ⊂ B pour dire que A est inclus dans B, c’est à dire que A ⊃ B se lit alors B est inclus dans A. En marge, le symbole ⊂ est parfois lui aussi une source d’induction en erreur, comme A ⊂ B signifie tantôt que A peut être égale à B ou que A est strictement plus petit que B.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Mer 6 Mai 2020 21:10
Message Re: Les logiques : notes en vrac

Ces deux sont à souligner à part maintenant, le premier, puis le second.

Le premier n’a pas l’air d’avoir l’importance qu’il a, alors il faut la dire explicitement : MSC, est une classification des domaines des mathématiques ; il fallait bien ça, dans les thèmes des mathématiques sont vastes au point d’être inconnus les uns des autres. Les catégories principales sont identifiées par deux chiffres suivis de chiffres et/ou de lettres, ce qui suit les deux chiffres initiaux, peut être XX (ou __ sur certains sites) en guise de blancs, pour dire qu’on désigne une catégorie principale toute entière. Les catégories principales qui nous intéressent ici, sont MSC 00-XX et MSC 03-XX, pour “ General ” et “ Mathematical logic and foundations ”.

Le second site, fait usage de cette classification ; c’est visible quand on consulte la page “ Subject index ”. D’autres sites sur les mathématiques font aussi référence à cette classification, même si plus discrètement.

Le second site a mis en ligne sont contenu sous forme d’archives sur Github ; pour les gens qui connaissent, voici le lien : planetmath (github.com). Là encore, on retrouve l’organisation selon la classification MSC, avec un dépôt par catégorie principale.

La classification du premier site est décrite pas cet autre site, qui annonce aussi une révision cette année, MSC 2020 : Mathematics Subject Classification (mathscinet.ams.org).

Pour une copie locale des codes classification, ce qui peut être utile pour ranger des documents ou organiser une recherche sur le web, voir l’une ou l’autre de ces options, pour MSC 2010 : MSC 2010 Classification Codes (cran.r-project.org) ou Laurent-Dubois-1977/msc2010 (github.com).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 18835
Jeu 7 Mai 2020 00:34
Message Re: Les logiques : notes en vrac
Le terme iff, “ if and only if ”, ne désigne pas une condition, mais une relation logique. Il faut vraiment seulement le comprendre comme ↔ et comme rien d’autre. Encore un exemple de vocabulaire trompeur.

Ce qui me le fait dire, c’est par example ce qui suit. On peut voir une chose définie, ainsi que des propriétés possibles de certaines instances de cette chose, parmi lesquelles P1 et P2, ces deux propriétés étant en fait équivalentes, seulement présentées différemment. On peut voir dire dans la définition de la prorpiété P1, P1 iff P2 et dans la définition de la propriété P2, P2 iff P1. La définition ne pouvant pas être circulaire, ça ne peut que être une relation réciproque (ce qui se comprend, si les deux propriétés sont équivalentes). Dans ce cas là, P2 est démontrable à partir de P1 et P1 est démontrable à partir de P2, les deux étant déjà posées, la définition n’étant pas circulaire.

Une condition est une dépendance, elle doit être établie à priori, elle ne peut donc pas être réciproque : la définition de A ne peut pas dépendre de la définition de B si la définition de B dépend de la définition de A, comme il faudrait que l’une existe avant l’autre et réciproquement. Une relation logique n’en est pas une, comme elle peut être vérifiée ou non et qu’elle est vérifiée à posteriori : les définitions de A et de B étant posées, on peut démontrer plus loin une relation réciproque entre les deux ou on y parviens pas et le tout est par la suite encore invalidé. Plutôt que de succession temporelle, ce qui peut poser un problème de compréhension, on peut parler de niveaux d’élaboration.

Il faut distinguer dépendance et relation, et iff désigne une relation, pas une dépendance.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet