Dimanche 23 mars 2008
Suite de l’examen de « l’approche formelle» (15 et 16 janvier 2007). Réflexion sur le « VRAI ».
Revenons à la démonstration de l’exemple précédent.
E10 : QUELQUESOIT a APPARTIENT N QUELQUESOIT b APPARTIENT N* ILEXISTEUNSEUL q APPARTIENT N ILEXISTEUNSEUL r APPARTIENT N, a = b * q + r ET r < b. COMPLEMENT : q
= QUOTIENT(a,b) ET r = RESTE (a,b)
E11 : 2 APPARTIENT N
E12 : 10 APPARTIENT N*
E13 : 0 APPARTIENT N
E14 : 2 = 0 * 10 + 2
E15 : 2 < 10
Donc E 16 : RESTE (2,10) = 2
E 17 :QUELQUESOIT n APPARTIENT N Fin(n) = Reste (n,10)
Donc E18 : Fin(2) = 2.
E19 : QUELQUESOIT n APPARTIENT N Fin(n) = 2 => Paire(n) = VRAI.
Donc E 20 : Paire(2) = VRAI.
Rappel (on voulait arriver à E20 « 2 est pair »).
On remarque que lorsque l’on écrit tous ses énoncés, on sous-entend toujours qu’ils sont vrais.
E10 est VRAI (démonstration supposée établie, il comporte aussi des définitions).
E11, E12 et E13 sont VRAIS. Cela devrait être justifié par la définition de N’et N*).
E14 et E15 sont VRAIS. Cela devrai être justifié par les définitions de la multiplication, de l’addition, de la relation de comparaison « < ».
Donc E 16 … VRAI
E 17 est VRAI (définition de Fin)
Donc E18 VRAI
E19 est VRAI (c’était l’assertion de « départ » ; en pratique est très réduite).
Donc E 20 …VRAI.
Les « donc » sont les articulations de la démonstration. Il s’agit d’une relation sur les énoncés. L’énoncé d’entrée est fréquemment le regroupement (par des ET)
de plusieurs énoncés. Le fait que E16, E18 et E20 soient VRAIS sont des productions de la démonstration.
Il est intéressant d’examiner ces « donc » pour comprendre les règles de démonstration.
Le premier « donc » utilise E10 et identifie les variables a=2, b = 10, q = 0, r = 2. E11, E12 et 13 justifient les conditions. E14 et E15 montrent que
les 2 expressions sont satisfaites. En conséquence, r = 2 est bien l’unique RESTE(2,10). Dit autrement : « il y en a un unique, j’en trouve un, c’est donc celui là ».
Le deuxième « donc » utilise E11, E16 et E17 (et la transitivité de =).
Le troisième « donc » utilise E11, E18 et E19. Il exploite la définition de «=> ».
Donc et =>
On peut écrire un énoncé en utilisant =>
On rédige une démonstration en utilisant « donc ». Mais une démonstration est en aussi un énoncé. Le texte précédent peut être réécrit en rajoutant des
« VRAI », des () et en remplaçant donc par =>. C’est fastidieux et pas particulièrement lisible. On aboutit à un énoncé E99.
On veut une « bonne » démonstration. Quelle est la contrainte sur E99 ?
Plutôt que E99, restreignons nous à E 100 pour le deuxième « donc ».
E100 : {E11 (2 APPARTIENT N ) VRAI ET E16(RESTE (2,10) = 2 ) VRAI ET [E17 :QUELQUESOIT n APPARTIENT N Fin(n) = Reste
(n,10)] VRAI } => {(E18 : Fin(2) = 2) VRAI }.
E11, E16, E17, et E18 ne sont là qu’à titre de repère. Si on les enlève, on a :
E100 : {(2 APPARTIENT N ) VRAI ET (RESTE (2,10) = 2 ) VRAI ET [QUELQUESOIT n APPARTIENT N Fin(n) = Reste (n,10)] VRAI }=>
{(E18 : Fin(2) = 2) VRAI}.
La démonstration est « bonne » parce que l’énoncé E100 est VRAI. Pourquoi E100 est VRAI ? Détaillons.
On identifie n à 2 dans E17. C’est licite grâce à E11. D’où [Fin(2) = RESTE(2,10)] VRAI.
Grâce à E16 et à la transitivité de « = », on obtient bien E18.
La puissance de l’approche formelle réside dans cette récursivité : la démonstration est un énoncé : il fait donc partie du « même univers » que les énoncés sur
lesquels il porte. Cela rejoint la fonction métalinguistique du langage (Jakobson). Cela a un prix (Godel).
On peut aussi remarquer que cette récursivité est potentiellement infinie.
E100 c’est aussi E101 : « E100 VRAI » et ainsi de suite.
Pour un énoncé VRAI ou FAUX, cette montée dans les niveaux n’a pas d’intérêt ni de conséquence. Mais pour les énoncés indécidables, qu’est-ce que cela peut engendrer ?
par thidgr
publié dans :
Errements
ajouter un commentaire commentaires (0) créer un trackback recommander
ajouter un commentaire commentaires (0) créer un trackback recommander
Commentaires