Exercice : 1) On suppose admise la règle R donnée dans l'exrcice : Montrons que l'on peut en deriver le tiers exclu: Soit P: Prop, on a P |- P (assumption) ~P |- ~ P (assumption) ----------------------------------------------------- |- P \/~P (regle R) 2) Reciproquement, si l'on admet le tiers exclu, on peut obtenir la regle R Soient A, B , C : Prop et Gamma, on suppose qu'on a Gamma, A |- B et Gamma, ~A |- C ------------- (hypothese) -------------- (hypothese) Gamma, A |- B Gamma, ~A |- C Gamma |- A \/ ~A ----------------------------------------------------------------------------- Gamma |- C (elimination du ou) Problème --------- 1ere question -------------- Definition arc (i j:Nat) := i=0 /\ j=1 \/ i=1 /\ j=2 \/ i=2 /\ j=0 \/ i=3 /\ j=0 \/ 3<=i /\ j=succ i. 2eme question a) Montrer "arc 1 2" revient a montrer 1=0 /\ 2=1 \/ 1=1 /\ 2=2 \/ 1=2 /\ 2=0 \/ 1=3 /\ 2=0 \/ 3<=1 /\ 2=succ 1. (se montre en utilisant 2 fois la regle d'introduction du "ou", une fois la regle d'introduction du "et", et la regflexivité de l'égalité. b) On doit montrer i : Nat H : 3 <= i -------------------------------- i=0 /\ j=1 \/ i=1 /\ j=2 \/ i=2 /\ j=0 \/ i=3 /\ j=0 \/ 3<=i /\ succ i =succ i. (facile : regles d'introduction du ou, du et , et de l'egalite) c) Supposons H : arc 2 1 et montrons False : L'énoncé de H devient 2=0 /\ 1=1 \/ 2=1 /\ 1=2 \/ 2=2 /\ 1=0 \/ 2=3 /\ 1=0 \/ 3<=2 /\ 1=succ 2 Par élimination du "ou" du "et" on obtient des sequents ayant toujours au moins une hypothese fausse: par exemple: 2=0 1=1 ----- False d) On doit prouver : i : Nat H : 0=0 /\ i=1 \/ 0=1 /\ i=2 \/ 0=2 /\ i=0 \/ 0=3 /\ i=0 \/ 3<=0 /\ i=succ 0. -------------------------- i=1 En eliminant les ou, puis les et dans l'hypothese H, on trouve un but trivial : 0=0 i=1 ----- i=1 et les autres cas sont triviaux : 0=1 i=2 ------ i=1 (car on peut prouver ~(0=1)) Question 3 La proposition "Connected i j" est définie de façon imprédicative : "i est connecté à j si tout ensemble X de sommets (qui contient i et tel que pour tout sommet k, si k appartient a X, alors X contient aussi tout sommet l relié à k par un arc) contient auyssi le sommet j". question 4. Preuve de "Connected 0 2" Soit X un ensemble contenant le sommet 0 et tel que pour tout sommet k, si k appartient a X, alors X contient aussi tout sommet l relié à k par un arc. alors X contient aussi 1 (car il y a un arc de 0 à 1) X contient aussi 2 (car il y a un arc de 1 à 2). On a donc montré la proposition "Connected 0 2" Preuve de forall i, Connected 0 i -> i=0 \/ i=1 \/ i=2. ------------------------------------------------------ Soit i, supposons "Connected 0 i" On considere le predicat X(i)= i=0 \/ i=1 \/ i=2. On a bien sûr X(0) de plus soit k tel que X(k), c'est à dire k=0 \/ k=1 \/ k=2 soit l tel que arc k l si k=0, alors l= 1 et on a bien X(l) (C'est à dire 1=0 \/ 1=1 \/ 1=2) si k=1 alors l=2 et on a bien X(2) si k=2 alors l=0 et on a bien X(0) On a donc X(l) D'apres la definition de Connected D'apres la definition de Connected, on a bien X(i) c'est à dire i=0 \/ i=1 \/ i=2.