Re: Le cerveau n'est pas logique

La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout...

La correspondance s'étend aussi au raisonnement par l'absurde et donc à la logique classique, ce sont les exceptions dans les langages de programmation (les blocs try-with-finally). Voir ce texte de Jean-Louis Krivine (page 3).

Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond...

Ce n'est qu'une question de vocabulaire : il y a d'un côté les jugements que l'on considère (calcul des prédicats ou calcul propositionnel, au premier ou second ordre) et de l'autre les règles de déductions (classique ou intuitionniste). Comme dans une logique on considère à la fois les règles de formations des jugements et les règles de déduction, pour éviter toute ambiguïté, il serait sans doute préférable de parler de logique classique du premier ordre et de logique intuitionniste du premier ordre.

Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.

Le quantificateur universel c'est le \lambda du lambda-calcul, le\ de Haskell, le fun de OCaml... c'est lui qui abstrait sur la totalité d'un domaine et, effectivement, dans le calcul des prédicats, on abstrait sur tout le domaine du modèle — sur tout l'univers des ensembles dans ZF. Les langages dynamiques sont des langages avec typage statique... qui n'ont qu'un seul type statique. Là où dans les théories des types, comme en Coq, on peut n'abstraire que sur les valeurs d'un type donné.

L'implication est bien toujours le signe d'une fonction mais, dans mon exemple, elle ne spécifie rien sur sa sortie pour une entrée qui n'est pas un ordinal. Si on reprend mon énoncé (légèrement modifié) :

il dit qu'à tout ensemble x, il peut en associer un autre y. Lorsque x est un ordinal, l'énoncé affirme que y est son prédécesseur qui est aussi un ordinal, mais dans le cas contraire (qui peut arriver, on a quantifié sur tous les ensembles), il ne dit rien sur y. La preuve d'un tel théorème expose, dans le cas où x est un ordinal, un moyen de produire un tel y et fournit la preuve que y est aussi un ordinal. En revanche, dans le cas où x n'est pas un ordinal, elle ne dit rien sur y (si ce n'est que c'est un ensemble, donc n'importe quelle valeur possible). Ce qui me fait penser à ce code Go :

func pred(v interface{}) (uint, error) {
 var res uint
 var err error
 switch i := v.(type) {
 case uint:
 if i == 0 {
 res = uint(0)
 } else {
 res = uint(int(i) - 1)
 }
 default:
 err = errors.New("not an uint")
 }
 return res, err
}

Il prend en entrée toute valeur possible (n'importe quel ensemble pour ZF), dans le cas où c'est un uint renvoie un y selon la même spécification que l'énoncé, ou bien renvoie une erreur si l'entrée n'est pas de type uint (cas de la preuve qui ne dit rien sur y, on renvoie une erreur). Ici le procédé est totalement constructif au sens des règles de déductions intuitionnistes. Le fait que la preuve du théorème prouve aussi que y est un ordinal, quand x l'est, se retrouve sur le type de sortie de la fonction en Go.

Après réflexion, on pourrait faire quelque chose de similaire en OCaml. Pour cela, il faut un type dans lequel on puisse plonger des valeurs de n'importe quel type : on parle de type universel. La signature d'un module fournissant un tel type est :

module type Univ = sig
 type t
 val embed : unit -> ('a -> t) * (t -> 'a option)
end

Je passe les détails d'implémentations d'un tel module (il faut utiliser un type somme extensible, comme l'est celui des exceptions dans le langage) et montre juste son usage en supposant que l'on a module U : Univ, c'est à dire un module fournissant un tel type :

(* ici on a des fonctions pour injecter dans et projeter
 * depuis le type `U.t` des valeurs de type `int` ou `nat` *)
let (inj_int : int -> U.t), proj_int = U.embed()
let (inj_nat : nat -> U.t), proj_nat = U.embed()
(* on définit maintenant à partir de la fonction `pred` sur `nat`
 * une fonction `pred` générique sur le type universel `U.t` *)
 let pred_gen v = match proj_nat v with
 | None -> None
 | Some n -> Some (pred n)
;;
val pred_gen : U.t -> nat option = <fun>
(* si la valeur de type `U.t` contient un `int`, on renvoie `None` *)
pred_gen (inj_int 2);;
- : nat option = None
(* si elle contient un `nat`, on renvoie son prédecesseur *)
pred_gen (inj_nat (S (S O)));;
- : nat option = Some (S O)

Pour en revenir aux différentes logiques, le problème est bien dans le calcul des prédicats. Il est tel que, lorsqu'on l'interprète, toute les choses dont il parle sont considérées comme étant homogènes. Par exemple, si on veut formaliser la théorie des espaces vectoriels dans un tel symbolisme, il faut mettre les scalaires et les vecteurs dans un même sac fourre-tout et un modèle d'une telle théorie devra donner une signification à la somme d'un scalaire et d'un vecteur (ce qui, fondamentalement, n'a aucun sens dans un tel cadre). Raison pour laquelle je disais que les approches de la logique via la théorie des types captent bien mieux la notion de concept : le concept de scalaire ne sera nullement mélangé arbitrairement avec celui de vecteur, ce seront deux types distincts.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.