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 vs théorie des catégories;
• 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 ) 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 ;
• Analyse de programme (model checking) ;
• Vérification de modèle (model checking) ;
• Interprétation abstraite (abstract interprétation).

⊢ 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 ».

J’ajoute à la liste « déduction naturelle vs autres raisonnements déductifs ».

J’ajoute à la liste « propositions vs prédicats ».

J’ajoute à la liste « induction vs récursion » et « sémantique(s) standard(s) ».

Une citation de Wikipédia EN, à creuser :





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

Je me disais bien qu’il y a une correspondance entre type et proposition ; ç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).

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 ? (je crois que plutôt pas).

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.

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 ( ) avec les systèmes de déduction naturelle.

(*) Russell ? 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 ?

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