Ce que j'ai fait en cours ce 17-12-07, 8h15

• Les 4 sens du verbe "être" d'après Frege
• La phrase d'Aristote et la critique de objet/est/attribut
• Et la naissance de la chimie avec Lavoisier
• La boxologie. Ce n'est pas parce qu'on met dans des boîtes que l'on fait du "conceptuel"
• un schéma relationnel "n-aire" à la Codd
• et

Notion de séquent : H |- P où H, collection d'hypothèses et P conjecture à prouver. Hypothèses et conjecture sont des prédicats. Ces prédicats peuvent être écrits en utilisant le symbole => (à ne pas confondre avec le tourniquet |- (turnstile en anglais))

H |- P se lit : H entraîne P ou encore Prouver P sous les hypothèses H

exemples :

s <: t, t <: u |- s <: u

|- 0 = 0

Notion de règle d'inférence :

séquent 1

....

séquent n

__________________

séquent

Les séquents au-dessus du trait sont les antécédents de la règle, celui au-dessous est le conséquent de la règle.

Usage de la règle par l'avant : le preuve de séquent dérive de celles de séquent1,..., séquent n. De la preuve de séquent1, ..., séquent n on dérive celle de séquent.

Usage de la règle par l'arrière : on voudrait prouver séquent. On remplace ce but par ceux corrrespondants à la preuve des séquents séquent1, ..., séquent n.

Ne pas confondre le => (implication) Prédicat => Prédicat

avec le |- (entraîne) Prédicat1, prédicat2 - Prédicat3

avec le trait horizontal (de la preuve des séquents, on déduit la preuve du séquent)

Et j'ai fini par :

Les règles de base du raisonnement mathématique :

• Hypothèse : si un prédicat fait partie des hypothèses, alors il est prouvé
• Monotonie : la preuve d'un prédicat sous certaines hypothèses n'est pas remis en cause par l'ajout d'hypothèses supplémentaires
• Coupure : si un prédicat est prouvé sous certaines hypothèses alors ce prédicat peut être ajouté à ces hypothèses si besoin est.

en conseillant aux élèves intéressés par le cours de lire, dans le silence qu'on ne peut obtenir dans l'amphi, le chapitre du poly sur la preuve (ou de me demander le cours en vidéo de J.R. Abrial sur la preuve).

Je voulais aussi rappeler ce qu'est :

• la décidabilité
• la semi-décidabilité

Mais il y a des messages sur ce bloc-notes qui traitent de cette question du DS