DEA Programmation Preuves constructives Examen Jeudi 16 Décembre 1999 Durée 2h Tous documents autorisés

1

Donner une démonstration en déduction naturelle intuitionniste du premier ordre, des propositions

((P 0) ∧ (P 0)) ⇒ (P 0)
(∀y (P y)) ⇒ (P 0)
(P 0) ⇒ (∀x (P x) ⇒ (P (S x))) ⇒ (P (S (S 0)))

Dans quel λ-calcul peut-on exprimer ces démonstrations ? Exprimer ces démonstrations par un terme de ce calcul.

2

La fonction “double” est définie par les équations suivantes

(d 0) = 0
(d (S x)) = (S (S (d x)))

(1) Donner une définition de cette fonction dans la théorie des types de Martin-Löf.

(2) Soit t un terme-preuve, dans la théorie des types de Martin-Löf, du théorème

∀x ∃y ((x = (d y)) ∨ (x = (S (d y))))

Quel est le type du terme (t (S (S (S (S (S 0)))))) ?

(3) Quelle est la forme normale du terme π_{1}(t (S (S (S (S (S 0)))))) ?

3

On définit une fonction de l’ensemble des propositions de la logique du premier ordre dans elle-même – |P (t_{1}, ..., t_{n})| = K,

– |A ⇒ B| = |A| ⇒ |B|,

– |A ∧ B| = |A| ∧ |B|,

– |A ∨ B| = |A| ∨ |B|,

– |¬A| = ¬|A|,

– |⊥| = ⊥,

– |∀x A| = ∀x |A|,

– |∃x A| = ∃x |A|.

(1) Soit B la proposition ∀x ∀y (S(x) = S(y) ⇒ x = y). Calculer la proposition |B|.

(2) Montrer que |A[x ← t]| = |A|.

(3) Quelles sont les variables libres de |A|?

(4) Dans le langage de l’arithmétique, on appelle T la théorie modulo sans axiomes avec les règles de calcul suivantes :

0 + y → y
S(x) + y → S(x + y)

(5) Montrer que si la proposition A est équivalente à A′ alors |A| = |A′|.

(6) Montrer que si A est démontrable dans la théorie T alors |A| est démontrable dans la théorie vide. La réciproque est-elle vraie ?

(7) Montrer qu’on peut associer à chaque démonstration π de A une démonstration |π| de |A| telle que si π contient une coupure, alors |π| aussi et de plus si π′ est obtenue en éliminant une coupure dans π alors |π′| est également obtenue en éliminant une coupure dans |π|.

(8) Démontrer que l’élimination des coupures dans T termine.