12 semaines de cours le vendredi 8h-9h30 au Petit Amphi Valrose ; 1er cours le 31 janvier
12 semaines de TD (1h30) ; début des TD lundi 3 février
1ère interrogation vendredi 14 mars en seconde partie du cours.
2ème interrogation en TD la semaine du 5 mai.
Au programme :
- Enoncés : construction (et, ou, négation, implication, etc), valeur de vérité, équivalence entre énoncés, implication entre énoncés (on distingue l'équivalence à l'intérieur d'un énoncé d'une équivalence entre énoncés et on explique le lien entre les deux).
- construction d'objets mathématiques (comme une application linéaire, une matrice de nombres réels, une suite de nombres rationnels) avec leurs types (les définitions dans les textes usuels)
- preuves : notion de théorème (ou proposition ou lemme...) avec le type d'objets dont ils parlent, l'hypothèse, la conclusion ; preuve vue comme un algorithme, vérification de preuve.
Tout ceci sera illustré par des éléments de cours d'analyse et d'algèbre de première année (par exemple pourquoi les opérations sur les lignes et les colonnes transforment un système d'équations linéaires en un système équivalent).
Progression du cours :
| 1. (31jan) Introduction au cours. Document projeté. 2. (7fev) Enoncés : quantifiés ou pas, portant sur des objets mathématiques (voir prochain cours), avec une valeur de vérité (pas forcément connue), avec éventuellement une preuve dans un contexte donné (théorème) ; relations de déduction entre énoncés (voir plus tard), Résumé d'un énoncé (ex. f est continue, f est bornée, etc.), résumé d'un objet : constantes dans les énoncés ; variable liée par un quantificateur, variables libre ; un énoncé dit quelque chose sur les variables libres et sur les constantes de l'énoncé. Opérations "non", "ou" sur les énoncés et définition de leurs tables de vérité ; opérations "et", "⇒", "⇔", calcul de leurs tables de vérité. Valeur de vérité des énoncés ∀x, P(x) et ∃x, P(x). Lectures, etc. : Les fondements des mathématiques par J-Y. Girard sur canal-u, 3. (14fev) Retour sur les énoncés sans quantificateur formulés avec ⌉ (non), ∨ (ou), ∧ (et) et des parenthèses. Valeur de vérité en logique classique, principe du tiers exclus, influence sur les preuves ex. existence de a,b irrationnels tels que ab soit rationnel. Notation P≡Q si les énoncés P et Q ont les mêmes valeurs de vérité (éventuellement fonction de variables libres de type "énoncé"), ex (P∨Q) ≡ ⌉(⌉P∧⌉Q), (∃x, P(x)) ≡ ⌉(∀x, ⌉P(x)). Calculs dans l'algèbre F2 et calculs des valeurs de vérité des énoncés sans ou avec quantificateur. Objets mathématiques (ce dont parlent les énoncés) : pot pourri ; dans l'ordre des fondations : énoncés (objets pour la logique), ensembles et applications, entiers naturels suites et nombres, algèbre et analyse. 4. (21fev) Relation d'égalité (=) et substitution de variable dans les énoncés. Théorie des ensembles : tous les objets sont des ensembles ; relations binaires =, ∈ (appartenance), lien entre les deux, ⊂ (inclusion) ; construction d'ensemble {x|P(x)} "l'ensemble des objets x vérifiant la propriété P", on a besoin de restreindre cette construction suivant certaines règles sinon on tombe sur des paradoxes tels que {x| x∉x}∈{x| x∉x} est à la fois Vrai et Faux. Qq règles de construction (axiomes) : ∅:={x|Faux}, paire : {z|z=a ou z=b} est un ens. noté {a,b}, réunion {z|∃x, z∈x et x∈X} est un ens. noté ∪X, ens. des parties {z|z⊂X} est un ens noté P(X), axiome de séparation {x| x∈X et P(x)}, qu'on note plutôt {x∈X|P(x)}, pour P une propriété portant sur les éléments de X, est un ens. Représentation ensembliste d'un couple (a,b) par {{a},{a,b}}, produit cartésien d'ensembles X×Y, représentation ensembliste d'une application f:X→Y (relation fonctionnelle) par son graphe {(x,y)|y=f(x)}. Rq X×Y, X→Y sont des objets typés : leur sont associées des constructions telles que les projections sur chaque composante (pour le produit cartésien), l'évaluation (pour les applications), etc. Lectures : Théorie naïve des ensembles sur Wikipedia (en anglais) 5. (7 mar) Synthèse : En théorie des ensembles tout objet est de la forme {x|P(x)} mais cette construction ne détermine pas toujours un ensemble : règles de construction ou axiomes. Type d'un objet : ensemble des énoncés et des constructions qui s'applique à cet objet, dépend du contexte ; ex. 0∈1 est un énoncé licite en théorie classique des ensembles (où tout objet est un ensemble) mais n'est pas licite lorsqu'on considère 0 et 1 comme de type entier ; l'énoncé "f est injective" indique que f est de type application, etc. Type couple (a,b) : 1er et 2nd élément du couple, égalité entre couples, produit cartésien A×B, relation sur A×B, graphe d'une relation, relation fonctionnelle sur A×B, application de A dans B. Type fonction A→B : constructions f(x), f-1(y), Df (domaine de définition), ensemble BA des applications A→B, énoncés "f est bien définie", " f est injective", "surjective", "bijective". Ensemble des entiers N et type entier : N,0∈N, S:N→N (successeur : S(n)=n+1) satisfaisant les axiomes de Peano. Démontration d'un énoncé ∀n∈N, P(n) par récurrence, construction d'une suite d'objets (un) par récurrence, ex. x0∈R et f application R→R étant donnés, existence et unicité d'une suite (un) vérifiant u0=x0 et ∀n∈N, un+1=f(un). Lecture : Type informatique (voir aussi Théorie des type), Axiomes de Peano sur Wikipedia. 6. (14 mar) Au programme : quelques constructions liées aux entiers : addition, multiplication des entiers, relation d'ordre Interrogation (45mn) 7 (21 mar) Introduction aux séquents et aux preuves. Un séquent Γ |- B se lit "Dans le contexte Γ on a B" Lectures Le calcul des séquents sur Wikipedia, voir aussi la version anglophone. 8. (4 avr) Séquents associé à un axiome ou un théorème suivant sa formulation, déclaration des variables libres et des hypothèses sur ces variables. Exemple avec le théorème "Toute partie non vide majorée de R admet une borne supérieure", commentaire sur le type R (ensemble des nombres réels, relations binaires (=,<), opérations (+,×÷,...), énoncés (x est irrationnel, etc)). Règles gouvernant le passage gratuit d'un séquent à un autre ; règles de réécriture (remplacement d'un énoncé par un énoncé équivalent). Document pour la suite du cours. 9. (11 avr) Enoncés quantifiés ou avec variables libres, ex "Toute partie non vide de R admet une borne supérieure", "Toute famille de n+1 vecteurs de Rn est liée", traduction en terme de séquents, règle (|-∀) permettant de passer des uns aux autres. La règle (|-∀) permet d'attribuer une valeur de vérité à un énoncé de la forme ∀x∈X,P(x) lorsque X est infini (si X est fini, X={x1,...,xn} alors ∀x∈X,P(x) est équivalent à (P(x1) et ... et P(xn)) ), exemple avec ∀x:R,x2+x+1>0. Autres règles du calcul des séquents gérant les quantificateurs : (|-∀), (∃|-), (∀|-)[x0] (particulariser une hypothèse), (|-∃)[x0] (exhiber). Les règles (|-∀) et (|-∃)[x0] permettent d'attribuer une valeur de vérité à un énoncé quantifié. Ex ∀x:R,x2+x+1>0. A faire : la règle (|-∃)[x0] permet d'attribuer une valeur de vérité à un énoncé de la forme ∃x∈X,P(x), exemple avec ∃x:R, x2+3x+1=0. 10. (18 avr) Complément sur les règles régissant les quantificateurs (|-∀), (|-∃)[t], (∀|-)[t], (∃|-), où t est une formule faisant intervenir les constantes et les variables déclarées dans le contexte. (|-∃)[t] et (∀|-)[t] ne sont pas gratuites : il faut choisir t ; seule aide : t s'exprime avec les variables libres du contexte et les constantes. Gestion des variables liées lors de l'application des règles (|-∀) et (∃|-), ex. preuve du séquent [ a:]0,+∞[ , ln est croissante sur ]0,+∞[ |- ln est minorée sur [a,+∞[ ] d'abord en formalisant puis (|-∃)[ln(a)] , (|-∀) Ce qu'on sait : définition explicite d'un terme par une formule (ex ln(x):=∫1xdt/t), implicite par une propriété caractéristique (ex exp est la solution de l'eq. diff. y'=y vérifiant y(0)=1), énoncés liés au type d'une constante (ex. règle des signes pour l'addition et la multiplication des nombres réels), théorèmes, ce qu'on a déjà prouvé. 11. (25 avr) Exploitation de ce qu'on sait : particularisation d'un théorème Γ,x:T,P(x)|-Q(x) en Γ,P(t)|-Q(t) où t est une formule (une expression) en les constantes et les variables libres déclarées dans Γ , règle pour l'égalité, règle du Modus Ponens. Exemple avec la preuve de |- ln(2)>0 partant de ln(1)=0, ln'(x)=1/x, 1/x>0 si x>0 et le théorème I: intervalle de R et f:I→R dérivable de dérivée >0 sur I alors f est strictement croissante. Règle distinguer suivant H ou plus généralement suivant H1,..., Hn ; exemple avec la preuve que toute famille de deux vecteurs du R-espace vectoriel R est liée. Preuve = succession d'applications de règles partant de ce qu'on sait aboutissant au séquent à prouver. Esquisse de preuve, preuve déductive (on part de ce qu'on sait), preuve à l'envers : ramener la preuve de Γ|-B à celles d'une liste de séquents plus simples ou plus proches de ce qu'on sait. 12. (9 mai) Preuves d'existence et d'unicité, exemple avec l'énoncé "L'équation x3/3+x2/2+x+1=0 admet une et une seule solution réelle" puis avec l'existence de {a,b,c} en théorie axiomatique des ensembles. Exploitation d'un résultat d'existence dans une preuve. Storyboard
 |
Documents du cours :
Feuille de TD 1 (3 fev)
Feuille de TD 2 (10 fev)
Feuille de TD 3 (17 fev), corrigé de quelques questions
Feuille de TD 4 (3 mar), corrigé de quelques questions.
Interrogation du 14 mars et un corrigé.
Feuille de TD 5 (31 mar)
Feuille de TD 6 (7 avr) Quelques réponses aux exercices.
Interrogations du 5 mai avec un corrigé.
Feuille de TD 7 (5 mai) et un corrigé.
Examen du 10 juin. Un corrigé (23mar16).
Lectures :
Le cours de 2011-12 par A. Hirschowitz, les exercices WIMS, un corrigé de l'examen (sur feuille) de juin 2013
J-Y. Girard, La théorie de la démonstration, Leçons de mathématiques d'aujourd'hui Vol 2, Cf cette page.
Liens :
La page du cours de Méthodologie en 2001-04
page de la Licence 1ère année - sciences fondamentales, page du Département de mathématiques