Matematisk logik HT 99
Kursen ger en introduktion till logik. Två viktiga mål med kursen är
att
- förstå vad ett bevis är
- lära känna ett formellt bevissystem
Vi kommer att behandla sats- och predikatlogik och göra bevis i
ett formellt system som kallas naturlig deduktion. En rad egenskaper
hos sats- och predikatlogik kommer att visas; bl a fullständighet
vilket visar att ett påstående är en logisk sanning om och endast om
den går att bevisa i naturlig deduktion. Vi kommer även att ta upp
Gödels ofullständighetssats som säger att det finns ingen fix mängd av
axiom från vilka alla aritmetiska sanningar kan visas.
Laborationer
Vi kommer att använda beviseditorn
Alfa, i
vilken man kan göra bevis i naturlig deduktion på dator.
Alfa använder sig av
beviskontrolleraren
Agda,
som också har ett
emacsgränssnitt.
Det kommer att bli två laborationer,
en i satslogik och en i predikatlogik. Dessutom finns möjlighet
att göra ytterligare en laboration i predikatlogik och en
om Kripkemodeller (den är dock svår!)
Kursbok
Logic for Mathematicians, författad av A. G. Hamilton och
utgiven på Cambridge University Press. Det är en pedagogisk och
välskriven bok som dock inte tar upp naturlig deduktion, vilket jag
därför skriver
några sidor
om; samma gäller om
Kripkemodeller,
som heller inte finns med i boken. Ur Hamilton ingår
kapiteln 1-6; för er som läser på Chalmers utgår kapitel 6.
Kursplan
Jag vill inte att ge en detaljerad plan för föreläsningarna redan nu.
Men efter varje föreläsning kommer jag att på den här sidan tala om
vad vi gått igenom samt vad som planeras för nästa föreläsning.
OBS! Ändring: tisdagen 7 december skall vi vara i HA2!
OBS! Extra övningar 8.00-9.45 tis 11 januari i MD1 och MD3.
Omtentamen är 18 april.
Jan Smith (kursansvarig)
Anders Claesson,
Fredrik Engström,
Henrik Seppänen (övningsledare)
Senast ändrad 00-05-02 kl 13.00