Hänvisningarna är till kursboken "Logic and Structure".
Föreläsning 3 november
En allmän introduktion till matematikens grundvalar.
Föreläsning 5 november
1.1.
Syntax för satslogik (Def. 1.1.1). Induktiva definitionen av PROP,
mängden av de
satslogiska formlerna (Def. 1.1.2). Bevis med induktion (Thm 1.1.3)
och definition med rekursion (Thm 1.1.6). Definition 1.1.4 (och det
som beror på den, dvs allt om "formation sequences") hoppar vi
över, annars är det mesta på sidorna 5-14 läsbart; Thm 1.1.8 dock
överkurs.
1.2.
Vi definierade begreppet valuering (Def 1.2.1, Thm 1.2.2), tautologi
och satslogisk konsekvens (Def 1.2.4).
1.4.
Reglerna for konjunktion, implikation och negation i naturlig
deduktion. Vi gjorde två små härledningar; dessa kan du se
om du öppnar filen /users/mdstud/smith/alfa/5_nov i Alfa (som du
startar med kommandot alfa).
Föreläsning 10 november
1.3
Vi visade att negation och konjunktion bildar en fullständig mängd av
konnektiver. Vi visade också att nand (Sheffers streck) är ett
fullständigt konnektiv och att nand och nor är de enda fullständiga
binära konnnektiverna (övningarna 4-6 sid. 28).
Thm 1.3.6 "visade" vi med ett exempel enligt övning 7 sid. 28; detta
illustrerade också disjunktiv normalform.
Det mesta i avsnitt 1.3 är nyttigt men jag kommer inte att ta upp
mer i det.
1.6 Reglerna för disjunktion i naturlig deduktion. Vi gjorde 3
härledningar i naturlig deduktion; dessa kan du se om du öppnar filen
/users/mdstud/smith/alfa/10_nov i Alfa.
Föreläsning 12 november
Brouwer-Heyting-Kolmogorov tolkningen av påståenden. Påståenden som
typer. Detta finns på de första sidorna i kapitel 5; en mer
detaljerad beskrivning finns i avsnittet "Propositions as sets" i
Type theory and Programming.
Andra
timmen demonstrerade Thomas Hallgren Alfa.
Föreläsning 17 november
Vi bevisade sundhetssatsen (Lemma 1.5.1 sid 40) och började på beviset
av fullständighetssatsen (Thm 1.5.13 sid 46).
Naturligtvis gjorde vi en härledning i naturlig deduktion, den finns i
/users/mdstud/malo/17_nov och kan studeras i Alfa. Härledningen
använder lagen om det uteslutna tredje, LEM, vilken ni skall visa i
satslogiklabben; därför utelämnade jag härledningen av LEM.
Föreläsning 19 november
Vi gjorde färdigt fullständighetsbeviset för satslogik. På slutet tog
vi igen upp påstående som typer.
Föreläsning 24 november
Vi började på kapitel 2 (sid 57 - 64).
Föreläsning 26 november
Reglerna i naturlig deduktion för predikatlogik. Vi gjorde ett antal
exempel som du kan titta på genom att öppna ~/malo/26_nov i Alfa.
Föreläsning 1 december
Avsnitt 2.4 om Tarskis semantik för predikatlogik.
Föreläsning 3 december
Avsnitt 5.3 sid. 166-169 om Kripke modeller, men endast för
satslogik. Exemplen på sid 169 är bra.
Föreläsning 8 december
Allmän diskussion om axiomsystem. Axiomen för grupper (sid. 85). Peanos
aritmetik (sid. 87). Och så började vi på beviset av
fullständighetssatsen (sid. 105-107).
Föreläsning 10 december
Vi avslutade beviset av fullständighetssatsen och visade hur
kompakthetssatsen kan användas för konstruktion av
icke-standardmodeller för aritmetik.
Föreläsning 15 december
Mer om icke-standardmodeller. Prenex normalform (sid. 78).
Föreläsning 17 december
Gödels ofullständighetssats.
Upp: Matematisk logik