Deducteam
Unsafe translation to Why3
The translation of types to Why3 introduced in #769 is unsafe: we must ensure that the types translated as fresh constants in Why3 are inhabited. See https://github.com/Deducteam/lambdapi/pull/769#discussion_r772928743 for the original comment.
The email mentioned in the comments is attached below
Il y a un soucis avec le théorème 18 de http://www.lsv.fr/~dowek/Publi/expressing.pdf concernant la correction et la complétude de l'encodage de la logique du premier ordre intuitioniste, dont la preuve est en fait donnée dans le rapport de stage de L3 d'Alexis Dorra en 2010, ici en copie, mais en fait introuvable sur Internet (il faudrait peut-être y remédier!).
Le théorème 18 dit: "Let L be a language, Σ be the associated context, V be a set of variables and A1 , . . . , An , B be propositions in L such that the free variables of A1 , . . . , An , B are in V . Let Γ1 be a context containing for each variable x of sort s in V , a variable x , of type s , and Γ2 be a context containing, for each hypothesis Ai a variable ai of type ||Ai||. Then, the sequent A1 , . . . , An |- B has a proof in Natural deduction if and only if there exists a λ-term π such that Σ, Γ1 , Γ2 |- π : ||B||."
Le théorème 1 de Dorra concernant la correction est: "S’il existe une preuve d’une proposition A en logique intuitionniste dans le contexte Γ, alors il existe un terme t typé par ϵ(Ȧ) en lambda calcul modulo dans le contexte ∆; ||Γ||." où ∆ est défini dans la Définition 1 en disant que: "pour toute variable libre x présente dans Γ et dans la proposition que l’on démontre, on a x : ι ∈ ∆."
Le problème est que ces deux théorèmes sont partiellement faux:
Prenons la proposition (∀x,px) ⇒ (∃x,px).
Une preuve possible en déduction naturelle est:
ax ---------------- ∀x,px |- ∀x,px ∀e ----------------- ∀x,px |- px ∃i ------------------ ∀x,px |- ∃x,px ⇒i ----------------- |- (∀x,px) ⇒ (∃x,px)
En appliquant le théorème 1, on obtient:
ax ---------------- h : ϵ(∀x,px) |- h : ϵ(∀x,px) ∀e ----------------- h : ϵ(∀x,px), x:ι |- h x : ϵ(px) ∃i ------------------
Premier problème: la preuve du théorème 1 ne contient pas le cas ∃i. Ceci dit, ϵ(∃x,px) est défini dans la Définition 3 comme Π q : o, (Π x : ι, ϵ(p x) ⇒ ϵ(q)) ⇒ ϵ(q). On pourrait donc en déduire qu'il faut prendre:
h : ϵ(∀x,px), x : ι |- λ q : o, λ g : (Π x : ι, ϵ(p x) ⇒ ϵ(q)), g x (h x) : ϵ(∃x,px)
Problème: x apparaît librement dans λ q : o, λ g : (Π x : ι, ϵ(p x) ⇒ ϵ(q)), g x (h x) mais n'apparaît librement ni dans ϵ(∀x,px) ni dans ϵ(∃x,px). Autrement dit, le contexte ∆ dans le théorème 1 ou le contexte Γ1 dans le théorème 18 ne dépend pas seulement des propositions mais aussi de la preuve...
Il me semble que le problème vient du fait qu'en logique du premier ordre, les domaines d'interprétation sont implicitement supposés non vides, et cela n'est pris en compte ni dans la traduction ni dans la preuve de correction.
Pour se débarrasser du x : ι qui reste, il convient de le remplacer par un terme clos de type ι, qui témoigne du fait que le domaine/type ι est non vide. Il faudrait donc rajouter dans la signature une constante c : ι sauf si ι est habité en utilisant les symboles de fonctions déjà déclarés.
