Matematisk logik, HT 2000

Sidans innehåll

• Aktuellt.
• Schema.
• Vad handlar kursen om?
• Kurslitteratur.
• Kursinnehåll.
• Vad vi gjort hittills på föreläsningarna.
• Vad vi kommer att göra de närmaste föreläsningarna.
• Plan för övningar.
• Laborationer.
• Några gamla tentor.
• Lärare.

Aktuellt

OMTENTAN från 11 augusti är nu rättad!

Lektionen på torsdag flyttad till föreläsningssalen VG. Vi är alltså i VG hela förmiddagen.

Lösning till lab 2 finns i /users/mdstud/ml00/labb_predikatlogik_losning och därmed kan ni inte lämna in lab 2 längre.

Lösning till lab 1 finns i /users/mdstud/ml00/labb_satslogik_losning och därmed kan ni inte lämna in lab 1 längre.

Tentan är flyttad! Nya datumet är den 13:e januari och är på Väg och vatten 8.45-13.45. Därför flyttar vi också sista inlämningsdag för de två sista labbarna till den 12:e januari. (Tentan den 16 januari är 8.45-13.45 i VV13.)

Vad handlar kursen om?

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

Kurslitteratur

Kursbok är 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.

För den intresserade finns det en mängd bra böcker att läsa om man vill gå lite längre. En som är speciellt bra är Introduction to mathematical logic av E. Mendelson.

Kursinnehåll

Ur Hamilton:

• Kapitel 1: Hela kapitlet.
• Kapitel 2: 2.1 fram till Proposition 2.8 (som alltså inte ingår); ni behöver inte kunna göra några härledningar i systemet L. Hela avsnitt 2.2.
• Kapitel 3: Allt utom avsnitt 3.5
• Kapitel 4: Sid 73-76. Avsnitt 4.2 men ersätt alla härledningar i systemet K med härledningar i naturlig deduktion (blir enklare!). 4.3 ingår, men inte sid 91. Inga bevis i 4.4 krävs men ni måste känna till satserna 4.40 och 4.41. Avsnitt 4.5 ingår.
• Kapitel 5: Hela kapitel 5 ingår. Speciellt viktiga är avsnitten om likhet och aritmetik.
• Kapitel 6 Hela kapitlet. Speciellt viktigt är avsnitt 6.5.

Dessutom:

• Naturlig deduktion
• Kripkemodeller.

Vad vi gjort hittils på föreläsningarna

• 2 november: Jan höll en allmän introduktion till logik och matematikens grundvalar.
• 7 november: Fredrik gick igenom större delen av kapitel ett i boken. Det gick ganska snabbt och tyvärr hade jag inte tid att göra så många exempel. Sektion 1.5 hann jag inte riktigt med hela, och sektion 1.6 hoppar vi över (om det behövs går vi igenom det på övningarna).
• 9 november: Jag började med att avsluta sektion 1.5 (och därmed kapitel 1). Sedan gick jag igenom alla härledningsreglerna för konstruktiv satslogik i naturlig deduktion. Jag sa några ord om Alfa och visade några overhead för att förbereda för labben på tisdag. Till sist formulerade jag RAA och visade ett kort exempel. Två av bevisen jag gjorde på tavlan kan ses i Alfa om ni öppnar filen /users/mdstud/ml00/exempel_9_nov.
• 14 november: Jan pratade mer om naturlig deduktion och speciellt om Curry-Howard tolkningen. Han gick också igenom RAA ordentligt. Industriella applikationer av satslogik pratade han också lite om.
• 16 november: Första timmen pratade jag om kapitel 2 i boken. Jag definierade systemet L och jämförde med ND. Jag formulerade en sats som i stort sa att en formel går att bevisa i L omm den går att bevisa i L (jag gav en bevisskiss). Jag försökte också att hinna med sundhetssatsen. Jag formulerade den ordentligt och gjorde ett bevis, som pga tidbrist blev lite för odetaljerat. Jan kanske säger lite mer om detta nästa föreläsning. Andra timmen demonstrerade Thomas Hallgren Alfa. Han pratade lite om Alfa i allmänhet och visade några funktioner, tex hur man skriver ut sina bevisträd och hur man kan få dem översatta till naturligt språk.
• 21 november: Jag (för ögonblicket Jan) gick igenom större delen av Kapitel 2, men beviset av fullständighetssatsen är inte slutfört.
• 23 november: Började på predikatlogik: definition av syntaxen och reglerna i naturlig deduktion.
• 28 november: Fullständighetsbeviset för satslogik. En liten härledning i naturlig deuktion.
• 30 november: Avsnitt 3.3-4: Tolkning av ett predikatlogiskt spåk. Tarskis sanningsdefinition.
• 5 december: Kap 4, systemet K. Konstruktiv semantik för satslogik. En inte pytteliten härledning i naturlig deduktion (den klassiska drinkaren).
• 7 december: Kapitel 4: Fullständighetssatsen, kompakthetssatsen.
• 12 december: Fredrik: Kapitel 5 (5.2 och 5.4). Först definierade jag likhetsaxiomen och sa något om normala modeller. Jag visade (nästan) att till varje modell finns en elementärt ekvivalant modell, detta motiverade till att endast titta på normala modeller. Sedan ställde jag upp axiomen för PA och jämförde dem med Peanos usprungliga axiom (hans femte är inte av första ordningen utan av andra ordningen). Jag visade med hjälp av kompakthetssatsen (och fullständighetssatsen) att det finns icke-standard modeller till PA. Jag nämde också något om vad Gödels ofullständighetssats säger.
• 14 december: Jan: Nästan hela tiden användes för att gå igenom Kripkemodeller.
• 19 december: Börjar på Gödels ofullständighetssats (kapitel 6). Någon Kripkemodell. Bläddrar i boken och talar om vad som är viktigt inför tentan.
• 21 december: Kapitel 6.
• 9 januari: Repetition och uppgifter från tentan 2000-01-15.
• 11 januari: Repetition och tentaräkning.

Vad vi kommer att göra de närmaste föreläsningarna

Inga fler föreläsningar, tyvärr...

Plan för övningar

• 16 november: Kapitel 1. Exempel på bra övningar är 4, 12b, 14c, 17b, 18 och 20a,c. Naturlig deduktion för satslogik.
• 23 november: Kapitel 2. Extra bra övningar: 9, 10 och 11.
• 30 november: Kapitel 3 och ND för predikatlogik. Jag definierade vad det betyder för en term att vara fri för en variabel. Jag gjorde två härledningar i ND, den sista hann jag inte riktigt bli färdig med (det sista jag gjorde var lite fel), men bägge härledningarna finns nu i filen /users/mdstud/ml00/ovning_30_nov (tack Sofia).
• 7 december: Kapitel 3. Jag repeterade semantiken för predikatlogik och gjorde ett par övningar (3.12, 3.16 och 3.22).
• 14 december: Först tog jag upp prenexform. Sedan pratade jag lite om tentan och hur dem brukar se ut. Sista timmen visade jag att man inte kan axiomatisera ändlighet och räknade lite på kapitel 4.4 och 4.5. Jag pratade också lite kort om Lindströms sats.
• 21 december: Kapitel 6 och kripkemodeller.
• 11 januari: Repetition och tentaräkning.

Laborationer

Alfa startas med kommandot alfa - -norec . Och en härledning startas alltid med att man väljer ND Style Proof i menyn.

Det är lätt att se att labben är riktigt löst: det får inte finnas kvar några ?.

Bonuspoängen ni får på tentan får användas både på ordinarie tenta och vid första omtenta tillfället, men inte senare.

Laboration i satslogik

Lösningen: /users/mdstud/ml00/labb_satslogik_losning

Ingen av uppgifterna är stora, speciellt inte djupet på bevisträdet; härledningen av assoc-disj blir dock ganska bred. Men en del är kluriga, t ex Not_Not_LEM och de om Peirces lag.
Ni får 1 bonuspoäng för godkänt på tentan.

Laboration i predikatlogik

Lösningen: /users/mdstud/ml00/labb_predikatlogik_losning

Ni får 1 bonuspoäng för godkänt på tentan.

Laboration om konstruktivt drinkarproblem

Denna lab är en omformulering av den sista uppgiften i predikatlogiklabben, så att den är konstruktivt giltig. Den är nog klart svårare än den klassiska drinkaren. Korrekt lösning ger en halv poäng på VG gränsen. Och ingen ledning kommer att ges! Och självfallet skall den lösas utan RAA!

Laboration om Kripkemodeller

Detta är en en labb om Kripkemodeller i vilken sundhet och fullständighet för fragmentet av satslogik som endast innehåller implikation och konjunktion visas. Detta är en svår labb och kommer att ge 1 bonuspoäng för VG. Det finns mycket kommentarer i labben och många av bevisen är redan genomförda.
I det här beviset skall man inte använda ND style proof! Och Alfa måste startas utan flaggan norec eftersom det finns rekursiva anrop!
För att förstå syntaxen är det lämpligt att titta på Agdas hemsida. Jag har också gjort en liten uppvärmingsfil, med några enkla exempel från sats- och predikatlogik.

/users/mdstud/ml00/uppvarmning.kripke

med lösningar

/users/mdstud/ml00/uppvarmning.kripke.lösn

Några gamla tentor

• Oktober 96
• Oktober 97
• Januari 99
• Januari 00 GU
• Januari 00 CTH
• Några gamla tentauppgifter

Lärare

• Kursansvarig och föreläsare är Jan Smith.
• Övningsledare är Fredrik Engström och Henrik Seppänen.
• Laborationshandledare är Anders Claesson.