Les logiques : notes en vrac

Les dix règles d’inférence du standard OpenTheory

Et OpenTheory, repose sur HOL …

Source de ce qui suit : The OpenTheory Standard Theory Library (gilith.com) [PDF], Joe Hurd, Avril 2011.

refl t: ∴ ⊢ t = t
(une chose est égale à elle‑même)

assume ϕ: ∴ {ϕ} ⊢ ϕ
(une prémisse est considérée comme un fait connu)

eqMp: Γ ⊢ ϕ = ψ, Δ ⊢ ϕ ∴ Γ ∪ Δ ⊢ ψ
(si dans un contexte on sait que deux certaines choses sont égales, si dans autre contexte on sait la première chose, alors dans l’union des deux contextes, on sait la deuxième chose)

absThm v: Γ ⊢ t = u ∴ Γ ⊢ (λv.t) = (λv.u)
(deux expressions égales se substituent l’une/l’autre comme corps d’une fonction)

appThm: Γ ⊢ f = g, Δ ⊢ x = y ∴ Γ ∪ Δ ⊢ f x = g y
(si deux fonctions sont égales, si deux expressions sont égales, alors l’application de ces deux fonctions à l’une de ces deux expressions, donne deux expressions égales)

deductAntisym: Γ ⊢ ϕ, Δ ⊢ ψ ∴ (Γ - {ψ}) ∪ (Δ - {ϕ}) ⊢ ϕ = ψ

subst σ: Γ ⊢ ϕ ∴ Γ[σ] ⊢ ϕ[σ]
(si dans un contexte on sait une chose, alors si dans ce contexte on peut effectuer une certaine substitution, on sait qu’on peut faire cette substitution dans cette chose qu’on sait)

betaConv ((λv.t) u): ∴ Γ ⊢ (λv.t) u = t[u/v]
(l’application d’une fonction à un argument, est égale aux corps de cette fonction, dans lequel on a substitué le nom du paramètre de cette fonction, par l’expression sur laquelle on l’applique)

defineConst c t: ∴ ⊢ c = t
(définition d’une constante liée à une valeur)

defineTypeOp n abs rep vs: ⊢ ϕ t ∴ ⊢ abs (rep a) = a, ⊢ ϕ r = (abs (rep r) = r)


Notes

Le symbole « ∴ », représente le séquent, comme expliqué dans le message Re: Les logiques : notes en vrac, du 27 Avril 2014.

L’égalité ici, doit sûrement se comprendre comme une égalité syntaxique (pas l’unification), parce que sinon la règle “absThm v” n’aurait pas de sens. Il y a probablement d’autres choses implicites encore.

La règle “betaConv”, c’est la règle nommé β‑réduction dans le lambda‑calcul ; elle est parfois écrite “(λv.t) u = t[v := u]”, … une autre notation pour dire la substitution d’une liée, à une expression. D’ailleurs il faudra que j’en fasse un sujet, des règles du lambda‑calcul.

En plus de ces dix règles d’inférence, OpenTheory applique quand nécessaire, deux opérations : le renommage des types et des contextes pour éviter les conflits de noms dans certains contextes (ce qui rappel qu’on parle bien d’égalité syntaxique) et la composition de plusieurs théories en satisfaisant les suppositions (les prémisses) de l’une avec les théorèmes des autres.

Ce standard inclus quelques théories de base, auxquelles il est possible de se référer pour ne pas avoir à les répéter à chaque fois dans chaque fichier d’une théorie. Des théories sont incluses pour les choses suivantes :

• Le type booléen;
• les listes;
• le type option;
• les types produits (paires);
• les types sommes (alternatives);
• le type unité (unit);
• les fonctions en général;
• les entiers naturels;
• les relations (c’est vague, pour moi).

Ajouté à la bibliographie de la page 2 : From LCF to HOL — a short history (cl.cam.ac.uk) [PDF], Mike Gordon, 2000.

Dans HOL4 (hol-theorem-prover.org), un assistant de démonstration, on dispose de huit primitives pour créer des théorèmes dérivés et donc des preuves :

• ASSUME (introduction d’une supposition);
• REFL (réflexivité);
• BETA_CONV (béta‑conversion);
• SUBST (substitution);
• ABS (abstraction);
• INST_TYPE (instanciation d’un type);
• DISCH (décharge de supposition);
• MP (modus‑ponem).

On peut reconnaitre des similitudes avec les dix règles d’inférences de HOL‑Light (mentionnées précédemment) et les dix règles d’inférence d’OpenTheory, tout en notant qu’il n’y en a ici que huit, au lieu de dix.

Je commenterai plus, plus tard, en ajoutant seulement pour le moment que quatre de ces huit primitives, sont considérées comme des axiomes du système de déduction, et ces quatre axiomes, sont en fait eux‑mêmes une généralisation d’une logique de base.

C’est dans l’œuvre d’Euclide, « Éléments », que semble avoir été posée pour la première fois à l’écrit, la méthode déductive appliquées aux mathématiques, environ 300 ans avant J.C..

Les trois principaux systèmes d’axiomes en dehors de l’informatique, sont :

• Les axiomes d’Euclide, pour la géométrie plane.
• Les axiomes de Peano, pour les nombres entiers.
• Les axiomes ZFC, Zermelo‑Fraenkel plus le théorème du choix, pour les mathématiques en général.

Notez qu’il est précisé « en dehors de l’informatique », ce qui explique que HOL n’y figure pas, alors qu’il en est souvent question dans ce sujet.

Ci‑dessous, une présentation du théorème de Gödel, orale et en images. C’est de cette présentation qu’est tirée cette liste de systèmes d’axiomes.

Les théorèmes d'incomplétude de Gödel — Science Étonnante № 37

Sur une interprétation et une démonstration en termes informatiques, du théorème d’incomplétude de Gödel.

Incomplétude — Passe‑Science № 7

Une présentation de Microsoft, dont les premières vignettes donnent en termes simples, un aperçu du fonctionnement des solveurs SMT : Satisfiability Modulo Theories: an appetizer (microsoft.com) [PDF], Leonardo de Moura, 2009.

Pour une anecdote, voir le sujet « Le mot “rationalisme” ».

À propos de quelques formes d’implication et de conséquence,
en logique : Réponse à “Implies vs. Entails vs. Provable” (math.stackexchange.com).

La logique et le « bon sens » ne sont pas la même chose. La logique ne fait pas partie du « bon sens » et le « bon sens » n’est pas toujours logique.

Un rappel tiré de cette vidéo, dont on peut conclure qu’il faut toujours interpréter une logique comme elle a été conçue, sans le faire dans un autre langage confondant logique et méta‑logique, et sans y incorporer des éléments d’une autre logique sans que ce ne soit prévu.

Quatre paradoxes de la logique mathématique — Science4All — 2016