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 : 15320
Mar 19 Nov 2013 18:09
Message Les logiques : notes en vrac
C’est un sujet assez difficile à cerner, il ressemblera peut‑être à des notes personnelles, mais pourquoi pas en faire un sujet ici, si des gens veulent lire les notes et commenter. Ce sont des notes pour débroussailler les sujets de la logique, avec un biais avoué envers les formes de la logique ayant des intérêts pratiques en informatique.

À expliquer et à synthétiser succinctement :

  • HOL vs FOL (Higher Order Logic vs First Order Logic);
  • Théorie des types vs théorie des ensembles;
  • Logique constructiviste (alias intuitionniste) vs logique classique;
  • Turnstile (⊢, c’est quoi son nom français ?) vs entailment (⊧, c’est quoi son nom français ?) vs implication vs « barre horizontale » (elle s’appelle comment ?);
  • Soundness (correction ou « correctitude » en français) vs complétude vs cohérence (alias consistance);
  • Soundness (j’aime mieux le mot anglais pour dire ça Rougi ) d’un système d’axiomes : comment en faire la démonstration;
  • Implication vs conséquence;
  • Sémantique vs syntaxe et relations possibles entre les deux et rôle et portée de la réécriture;
  • Sémantique vs interprétation;
  • Déduction naturelle vs autres raisonnements déductifs;
  • Propositions vs prédicats;
  • Induction vs récursion (et les types, inductifs vs récursifs);
  • Sémantique(s) standard(s);
  • Modèles standards et modèle général d’une logique/d’un langage;
  • Appréciation théorique vs appréciation pratique (d’un système, d’un langage, etc);
  • Logique faible vs logique forte;
  • Avantages supposés de FOL vs inconvénients supposés de HOL;
  • Sémantique, axiomatique vs dénotationnelle vs opérationnelle (axiomatic vs denotational vs operational semantic);
  • Calcul des séquents vs déduction naturelle vs L‑systèmes vs système à la Hilbert (sequent calculus vs natural deduction vs L‑systems vs Hilbert‑style system);
  • Écriture, ré‑écriture et normalisation;
  • Notation et dénotation;
  • Théorie des domaines (de Scott);
  • Logique ou proposition imprédicative; imprédicativité;
  • CIC (Calculus of Inductive Constructions) vs CTT (Computational Type Theory) vs ITT (Intuitionistic Type Theory) et leurs rapports ou non‑rapport avec les types dépendants;
  • Arithmétique de Peano (Peano Arithmetic ou PA) et Arithmétique de Heyting (Heyting Arithmetic ou HA);
  • Axiome de réductibilité (axiom of reducibility) de Russel et Whitehead;
  • Notion d’individuels (individuals) en HOL;
  • Le statuts des entiers naturels dans un système logique (notion primitive ou dérivée);
  • Définitions de la notion de type (ex. défini par l’équivalence, ou autres);
  • Sémantiques BHK et PER.

Dernière édition par Hibou le Mer 1 Oct 2014 09:32, édité 28 fois.

Mise à jour de la liste

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15320
Mar 19 Nov 2013 20:26
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Turnstile (⊢, c’est quoi son nom français ?) vs entailment (⊨, c’est quoi son nom français ?) vs implication ;

⊢ s’applique à la syntaxe, et ⊨ s’applique à la sémantique. C’est déjà une différence claire entre les deux. Tous deux sont des conséquences : conséquence syntaxique pour le ⊢ et conséquence sémantique pour le ⊨. L’implication ⇒ (parfois notée ⊃ ou encore parfois assez mal notée →), est un opérateur du calcul des propositions.

J’ajoute à la liste, la question « conséquence vs implication ».

J’ajoute à la liste, la question « sémantique vs syntaxe et relation entre les deux ».

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 : 15320
Mer 4 Déc 2013 16:12
Message Re: Les logiques : notes en vrac
J’ajoute à la liste « déduction naturelle vs autres raisonnements déductifs ».

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 : 15320
Ven 13 Déc 2013 03:56
Message Re: Les logiques : notes en vrac
J’ajoute à la liste « propositions vs prédicats ».

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 : 15320
Mer 25 Déc 2013 11:23
Message Re: Les logiques : notes en vrac
J’ajoute à la liste « induction vs récursion » et « sémantique(s) standard(s) ».

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 : 15320
Mer 25 Déc 2013 12:22
Message Re: Les logiques : notes en vrac
Une citation de Wikipédia EN, à creuser :

Wikipedia a écrit : 
Intuitionistic type theory is based on a certain analogy or isomorphism between propositions and types: a proposition is identified with the type of its proofs. This identification is usually called the Curry–Howard isomorphism, which was originally formulated for intuitionistic logic and simply typed lambda calculus. Type theory extends this identification to predicate logic by introducing dependent types, that is types which contain values.


Traduction a écrit : 
La théorie intuitionniste des types, est basée sur une certaine analogie ou isomorphisme, entre types et propositions : une proposition est assimilée au type de sa preuve. Cette équivalence est habituellement désignée sous le nom de Isomorphisme de Curry‑Howard, initialement formulé pour la logique intuitionniste et le lambda‑calcul simplement‑typé. La théorie des types étend cette assimilation à la logique des prédicats, au moyen de l’introduction des types dépendants, c’est‑à‑dire des types possédant une valeur.


Source : Intuitionistic type theory (en.wikipedia.org)

Je me disais bien qu’il y a une correspondance entre type et proposition Sourire doux ; ça se confirme.

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 : 15320
Ven 27 Déc 2013 18:36
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Je me disais bien qu’il y a une correspondance entre type et proposition Sourire doux ; ça se confirme.

Les types y ont par ailleurs une fonction importante : ils sont la solution au paradoxe de Russell, celui de l’ensemble des ensembles qui est inclus ou pas dans lui‑même (les lambda expressions, aussi, sont une solution à ce paradoxe).

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 : 15320
Ven 27 Déc 2013 18:37
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
J’ajoute à la liste « induction vs récursion » et « sémantique(s) standard(s) ».

J’aurais plutôt dut ajouter « modèles standards et modèle général »… je ne sais même pas si je n’ai pas confondu modèle et sémantique… ou alors c’est la même chose ? J’en sais rien (je crois que plutôt pas).

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 : 15320
Sam 28 Déc 2013 19:08
Message Re: Les logiques : notes en vrac

Historique à très gros traits


Syllogisme : Les Grecs connaissaient le syllogisme, qui dérive une conclusion à partir d’une ou plusieurs prémisses, vers 300 avant l’ère Chrétienne. Deux formes coexistaient : celle de Aristote et celle de Zénon‑de‑Citium. Était‑ce l’implication ou cela différait‑il ? Cette logique connaissait deux quantificateurs : « tous » et « des » (“all” et “some”).

Logique des propositions : Les Grecs ont connu une forme de logique des propositions, formalisée par Chrysippe de Soles (Chrysippus en Anglais), en 200 avant l’ère Chrétienne. Cette notion a été perdue par la suite, et n’a été re‑inventé ou re‑découverte, par Pierre Abélard, qu’au début du second millénaire, soit environ 1200 à 1300 ans plus tard. Je ne sais pas si cette logique disposait de quantificateurs.

Logique des propositions (2) : La logique des propositions a été reprise et affinée par Leibniz au début des années 1700, soit 7 siècles après Abélard et 2000 ans après Chrysippe. Ses travaux, restés méconnus des logiciens de son époque, ont été eux‑même réinventé et re‑affiné par Boole et De Morgan, dans les années 1800, un siècle après Abélard.

Syllogisme (2) : le Syllogisme d’Aristote, a été d’une manière repris par Boole dans les années 1800, pour qui le syllogisme des Grecs, pouvait être vu comme une interprétation de sa logique algébrique (l’algèbre de Boole).

Logique du premier ordre (FOL) / Logique des prédicats (Syllogisme + Logique des propositions) : La logique des prédicats (du premier ordre), combinant les caractéristiques de la logique des propositions et le syllogisme, a été définie par Frege, dans la seconde moitié des années 1800.

Logique du second ordre (SOL) : la logique du premier ordre, a été généralisée, sous le forme de la logique du second ordre, par Peirce, à la même époque ou quasiment en même temps, que la logique des prédicats (du premier ordre).

Logique d’ordre supérieur (HOL) / logique d’ordre N : bien que à la suite de la logique d’ordre 1 et d’ordre 2, il soit parfois fait mention de la logique d’ordre 3, il se trouve plus de référence à propos des logiques d’ordre supérieur, en général. Je ne connais pas la date de la première mention de cette logique, je sais seulement qu’elle a commencé à faire parler d’elle dans les années 1970 (à la suite de LCF — Logic of Computable Functions), et qu’elle est toujours populaire dans les sciences de l’informatique.

À côté de ces logiques, qui représentent le plus gros, l’époque contemporaine (1900 et 2000), a vu naitre d’assez nombreuses autres formes de logiques (dont, pour les principales, les logiques modales, les logiques multivaluées, …), qui ne sont pas mentionnées dans cette historique.

Ce que signifie l’ordre d’une logique — premier ordre, second ordre, troisième ordre, et ordres supérieurs — sera résumé plus tard.

Image
Hibou57

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

Dernière édition par Hibou le Ven 1 Jan 2016 04:16, édité 4 fois.

Mise à jour

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15320
Sam 28 Déc 2013 20:10
Message Re: Les logiques : notes en vrac

Systèmes de preuve à la Hilbert vs systèmes de déduction naturelle


Les systèmes de déduction à la Hilbert, sont des systèmes qui présentent un grand nombre d’axiomes et un relativement petit nombre de règles (par rapport au nombre d’axiomes), les règles d’inférences.

Les systèmes de déduction naturelle (c’est juste leur nom, rien ne prouve qu’ils soient plus naturels pour tout le monde), sont des systèmes qui présentent souvent un petit nombre d’axiomes et des règles de déduction organisées en règle d’introduction et règle d’élimination ; des règles duales, donc (à une exception prêt, celle du faux).

Pourquoi les règles des systèmes à la Hilbert s’appellent des règles d’inférences et les règles des systèmes de déduction naturelle s’appellent des règles de déduction ? Je ne sais pas… pour moi, déduction et inférence, sont une même chose.

Je ne sais plus qui (*) disait en gros « mieux vaut des définitions que des axiomes, et les axiomes, c’est un peu comme voler plutôt que profiter des fruits mérités du travail ». L’idée sous‑jacente, est de dériver des théorèmes à partir d’un petit nombre d’axiomes, et d’utiliser ces théorèmes dérivés aussi commodément que s’ils étaient des axiomes. Ce principe s’applique plus naturellement ( Hmmm! ) avec les systèmes de déduction naturelle.

(*) Russell ? J’en sais rien Si je retrouve la citation et son auteur, je corrige ce passage en le précisant.

Le second type est réputé plus fiable (pour des raisons pratiques), et aura de plus en plus la faveur du monde de la logique dans les années à venir, par l’effet de la généralisation des logiciels d’assistance à la démonstration et de validation informatique des démonstrations, et respectant le critère de De Bruijn. Le premier type, qui repose sur des axiomes et méthodes ad‑hoc, est même encore de nos jours fréquemment jugé commode et pratique par les mathématiciens, mais les sciences de l’informatique ne sont pas tant de cet avis, et ce type de système ne verra probablement sa popularité que décliner dans l’avenir.

Autrement encore, le premier type est jugé facile à comprendre mais difficile à manier, et le second, difficile à comprendre et facile à manier. C’est une appréciation répandue qu’il faudrait justifier. Peut‑être que les systèmes à la Hilbert prennent des gros raccourcis en se souciant peu du détail des étapes, ce qui les rend plus accessibles à l’intuition, tandis que les systèmes de déduction naturelle, rendent plus clairs les passages entre les étapes, mais au prix de plus longs enchaînements qui rendent l’ensemble d’une preuve moins compréhensible aux humains ? J’en sais rien

À noter que intuitif dans un sens ou l’autre, les deux systèmes ont la même obligation d’être justes. La question de l’intuitif, n’est pas celle de la confiance.

Image
Hibou57

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

Dernière édition par Hibou le Dim 29 Déc 2013 16:32, édité 1 fois.

Mise à jour

Profil Site Internet
cron