A l’occasion de la
première journée mondiale de la logique http://www.logica-universalis.org/wld
le 14 janvier 2019 (jour de la naissance d’Alfred Tarski et
de la mort de Kurt Gödel, suivant une idée de J.-Y. Beziau)
nous proposons, à Montpellier, quelques exposés de vulgarisation
scientifique.
LUNDI 14 JANVIER 2019 15:00-19:00 Salle SC 001 Polytech
(bâtiment 31), Campus Triolet (campus sciences), Université de
Montpellier
UNE HISTOIRE DE LA LOGIQUE MATHEMATIQUE : DE LA PHILOSOPHIE A
L'INFORMATIQUE
D’Aristote à la scolastique, la logique fut placée au commencement
des études et traités de philosophie,
afin que le philosophe raisonne sur tout sujet avec une rigueur
comparable à celles des mathématiques.
En dépit de quelques contributions isolées, il faut attendre la
fin du XIXe, avec le questionnement
sur les fondements et la cohérence des mathématiques,
pour que la logique se renouvelle et revienne au premier plan de
la scène scientifique.
Ce mariage entre logique et mathématique
a évidemment connu des succès en mathématiques,
mais il a aussi intensément contribué au développement de la
notion de calcul et de l’informatique,
dès la seconde guerre mondiale, en raison des liens entre
décidabilité et calculabilité.
Nous retracerons le développement de la logique mathématique au
XXe siècle,
nous nous pencherons plus particulièrement sur la notion de calcul
et de preuve formelle.
VÉRITÉ VERSUS VALIDITÉ À LA LUMIÈRE DE LA MÉTHODOLOGIE DES
SCIENCES DÉDUCTIVES DE TARSKI
Dans sa quête d'une définition sémantique de la la vérité, Tarski
introduit deux notions très simples qui vont se révéler très
fécondes:
la notion de satisfaction d'une phrase ouverte par un élément de
l'univers du discours
et la notion de modèle d'une formule dans un domaine
d'interprétation donné.
ceci est au coeur de la méthodologie des sciences déductives qui
articule syntaxe et sémantique
et permet de clarifier les relations entre vérité dans une
interprétation et validité logique.
Après avoir présenté les principaux aspects de cette élaboration,
j’illustrerai sur un exemple simple la fécondité de cette
approche.
LA LOGIQUE DANS LE DEBAT PUBLIC
Pour Aristote, la logique était une arme pour se défendre des
beaux parleurs, qu’en est-il aujourd’hui dans les débats
sciences/sociétés.
Peut-on fonder sur la logique la confiance la participation et la
créativité des débats.
PROUVER UN PROGRAMME, ÇA VEUT DIRE QUOI ?
En Informatique, certains systèmes sont dits critiques en ce sens
qu'un bug informatique peut provoquer
une défaillance du système dont les conséquences peuvent être
potentiellement catastrophiques (pertes humaines,
pertes financières, conséquences graves pour l'environnement,
etc.). Ainsi, le développement
de ces systèmes nécessitent l'utilisation de méthodes spécifiques
permettant d'assurer la production de logiciels sûrs.
Ces méthodes sont appelées méthodes formelles.
Parmi ces méthodes, il y a en particulier les méthodes déductives
reposant principalement sur l'utilisation de la logique,
et appelées également preuve de programme. L'idée consiste à
spécifier formellement le comportement du programme
au moyen de la logique et à faire une preuve que le programme est
conforme à cette spécification.
Cet exposé s'adresse essentiellement aux curieux qui veulent
comprendre
sur des exemples simples les différents principes cachés derrière
la preuve de programme.