Logique propositionnelle et preuves

[busard_des_roseaux]

La formule que tu cherches à prouver est une tautologie. Toutes les contorsions que tu fais (agrandir la théorie, lemme de déduction, etc) n'est que poudre aux yeux.

Il semble qu'içi, on fasse ce que tout un chacun fait tous les jours: pour démontrer A->B, on ajoute la prémisse A aux axiomes et on fait ensuite une déduction de B. Je ne vois pas ce que cela a d' "anti-naturel".

D'autre part, il est clair que la logique formelle est un secteur qu'on devrait encourager avec ses applications en démonstration automatique, en intelligence artificielle. Il y a des choses étonnantes,à l'époque moderne, par ex., que l'on puisse faire vérifier des théorèmes non triviaux par des machines, ou que des logiciels trouvent des démonstrations et étonnent leurs..créateurs (cf. théorème des 4 couleurs). On est vraiment dans le mythe faustien de la machine qui dépasse son concepteur.

[tize]

Le dépasser, je ne pense pas, par contre le compléter ou l'aider c'est sur...Il n'est pas encore dit qu'une machine puisse un jour simuler la conscience humaine...certains scientifiques (mais pas tous les scientifiques) pensent même que dans cette direction on peut un jour être confronté à des problèmes insurmontables et que la conscience humaine serait bien plus qu'un programme simulé par une machine quantique...

[busard_des_roseaux]

Le dépasser, je ne pense pas, par contre le compléter ou l'aider c'est sur...

Il ya un truc que j'ai lu qui m'a vraiment bouleversé: ceux qui ont démontré le thm des 4 couleurs avaient écrit un programme intelligent qui faisait de la démonstration automatique dans le domaine des graphes. Ses concepteurs racontent que le programme s'est mis à fonctionner "comme de manière autonome" (parce que le fonctionnement d'un programme intelligent dépend des données d'entrée puis s'alimente des données qu'il produit,qu'il est relativement imprévisible). Le programme a produit des démonstrations originales et des théorèmes nouveaux auquels ses concepteurs n'avaient pas pensé. Perso, j'avais écrit un programme qui dérivait formellement des fonctions,juste en programmant les formules que tout le monde connait :
(u+v)'=u'+v' et (vou)'=v'ou.u'
une fois écrit, mon programme dérivait des fonctions "incroyables" du style
dérivée n_ième de

car il se fichait de la complexité.Cet aspect, qu'apporte la machine, est fascinant.