DD1351 Logik för dataloger 7,5 hp

Tillfälleskod	Termin(er)	Period(er)	Föreläsare
51105	HT2024	1-2	Johan Karlander

Föreläsning 1

Satslogik används för att ta reda på sanningsvärdet (T/F) hos satser.

Enkla satser: Anges med booleska variabler \(p,q,r\).
Sammansatta satser: Byggs upp med konnektiv \(\lnot\) (inte), \(\land\) (och), \(\lor\) (eller), \(\rarr\) (medför, om...så)

Konnektiv

Sanningsvärdestabeller: (från bas-matte) För "och":

\(\land\)	T	F
T	T	F
F	F	F

..."eller":

\(\lor\)	T	F
T	T	T
F	T	F

...implikationen \((p\rarr q)\), som även kan formuleras som \(\iff\lnot p\lor q\):

→		p
		T	F
q	T	T	T
	F	F	T

Logisk analys av resonemang

Tre påståenden, som vi antar är sanna:

1. Om tåget kommer för sent och det inte finns en taxi vid stationen så blir John sen till sitt möte.
2. John blir inte försenad till sitt möte.
3. Tåget kom för sent.

Slutsats: Det finns en taxi vid stationen.

Detta är sant genom påståendenas syntaktiska form (och inte genom semantisk form). Dvs. det räcker att se meningarnas struktur (och ej semantik/ordförståelse) för att kunna nå slutsatsen.

Satslogik är en metod för att avgöra sanning genom syntaktisk form.

Anta att \(\begin{cases}p&:\text{tåget kommer för sent}\\q&:\text{det finns en taxi vid stationen}\\r&:\text{John kommer för sent till mötet}\end{cases}\)

Resonemanget är att \(p\land\lnot q\rarr r\), \(\lnot r\) samt \(p\) alla är sanna, vilket ger slutsatsen \(q\).

Förenklad syntax: 1:a påståendet är förenklat, och kan formellt skrivas \((p\land(\lnot q))\rarr r\). Tolkningen av den förenklade formen avgörs av bidningsregler:

Svag		Stark
\(\rarr\)	\(\{\lor,\land\}\)	\(\lnot\)

Obs! \(p\lor q\land r\) är meningslöst. Parenteser behövs.

Föreläsning 2 (2024-09-02)

Från inspelad föreläsning + boken

Naturlig deduktion

Givet ett antal premisser \(\phi_1,\phi_2,\dots,\phi_n\) kan man härleda satsen \(\psi\). Detta kan formuleras som en sekvent:

\[\phi_1,\phi_2,\dots,\phi_n\vdash\psi\]

Om inget står till vänster om sekventsymbolen \(\vdash\), kan satsen bevisas utan premisser.

Regler:

• Och-introduktion: \(\frac{\phi\quad\psi}{\phi\land\psi}\land\text i\)
• Och-eliminering: \(\frac{\phi\land\psi}{\phi}\land\text e_1\) eller \(\frac{\phi\land\psi}{\psi}\land\text e_2\)

Bevisexempel: Bevis av \(p\land q,r\vdash q\land r\):

\[\begin{align*}&1.&&p\land q&&\text{premiss}\\&2.&&q&&\land\text e_2\ 1\\&3.&&r&&\text{premiss}\\&4.&&q\land r&&\land\text i\ 2,3\end{align*}\]

• Implikations-eliminering (modus ponens): \(\frac{\phi\quad\phi\rarr\psi}{\psi}\rarr_\text e\)

Bevisexempel: Bevis av \(p\rarr(q\rarr r),p\land q\vdash r\):

\[\begin{align*}&1.&&p\rarr(q\rarr r)&&\text{premiss}\\&2.&&p\land q&&\text{premiss}\\&3.&&p&&\land\text e_1\ 2\\&4.&&q\rarr r&&\rarr_\text e\ 3,1\\&5.&&q&&\land\text e_2\ 2\\&6.&&r&&\rarr_\text e\ 5,4\end{align*}\]

• Implikations-introduktion: \(\frac{\boxed{\begin{aligned}\small\phi\\\small\psi\end{aligned}}}{\small\phi\rarr\psi}\rarr_\text i\)

  Exempel: Vi visar att \(\vdash p\land q\rarr q\).

  \[\begin{aligned}&\begin{aligned}&1.&\\&2.&\end{aligned}\boxed{\begin{aligned}&p\land q&\text{antagande}\\&p&\land\text e_1\ 1\end{aligned}}\\&\begin{aligned}&3.&\end{aligned}\begin{aligned}&p\land q\rarr p&\rarr_\text i\ 1\text-2\end{aligned}\end{aligned}\]

  I det inrutade "delbeviset" gjorde vi först ett antagande (\(p\land q\)), och kom i slutet fram till \(p\). Detta medför att \(p\land q\rarr p\).

Exempel: \(p\land q\rarr r\vdash p\rarr(q\rarr r)\) kan bevisas:

\[\begin{aligned}&1.&&\begin{aligned}p\land q\rarr r&&&\text{premiss}\end{aligned}\\&\begin{aligned}&2.\\&3.\\&4.\\&5.\\&6.\end{aligned}&&\fbox{$\begin{aligned}&\begin{aligned}&p&&&&&&&\text{antagande}\end{aligned}\\&\fbox{$\begin{aligned}&q&&&\text{antagande}\\&p\land q&&&\land_\text i\ 2,3\\&r&&&\rarr_\text e\ 4,1\end{aligned}$}\\&\begin{aligned}&q\rarr r&&&&&&\rarr_\text i\ 3\text-5\end{aligned}\end{aligned}$}\\&7.&&\begin{aligned}p\rarr(q\rarr r)&&\rarr_\text i\ 2\text-6\end{aligned}\end{aligned}\]

• Dubbel negation: \(\frac{\phi}{\lnot\lnot\phi}\tiny\lnot\lnot\text i\) (introduktion) samt \(\frac{\lnot\lnot\phi}{\phi}\tiny\lnot\lnot\text e\) (eliminering)

Regler: copy

Vi bevisar \(\vdash p\rarr(q\rarr p)\) på följande sätt:

\[\begin{aligned}&\begin{aligned}&1.\\&2.\\&3.\\&4.\end{aligned}&&\fbox{$\begin{aligned}&\begin{aligned}&p&&&&&&&\text{antagande}\end{aligned}\\&\fbox{$\begin{aligned}&q&&&&&\text{antagande}\\&p&&&&&\text{copy 1}\end{aligned}$}\\&\begin{aligned}&q\rarr p&&&&&&\rarr_\text i\ 2\text-3\end{aligned}\end{aligned}$}\\&5.&&\begin{aligned}p\rarr(q\rarr p)&&\rarr_\text i\ 1\text-4\end{aligned}\end{aligned}\]

Vårt första antagande är \(p\). Vi antar sedan \(q\), och eftersom vi redan vet att \(p\), kan vi upprepa detta (kallas för copy). Då kan vi skriva att \(q\rarr p\), vilket är detsamma som står till höger om implikationspilen i uttrycket \(p\rarr(q\rarr p)\), och hela detta uttryck har alltså visats.

Obs! Copy får endast göras från tidigare rader, och förutsätter även att vi aldrig lämnar en box.

Motsägelse (\(\bot\))

Om vi påstår att både \(\phi\) och \(\lnot\phi\) gäller har vi en motsägelse, och påståendet är falskt.

Motsägelser kan ändå vara användbara i hypotetiska resonemang: om \(\phi\) leder till \(\bot\), kan vi dra slutsatsen \(\lnot\phi\).

• Introduktion: \(\frac{\quad\boxed{\begin{aligned}\small\phi\\\small\bot\end{aligned}}\quad}{\small\lnot\phi}\small\lnot\text i\)
• Eliminering: \(\frac{\phi\quad\lnot\phi}{\bot}\small\lnot\text e\)

Exempel: Motbevisa med motsägelse.

\[\begin{aligned}&1.&&p&&\text{premiss}\\&2.&&p\rarr q&&\text{premiss}\\&3.&&\lnot q\land r&&\text{premiss}\\&4.&&q&&\rarr_\text e\ 1,2\\&5.&&\lnot q&&\land\text e_1\ 3\\&6.&&\bot&&\lnot\text e\ 4,5\end{aligned}\]

Exempel: Bevis av \(p\land\lnot q\rarr r,\lnot r,p\vdash q\).

\[\begin{matrix}&\begin{aligned}&1.&&p\land\lnot q\rarr r&&\text{premiss}\\&2.&&\lnot r&&\text{premiss}\\&3.&&p&&\text{premiss}\end{aligned}\\&\begin{aligned}\begin{aligned}&&4.&&\\&&5.&&\\&&6.&&\\&&7.&&\end{aligned}\boxed{\begin{aligned}&\lnot q&&&\text{antagande}\\&p\land\lnot q&&&\land\text i\ 3,4\\&r&&&\rarr_\text e\ 5,1\\&\bot&&&\lnot\text e\ 6,2\end{aligned}}\end{aligned}\\&\begin{aligned}&\enspace8.&&\lnot\lnot q&&&&&&&&&\lnot\text i\ 4\text-7\\&\enspace9.&&q&&&&&&&&&\lnot\lnot\text e\ 8\end{aligned}\end{matrix}\]

• Falsum: Om man får en motsägelse, kan man skriva "vad som helst" efteråt: \(\frac\bot{\phi}\tiny\bot e\)

  Exempel: \(\vdash p\rarr(\lnot p\rarr q)\)

  \[\begin{aligned}&\begin{aligned}&1.\\&2.\\&3.\\&4.\\&5.\end{aligned}&&\fbox{$\begin{aligned}&\begin{aligned}&p&&&&&&&\text{antagande}\end{aligned}\\&\fbox{$\begin{aligned}&\lnot p&&&&&\text{antagande}\\&\bot&&&&&\lnot\text e\ 1,2\\&q&&&&&\bot\text e\ 3\end{aligned}$}\\&\begin{aligned}&\lnot p\rarr q&&&&&&\rarr_\text i\ 2\text-4\end{aligned}\end{aligned}$}\\&6.&&\begin{aligned}p\rarr(\lnot p\rarr q)&&\rarr_\text i\ 1\text-5\end{aligned}\end{aligned}\]

  Vi antar först \(p\), och sedan \(\lnot p\). I den inre boxen uppstår nu en motsägelse (\(\bot\)), och vi kan därefter skriva \(q\). Vi får \(\lnot p\rarr q\), och den yttre boxen medför nu sammantaget \(p\rarr(q\rarr p)\).

• Disjunktions-introduktion: \(\frac{\phi}{\phi\lor\psi}\small\lor_{\text i_1}\) eller \(\frac{\psi}{\phi\lor\psi}\small\lor_{\text i_2}\)

• Disjunktions-eliminering: \(\frac{\enspace\begin{aligned}\\\\\small\phi\lor\psi\end{aligned}\quad\boxed{\begin{aligned}\small\phi\\\small\chi\end{aligned}}\quad\boxed{\begin{aligned}\small\psi\\\small\chi\end{aligned}}\enspace}{\small\chi}\small\lor_\text e\)

Exempel: \(p\lor q,\lnot p\vdash q\)

\[\begin{aligned}&\begin{aligned}&1.\\&2.\end{aligned}&\begin{aligned}&p\lor q&&&\text{premiss}\\&\lnot p&&&\text{premiss}\end{aligned}\\&\begin{aligned}&3.&\\&4.\\&5.\end{aligned}&\boxed{\begin{aligned}&p&&\text{antagande}\\&\bot&&\lnot\text e\ 3,2\\&q&&\bot\text e\ 4\end{aligned}}\\&\begin{aligned}&6.&\\&7.&\end{aligned}&\boxed{\begin{aligned}&q&&\text{antagande}\\&q&&\text{copy }6\end{aligned}}\\&8.&\begin{aligned}&q&&\lor_\text e\ 1,3\text-5,6\text-7\end{aligned}\end{aligned}\]

Sammanfattning, naturlig deduktion

Ett bevis till en sekvent är ett antal formler, där * varje formel antingen är en premiss i sekventen, ett tillfälligt antagande (öppnar en box), eller resultatet av någon regel (som tillämpas på tidigare nämnda formler i ej ännu stängda boxar). * alla antaganden är släppta (alla boxar stängda), och * sista formeln är sekventens slutsats.

Föreläsning 3 (2024-09-03)

Ny regel: falsum

"efter en motsägelse kan vi skriva vad som helst"

\[\frac{\bot}{\phi}\bot_\text e\]

Motivering 1: Antag att vi kan bevisa \(\phi\) och \(\lnot\phi\). Då måste \(\phi\lor\psi\) vara sann (\(\psi\) är vad som helst). Men eftersom \(\lnot\phi\) och \(\phi\lor\psi\) är sann så måste \(\psi\) vara sann!

Motivering 2: Det går att visa med sanningstabell att

\[\phi\rarr(\lnot\phi\rarr\psi)\]

alltid är sann. Antag att \(\phi\) och \(\lnot\phi\) är sann. Då är \(\lnot\phi\rarr\psi\) och \(psi\) är sann!

Predikatlogik

I Prolog har vi en prompter ?>. Vi ställer frågor till prolog.
?> 3+5 ger svaret 8.
Men mer avancerat använder vi variabler X, Y, Z...
Vi använder predikat father(X,Y) = X är far till Y.

Vi kan tala om för prolog att father(johan,elli) och father(johan,rej), father(johan,sigrid).

Vi kan fråga prolog ?>father(X,rej) och får svaret X=johan, eller ?>father(johan,Y) och får svaret Y=elli, Y=rej, Y=sigrid.

Predikat:
Enställiga predikat har formen p(x) där p är namnet på predikatet och x är en variabel.
Tvåställiga predikat har två variabler...

Det finns ett universum \(u\) som variablerna kan referera till (eller vara lika med). Då är p(x) en funktion \(u\rarr\{\text T,\text F\}\) (dvs. p(x) har värdet T [sant] eller F [falskt] för alla x)

Användning i matematiken:
\(u=\{\text{positiva heltal (>0)}\}\)
Vi kan definiera \(\text{Prim}(x):x\text{ är ett primtal}\).
Så \(\text{Prim}(5)=T;\text{Prim}(6)=F\)
Annat exempel: \(\text{delar}(x,y):x\text{ delar }y\).

Vi säga att t.ex. \(\text{Prim}(y)\rarr[\exists x\text{ delar}(x,y)\rarr x=1\lor x=y]\).
Vi ser också att \([\exists x\text{ delar}(x,y)\rarr x=1\lor x=y]\rarr\text{Prim}(y)\).

Nya saker i predikatlogik

1. Nya variabler \(x,y,\dots\) som refererar till objekt i \(u\).
2. Predikat som är funktioner \(u\rarr\{\text{T},\text{F}\}\)
3. Kvantifikatorerna \(\exists,\forall\)

Slut på föreläsning

Föreläsning 4 (prolog 1/4, 2024-09-09)

Relationer och predikat

Om \(p\) är en binär relation kan vi skriva \((a,b)\in p\). I predikatform skriver vi \(p(a,b)\).

Deklarativ programmering

Programmet är en beskrivning av problemdomänen. Delas in i funktionell programmering och logikprogrammering (t.ex. Prolog).

Logikprogrammering

Predikat beskriver relationer mellan objekt. Frågor (queries) besvaras med en sök-algoritm som kallas resolution.

Objekt i Prolog

• Individkonstanter: a, ´B´, foo, 4611
• Funktorer: Strukturnamn för noder i träd (samma syntax som för icke-numeriska individkonstanter).
• Logiska variabler: Börjar med versal eller _. Obs! Den anonyma variabeln ("void") skrivs _.

Exempel: foo(X,Y,Z) matchar termer med funktorn foo och där argumenten är termerna X,Y,Z. foo(_,_,_) matchar alla termer med funktorn foo och exakt 3 argument.

Termer

Givet en mängd variabler \(V\), konstanter \(C\) och funktionssymboler \(F\), är \(t\) en term omm antingen:

\(t\in V\), eller \(t\in C\), eller \(t=f(t_1,\dots,t_n)\) där \(f\in F\) och \(t_i\) är en term.

Unifiering

Två termer kan unifieras om det finns en substitution för variablerna sådan att termerna blir syntaktiskt identiska. T.ex. X och agnes unifieras av X=agnes. Termerna far(X, petter) och far(agnes, X) kan däremot inte unifieras.

Prolog-termer

I satsen a(b, c(X)). är a en 2-ställig predikatsymbol, c en 1-ställig funktionssymbol, b en konstant (dvs. en 0-ställig funktionssymbol) och X en variabel.

Obs! Funktionssymboler evalueras inte.

Fakta

Relationer som definieras explicit, varje tupel för sig, kallas för fakta.

Exempel:

far(anges, petter).
far(per, petter).
far(anton, per).

Vi kan nu ställa frågor, t.ex. ?- far(agnes, X) "vem är far till agnes?".

Prologsatser: regler

Relationer kan även definieras med regler, till exempel: farmor(X, Y) :- far(X, Z), mor(Z, Y). Sådana satser kallas för Horn-klausuler.

På detta sätt kan satsen far(anton, per). skrivas ekvivalent som far(X, Y) :- X=anton, Y=per..

Disjunktiva regler kan anges som separata klausuler, eller ekvivalent som foralder(X, Y) :- far(X, Y); mor(X, Y)..

Logisk vs. procedurell läsning av Prolog

• Logisk läsning: Som en predikatlogisk formel, deklarativt.
• Procedurell läsning: Proceduren som Prolog följer för att hitta ett bevis.
  • Prolog läser klausulerna uppifrån och ned, och kroppens literaler från vänster till höger.
  • Prolog försöker instansiera variablerna med termer: unifiering
  • Om detta misslyckas går Prolog till föregående literal inom klausulens kropp (om sådan finns), och annars till nästa klausul i programmet: backtracking.

Exempel: En fråga ?- p(Args). bevisas med resolution.

• Leta efter alla klausuler som definierar p.
• Välj den första, spara de kvarvarande som alternativ.
• Matcha argumenten Args med termerna i klausulens huvud, skapa nödvändiga variabelbindningar med unifiering.
• Om unifieringen misslyckas, prova nästa alternativa klausul.
• Bevisa annars målen i kroppen från vänster till höger. Om detta misslyckas, prova alternativ klausul.
• Om alla bevis är klara, presentera bindningarna. Annars är resultatet "no" eller "fail".

Aritmetik i Prolog

Obs! "=" beskriver unifierbarhet, och inte "samma värde".

Det speciella predikatet is utvärderar andra termen och unifierar med första: X is Expression.

Föreläsning 5 (prolog 2/4, 2024-09-12)

Föreläsning 6 (prolog 3/4, 2024-09-16)

TODO.

Föreläsning 7 (prolog 4/4, 2024-09-18)

TODO.

Föreläsning 8 (Satslogikens semantik, 2024-09-24)

Kort repetition

• Satslogik är ett formellt språk för att uttrycka påståenden med variabler (t.ex. \(p,q\)) och konnektiv (\(\land,\lor,\rarr,\lnot\)).
• Naturlig deduktion är ett system av regler för att generera nya påståenden (slutsatser) utifrån givna påståenden (premisser) med symbolisk manipulation. Genom att använda reglerna upprepade gånger kan vi konstruera bevis.

Man kan nu fråga sig: är alla regler korrekta och tillräckliga?

Satslogikens semantik

Semantik = innebörd, betydelse (jäm. syntax som enbart beskriver hur uttryck formas)
En formel kan vara sann eller falsk, beroende på ingående variabler.

En valuering är en tilldelning av sanningsvärden till varje variabel, t.ex. \(\{p:\text F,q:\text T,r:\text F\}\). Givet en sådan kan vi beräkna sanningsvärdet på hela formler med hjälp av sanningsvärdestabeller (en tabell per konnektiv). Efter att ha konstruerat sanningstabeller kan vi beräkna hela formelns sanningsvärde rekursivt, genom att ställa upp ett träd. Vi kan också synliggöra alla möjligheter i en tabell, genom att lista samtliga möjliga par \((p,q)\in\{(\text T,\text T),(\text T,\text F),(\text F,\text T),(\text F,\text F)\}\) i rader.

En formel kallas för en tautologi om den är sann oavsett värdena på de ingående variablerna. En sådan kan bevisas med naturlig deduktion utan premisser.

Modeller

En modell till en formel är en tolkning av symbolerna i formeln så att formeln blir sann eller falsk. Inom satslogik är en valuering en modell.

Logisk konsekvens

En formel \(\psi\) är en logisk konsekvens av \(\phi_1,\phi_2,\dots,\phi_n\) om \(\psi\) är sann i alla modeller (dvs. alla möjliga tilldelningar av variabler) i vilka \(\phi_1,\phi_2,\dots,\phi_n\) är sanna. Detta skrivs som:

\[\phi_1,\phi_2,\dots,\phi_n\vDash\psi\]

Obs! Detta innebär inte att \(\psi\) måste vara falskt i alla andra fall.

Logisk konsekvens i satslogik kan undersökas med en sanningsvärdestabell. T.ex. är det sant att \(p\land q\vDash p\lor q\) eftersom slutsatsen \(p\lor q\) är sann för alla valueringar av \(p,q\) sådana att \(p\land q\) (dvs. endast fallet \((p,q)=(\text T,\text T)\)).

Sundhet

Anta att vi kan bevisa \(\psi\) givet premisserna \(\phi_1,\dots,\phi_n\). Är det då också så att \(\psi\) är en logisk konsekvens av samma premisser? Denna (önskvärda) egenskap kallas för sundhet, och kan formuleras som:

\[\phi_1,\dots,\phi_n\vdash\psi\implies\phi_1,\dots,\phi_n\vDash\psi\]

Alla regler i naturlig deduktion är sunda.

En följd av satslogikens sundhet: Om \(\psi\) inte är en logisk konsekvens av \(\phi_1,\dots,\phi_n\), finns det heller inget bevis för \(\psi\) utifrån dessa premisser. Vi kan alltså använda metoden med sanningstabeller föra att visa att en sekvent inte är bevisbar.

Negationseliminering (naturlig deduktion)

En mängd formler är inkonsistent om man kan bevisa en motsägelse med dem (och \(\lnot_\text e\)).

Falsum

Om man kommit fram till en motsägelse, kan man skriva vad som helst efteråt. Falsumregeln är praktisk, men inte helt nödvändig.

Fullständighet

Om \(\psi\) är en logisk konsekvens av \(\phi_1,\dots,\phi_n\), kan vi då också bevisa \(\psi\) utifrån dessa premisser. Denna (önskvärda) egenskap kallas fullständighet, och naturlig deduktion är fullständig för satslogik. Om vi inte kan bevisa tautologier, är ett system inte fullständigt.

Bevis av att naturlig deduktion är fullständigt

Vi kan börja med att konstatera att de enklaste semantiska reglerna kan bevisas med naturlig deduktion. Vi kan t.ex. bevisa \(A,B\vdash A\rarr B\);\(A,\lnot B\vdash\lnot(A\rarr B)\); \(\lnot A,B\vdash A\rarr B\) och \(\lnot A,\lnot B\vdash A\rarr B\). Ovanstående formler är avkodade ur en sanningsvärdestabell.

Detta kan generaliseras. Antag t.ex. att \(\phi\) är en formel som innehåller \(p,q\). Antag t.ex. att \(\phi\) är F om \(\{p:\text T,q:\text F\}\). Då kan vi bevisa \(p,\lnot q\vdash\lnot\phi\).

Antag att \(\psi\) är en tautologi. Vi vill då visa \(\vdash\psi\). Antag att \(\phi\) bara innehåller \(p,q\). Ett semantiskt bevis för att \(\psi\) är en tautologi:

\(p\)	\(q\)	\(\psi\)
T	T	T
T	F	T
F	T	T
F	F	T

Vi kan koda av dessa och alltså visa att \(p,q\vdash\psi\); \(p,\lnot q\vdash\psi\); \(\lnot p,q\vdash\psi\) och \(\lnot p,\lnot q\vdash\psi\). Vi kan då också visa: \(\vdash p\land q\rarr\psi\), \(\vdash p\land\lnot q\rarr\psi\), \(\vdash\lnot p\land q\rarr\psi\) och \(\vdash\lnot p\land\lnot q\rarr\psi\).

Generellt gäller att om \(\vdash\phi_1\rarr\psi\) och \(\vdash\phi_2\rarr\psi\) så gäller \(\vdash\phi_1\lor\phi_2\rarr\psi\). Detta kan bevisas med ellereliminering.

Låt nu \(A=(p\land q)\lor(\lnot p\land q)\lor(p\land\lnot q)\lor(\lnot p\land\lnot q)\). Det går då att visa \(\vdash A\rarr\psi\). Det går även att visa \(\vdash F\) (lite jobbigt), vilket slutligen gör det möjligt att bevisa \(\vdash\psi\).

Exempel

Ett bevissystem har en enda bevisregel: \(\frac{}\phi\)
Systemet är fullständigt (går att bevisa allt som är sant [men även det som inte är sant...]) men inte sunt (går att bevisa falska påståenden).

Validitet och satisfierbarhet

En formel är valid om den är sann i alla modeller. T.ex. \(p\lor\lnot p\).
En formel är satisfierbar om den är sann i någon modell. T.ex. \(p\).
En formel är osatisfierbar om den är falsk i alla modeller. T.ex. \(p\land\lnot p\).
Om \(\phi\) är valid så är \(\lnot\phi\) osatisfierbar. Om \(\psi\) varken är valid eller osatisfierbar gäller samma sak även för \(\lnot\psi\).

Föreläsning 9

Repetition om predikatlogik

Predikatlogik utökar det satslogiska språket med variabler, konstanter, funktionssymboler, relationssymboler (t.ex. \(\gt,=\)) och kvantifierare (t.ex. \(\forall,\exists\)).

T.ex. \(\forall x\left(\text{Primtal}(x)\land x\gt2\rarr\text{Udda}(x)\right)\)

Naturlig deduktion med predikatlogik

Predikatlogikens semantik är komplicerad. Därför börjar vi med att använda naturlig deduktion.

Påståendet \(\forall x(P(x)\lor\lnot P(x))\) är sant i alla tolkningar. Vi bör alltså kunna visa \(\vdash\forall x(P(x)\lor\lnot P(x))\).

Problemet med "universum"

Vad kan \(x\) vara om vi skriver \(\forall x\)? Vi föreställer oss ett universum \(u\) som innehåller alla tänkbara \(x\).

Vanligt specialfall: \(\forall x\forall y(x+y=y+x)\)
Här kan vi tänka oss att t.ex. \(u=\mathbb R\). Detta måste då anges!
Om vi t.ex. skulle tänka oss att \(u=\text{"alla textsträngar"}\), och att operatorn \(+\) innebär konkatenering, stämmer inte påståendet.

Ett problem till: T.ex. påståendet "alla hundar är farliga" kan formuleras på flera sätt: (vi antar H: hund, F: farlig)

• Bra lösning: \(\phi=\forall x(H(x)\rarr F(x))\) med \(u=\text{"allt"}\).
• Annan lösning: Samma formel (\(\phi\)), men med \(u=\text{"alla djur"}\).
• En tredje lösning: \(u=\text{"hundar"}\). Då räcker \(\phi=\forall xF(x)\).
• Med ett mindre universum går påståendet inte att formulera.

Generellt sett använder vi ett universum som innehåller allt. Obs! Universum får aldrig vara tomt.

Bevisregler

Som bevisregler gäller alla regler från satslogiken, samt introduktions-/elimineringsregler för likhet \(=\), allkvantifiering \(\forall\) och existenskvantifiering \(\exists\).

• Alla-eliminering: \(\frac{\forall x\ \phi(x)}{\phi(t/x)}\forall x\ _\text{e}\)
• Finns-introduktion: \(\frac{\phi(t/x)}{\exists x\ \phi(x)}\exists_\text{i}\)
• Alla-introduktion: \(\frac{\boxed{\begin{matrix}x_0\\\vdots\\\phi(x_0/x)\end{matrix}}}{\forall x\ \phi(x)}\forall x_\text i\)
  • Om vi kan komma fram till \(\phi(x_0)\) med ett okänt objekt \(x_0\), kan vi göra det för alla möjliga \(x_0\).
  • Obs! Första raden i boxen (\(x_0\)) numreras inte.
• Finns-eliminering: \(\frac{\exists x\ \phi(x)\ \ \ \boxed{\begin{matrix}x_0,\ \phi(x_0/x)\\\vdots\\\chi\end{matrix}}}{\chi}\exists x\ _\text e\)
  • Dvs. inför ny \(x_0\) och antag, i samma box, \(\phi(x_0/x)\). Härled \(\chi\) och stäng boxen.

Fler regler (=)

"=" är en speciell relationssymbol som vi antar alltid finns i logiken. \(x=y\) betecknar att \(x\) och \(y\) är samma objekt (extensionell likhet): \(2+2=4\). Notera att Prolog har ett annat likhetsbegrepp (syntaktisk likhet).

• Likhetsintroduktion: \(\frac{}{t=t}=_\text i\)
• Likhetselimination: \(\frac{t_1=t_2,\ \phi(t_1/x)}{\phi(t_2/x)}=_\text e\)
  • "Byt några förekomster av \(t_1\) mot \(t_2\)."

Exempel

... (se 43:30 och framåt i inspelad föreläsning)

Föreläsning 10

Predikatlogikens semantik

Teorin för vad predikatlogiska formler betyder. Predikatlogiska formler kan hanteras på två sätt:

• Syntaktiskt - hur de är uppbyggda, avgöra om en formel är korrekt uppbyggd eller inte.
• Härledning (ND) - komma fram till bevisbarhet, men för att avgöra om en formel är sann/valid måste man använda modeller (ingår i predikatlogikens semantik)

Vi kommer att tala om modeller till formler. Vissa av dessa kallas för abstrakta modeller och andra för naturliga modeller.

Matematisk repetition:
Kryssprodukt: \(\{1,2\}\times \{3,4\}=\{(1,3),(1,4),(2,3),(2,4)\}\)

Binär relation: En binär relation över \(A\) är en delmängd av \(A\times A\). T.ex. "mindre än" är en binär relation över \(N\): \("<"=\{(0,1),(0,2),(1,2),(0,3),(1,3),\dots\}\) Allmänt kan n-ställiga relationer definieras, där varje komponent i mängdens n-tuplar är hämtad ur samma mängd.

Funktion: Kan ses som en speciell sorts relation. Om \(F\) är en binär relation över \(A\), där det för varje \(a\in A\) finns max ett \(b\in A\) s.a. \((a,b)\in F\), är \(F\) en funktion.

Unära relationer: Kallas ibland för egenskaper. Beskriver vilka element i mängden \(A\) som har en viss egenskap.

För satslogik kunde vi definiera en semantik med hjälp av sanningsvärdestabeller (föreläsning 8) - naturlig deduktion för satslogik är sund och fullständig med denna semantik.

Vi vill nu definiera en semantik (modellteori) för predikatlogiken.

Exempel: Formeln \(\forall x\forall y(x+y=y+x)\) är sann om vi tänker oss "addition över heltal", men inte sann om vi tänker oss "konkatenering av strängar".

En modell \(\mathcal M\) till en predikatlogisk formel \(\phi\) specificerar:

• ett universum \(A\)
• för varje konstant i \(\phi\): ett element i \(A\)
• för varje funktionssymbol \(f\) i \(\phi\): en funktion \(f^{\mathcal M}:A^n\rarr A\)
• för varje predikatsymbol \(P\) (t.ex. <) i \(\phi\): en n-ställig relation \({\mathrel P}^{\mathcal M}\in A^n\)

Om \(\phi\) är sann i modellen \(M\), skriver vi att \(M\vDash\phi\).

Rekursiv evaluering

För att evaluera om en formel är sann eller ej i en viss modell kan man rekursivt evaluera alla dess delformler. T.ex. för att avgöra om \(M\vDash\phi_1\land\phi_2\) ska vi avgöra om \(M\vDash\phi_1\) och \(M\vDash\phi_2\).

Jämfört med satslogik: I satslogiken är en modell en valuering, dvs. en rad i sanningstabellen.
Om det finns n variabler i den satslogiska formeln \(\phi\), finns det \(2^n\) rader i sanningstabellen för \(\phi\).
I predikatlogiken finns däremot oändligt många modeller till varje formel.
För att visa att en formel är valid (dvs. sann i alla modeller), måste man konstruera ett bevis.

Slutna och öppnar formler

En sluten formel (= en sats/sentence) är en formel utan fria variabler, t.ex. \(\forall x(U(x))\). Givet en modell \(M\) är en sats sann eller falsk.

En öppen formel innehåller fria variabler, t.ex. \(U(x)\). För att kunna veta om \(U(x)\) är sann eller falsk i \(M\) måste vi veta vad \(x\) är bundet till. Därför införs begreppet omgivning (definition 2.17), vilket är en funktion från variabler till värden: t.ex. \(x\rarr a\) (inte svårt men tekniskt).

I denna kurs kommer vi att fokusera på slutna formler.

Logisk konsekvens

Formeln \(\psi\) är en logisk konsekvens av \(\phi_1,\phi_2,\dots,\phi_n\) om \(\psi\) är sann i alla modeller i vilka \(\phi_1,\phi_2,\dots,\phi_n\) är sanna.

Detta skrivs \(\phi_1,\phi_2,\dots,\phi_n\vDash\psi\). Samtliga formler antas vara slutna.

Sundhet och fullständighet

Precis som för satslogik kan man visa att naturlig deduktion är ett sunt och fullständigt bevissystem för predikatlogik, dvs. att

\[\phi_1,\phi_2,\dots,\phi_n\vdash\psi\iff\phi_1,\phi_2,\dots,\phi_n\vDash\psi\]

Att bevisa detta är svårt och ingår ej i kursen.

Följder av sundhet

Predikatlogikens sundhet har några intressanta följder:

• Om \(\psi\) inte är en logisk konsekvens av \(\phi_1,\phi_2,\dots,\phi_n\) så finns det heller inget bevis för \(\psi\) utifrån premisserna \(\phi_1,\phi_2,\dots,\phi_n\).
  • Dvs. om vi kan hitta ett enda sätt att tolka symbolerna i formlerna så att \(\phi_1,\phi_2,\dots,\phi_n\) blir sanna, men \(\psi\) falsk, så finns det inget bevis för \(\psi\) utifrån dessa premisser.
  • Vi behöver bara hitta en sådan modell för att visa att bevis saknas.
  • En formel är falsifierbar om det finns någon tolkning där den är falsk.

Några samband: \(\text{Val}(\psi)\iff\vdash\psi\iff\vDash\psi\iff\lnot\text{Fal}(\psi)\iff\lnot\text{Sat}(\lnot\psi)\)

\(\vdash\psi\implies\text{Sat}(\psi)\)

Exempel: Är \(\exists x\exists y(x\neq y\land R(y,f(y)))\) satisfierbar?
Svar: Ja, eftersom formeln är sann för modellen
\(\begin{cases}u=\{\text{"människor"}\}\\f(y)=\text{Mamma till }y\\R(x,y)=y\text{ är äldre än }x\end{cases}\)
Detta är en "naturlig modell" - bygger på en naturlig situation.
Det går även att skapa abstrakta modeller, t.ex.
\(\begin{cases}u=\{c_1,c_2\},c_1\neq c_2,f(c_1)=c_1,f(c_2)=c_2\\R(c_1,c_1)=R(c_1,c_2)=R(c_2,c_1)=R(c_2,c_2)=\text T\end{cases}\)
Denna modell satisfierar också formeln.

Validitet och satisfierbarhet (repetition)

En formel är valid om den är sann i alla modeller.
En formel är satisfierbar om den är sann i någon modell.
En formel är osatisfierbar om den är falsk i alla modeller.

Oavgörbarhet - lite teori

Vi har en predikatlogisk formel \(\phi\) och vill avgöra om den går att bevisa. Om vi inte lyckas hitta ett bevis, letar vi istället efter ett motexempel. Om vi inte heller hittar ett motexempel, måste formeln alltså vara antingen valid eller falsifierbar. Det finns ingen process för att ta reda på vilket av dem.

Detta hänger samman med predikatlogikens oavgörbarhet. Detta innebär att det inte finns något datorprogram som alltid terminerar och svarar "ja" exakt när \(\phi\) är valid, och "nej" annars.

Man kan visa detta genom att, givet ett program P, generera en formel \(\phi\) som är valid omm P terminerar. Eftersom termineringsproblemet är oavgörbart så måste då även validitetsproblemet vara oavgörbart.

Ett oavgörbart problem

Betrakta alla möjliga Java-program \(J_1,J_2,\dots\) som tar ett heltal som indata och returnerar ett heltal (eller aldrig terminerar). Definiera nu

\[D(n)=\begin{cases}1&\text{om }J_n(n)\text{ inte terminerar}\\J_n(n)+1&\text{annars}\end{cases}\]

Antag att \(D\) kan implementeras (dvs. \(D=J_k\) för något \(k\)). Men då kommer \(D(k)\) antingen både returnera \(1\), och inte terminera, eller returnera både \(x\) och \(x+1\). Motsägelse - det finns alltså inget Java-program som beräknar \(D\).

Det underliggande problemet är att det inte går att avgöra huruvida \(J_n(n)\) terminerar eller ej.

Termineringsproblemet

Resonemanget ovan visar att termineringsproblemet är oavgörbart. Mängden \(T\) är terminerande Java-program är rekursivt uppräkningsbar, men inte rekursiv.

Termineringsproblemet innebär inte att vi aldrig kan säga om ett program terminerar. Det innebär däremot att vi inte kan hitta en systematisk metod som alltid avgör detta för ett givet program och indata.

En mängd är rekursivt uppräkningsbar om man kan skriva ett datorprogram som, givet ett objekt \(x\), ger resultatet "ja" precis när \(x\in M\). Om \(x\notin M\) kan programmet svara "nej" eller inte terminera alls.

Mängden \(\{\text{"alla valida predikatlogiska formler"}\}\) är rekursivt uppräkningsbar, eftersom vi kan konstruera ett program som, givet en predikatlogisk formel, testar alla möjliga bevis i naturlig deduktion. Om formeln är valid, kommer ett bevis att hittas förr eller senare. Det saknas däremot en metod för att göra motsatsen.

En mängd är rekursiv om man kan skriva ett datorprogram som alltid terminerar och alltid svarar rätt på huruvida \(x\in M\) eller ej.

Föreläsning 11 (29 oktober)

Axiomatisering

Definition: En teori T består av en mängd formler \(T=\{\phi_1,\phi_2,\dots\}\) (vanligen oändlig). T har ofta en normal modell/tolkning. Ibland kan vi hitta vissa formler i T som vi kallar axiom \(A_1,A_2,\dots,A_n\) som fungerar så att \(\phi\in T\iff A_1,A_2,\dots,A_n\vdash\phi\).

Viktigast idag: Peanos axiomatisering av heltalsaritmetik

Vi vill kunna bevisa saker som \(2+2=4\), \(\forall x\forall y(xy=yx)\), ...

Vi använder ett begränsat antal grundsymboler: \(0\), \(+,\cdot\) och \(S(x)\)

Utgående från Peanos axiom går det att visa alla egenskaper hos heltalsaritmetik.

Peanos axiom, del 1:
(1) \(\lnot\exists x(S(x)=0)\), dvs. 0 är det första talet
(2) \(S(x)=S(y)\rarr x=y\)
(3) \(x+0=x\)
(4) \(x+S(y)=S(x+y)\)

Kommentar: Egentligen skulle vi skriva \(\forall x\) framför axiomen. Men vi struntar i det.

Definition: Vi definierar 1 som S(0), 2 som S(S(0)), osv.

Bevis av \(2+2=4\):
Vi vill egentligen bevisa \(S(S(0))+S(S(0))=S(S(S(S(0))))\).
Ax. #4: \(S(S(S(0))+S(0))\)
Ax. #4: \(S(S(S(S(0))+0))\)
Ax. #3: \(S(S(S(S(0))))\)

Peanos axiom, del 2:
(5) \(x\cdot S(0)=x\)
(6) \(x\cdot S(y)=x\cdot y+x\)
(7) Induktion, det svåraste axiomet: Låt \(P()\) vara ett predikat definierat med en predikatlogisk formel. Då gäller

\[P(0)\land\forall x(P(x)\rarr P(S(x)))\rarr\forall x P(x)\]

Exempel: Bevisa \(\forall x\forall y\forall z((x+y)+z=x+(y+z))\). Vi använder induktion över z. Sätt \(P(k)=(x+y)+k=x+(y+k)\).

1: Kolla \(P(0):(x+y)+0=x+(y+0)\) Är det sant?
Vi ser att \((x+y)+0=x+y=x+(y+0)\) (enl. Ax. #3)

2: Nu antar vi att P(k) är sant, dvs. \((x+y)+k=x+(y+k)\).

3: Vi försöker sedan visa att \(P(S(k))\) är sant, dvs. \((x+y)+S(k)=x+(y+S(k))\).

Det visar sig att det också är lämpligt att visa \(P(1)\), dvs.

\[(x+y)+S(0)=x+(y+S(0))\]

Bevis: \((x+y)+S(0)\)
Ax. #4: \(=S((x+y)+0)\)
Ax. #3: \(=S(x+y)\)
Ax. #4: \(=x+S(y)\)
Ax. #3: \(=x+S(y+0)\)
Ax. #4: \(=x+(y+S(0))\)

4: Vi kan nu bevisa målet: \((x+y)+S(k)\)

Ax. #3: \(=(x+y)+S(k+0)\)
Ax. #4: \(=(x+y)+(k+S(0))\)
P(1): \(=((x+y)+k)+S(0)\)
Ind. ant.: \(=(x+(y+k))+S(0)\)
P(1): \(=x+((y+k)+S(0))\)
P(1): \(=x+(y+(k+S(0)))\)
Ax. #4: \(=x+(y+S(k+0))\)
Ax. #3: \(=x+(y+S(k))\)

Ax 7 ger nu att \(P(z)\) gäller för alla \(z\), dvs. att

\[\forall x\forall y\forall z((x+y)+z=x+(y+z))\]

Exempel: Vi kan bevisa att \(0\cdot0=0\) (!).
Det följer inte omedelbart från axiomen.
Vi skriver \(0\cdot S(0)\)
Ax. #6: \(=0\cdot0+0\)
Ax. #3: \(=0\cdot0\)
Så vi har bevisat att \(0\cdot S(0)=0\cdot0\).
Men å andra sidan gäller att \(0\cdot S(0)=0\) enligt Ax. #5.
Dvs. \(0\cdot0=0\).

Vad är egentligen Peano-aritmetik?

• Ett språk som består av symbolerna 0, +, *, S( ).
• En teori som fås med Peanos axiom.
• Ett sätt att syntaktiskt beskriva "vanlig" aritmetik.
• Tänkt att ha "vanlig" matematik som enda modell.

Men! Det visar sig att Peano-aritmetik inte riktigt klarar allt detta!

Gödels ofullständighetssats: I varje teori som är effektivt axiomatiserbar finns det en formel \(\phi\) sådan att varken \(\phi\) eller \(\lnot\phi\) går att bevisa.

Exempel: Annan axiomatisering: en "släktinglogik".
Vi tänker oss att \(u=\{\text{människor}\}\).
Vi har predikat \(\text{parent}(x,y)\), \(\text{child}(x,y)\), \(\text{ancestor}(x,y)\) och \(\text{descendent}(x,y)\).
Om vi vill axiomatisera logiken måste vi ställa krav på predikaten (vilka egenskaper predikaten skall ha). Vad skulle det kunna vara?
T.ex. \(\forall x\forall y(\text{parent}(x,y)\rarr x\neq y)\) osv.

Föreläsning 12 (31/10-2024)

Matematisk induktion (heltal)

\(P(x)\) är ett påstående om ett naturligt tal \(x\).
Vi vill visa \(\forall xP(x)\)
Induktion: Antag att vi vet att \(P(0)\) är sant och att \(\forall x(P(x)\rarr P(x+1))\) är sant. Då gäller \(\forall xP(x)\)

Varför fungerar induktion?

Antag att (1) och (2) gäller, men \(\forall xP(x)\) inte är sant. Då finns ett minsta tal \(a\) så att \(P(a)\) är falskt. Då är \(P(a-1)\) sant. Men \(P(a-1)\rarr P(a)\) så \(P(a)\) är sant. Motsägelse!

Typiskt exempel på induktion

Visa att \(\sum_{i=1}^xi=\frac{x(x+1)}2\)
Induktion: Sätt \(P(x):\sum_{i=0}^xi=\frac{x(x+1)}2\)
Vi kan skriva detta som \(\text{VL}(x)=\text{HL}(x)\).
Vi kollar nu \(P(0)\), vilket visar sig vara sant då \(\text{VL}(0)=\text{HL}(0)\).

Antag att \(P(x)\) är sant, dvs. \(\sum_{i=0}^xi=\frac{x(x+1)}2\)
Då gäller \(\text{VL}(x+1)=\sum_{i=0}^{x+1}i=\sum_{i=0}^xi+(x+1)=\text{VL}(x)+(x+1)\)

Kan det vara så att \(\text{HL}(x+1)=\text{HL}(x)+(x+1)\)?

\(\text{HL}(x+1)=\frac{(x+1)(x+2)}2\text{ och }\text{HL}(x+1)-\text{HL}(x)=\dots=x+1\)

\(\therefore P(x+1)\) är sant.

Induktionsprincipen ger slutligen, eftersom \(P(0)\) och \(\forall x(P(x)\rarr P(x+1))\), att \(\forall xP(x)\).

Rekursiv framställning av problemet

Definiera en funktion \(f(n)\) rekursivt genom \(\begin{cases}f(0)=0\\f(n+1)=f(n)+(n+1)&n\geq0\end{cases}\).
Vi ser att \(f(n)=\sum_{i=0}^ni\).
Satsen vi hade tidigare lyder då \(f(n)=\frac{n(n+1)}2\).

Induktionsbeviset kan nu uttryckas som: \(Q(n):f(n)=\frac{n(n+1)}2\)

1. \(Q(0):f(0)=0\) Ok!
   
2. Antag \(Q(n)\) sant.
   
3. Testa \(Q(n+1):f(n+1)=f(n)+(n+1)\)

Strukturell induktion

Induktion kan användas för andra objekt än heltal.
Vi kommer att tillämpa den på strukturer. Speciellt tittar vi på rekursiva strukturer.

Rekursiv struktur (informell definition):

1. S är ett objekt som innehåller delar.
2. S kan byggas upp av delarna.
3. Delarna är också strukturer av samma slag som S.
4. Delarna som bygger upp S kan ordnas i en partialordning.

Exempel: De naturliga talen. Talet 5 har t.ex. delarna 0, 1, 2, 3 och 4. Delarna kan bygga upp 5 (i detta fall på flera olika sätt, t.ex. 5=2+3), är av samma slag som 5 och kan partialordnas: \(0\leq1\leq2\leq3\leq4\).

Listor

[l,o,g,i,k] = l|[o,g,i,k]
                -- del --

Satslogiska formler: \(A=B_1\rarr B_2\) där \(B_1,B_2\) är delar av \(A\).

Binära träd

...

Idén med rekursiva strukturer

1. Vi kan definiera funktioner på strukturer rekursivt som funktioner på delarna.
2. Vi kan bevisa påståenden om strukturen genom att göra induktion över delarna (strukturell induktion). Obs! För att detta ska fungera måste vi ha en partialordning på delarna och vissa delar angivna som basfall. Det går till så här: del₁<del₂⟺del₁ är en del av del₂.
   Del \(i\) är ett basfall \(\iff\) del \(i\) innehåller inga delar.

Heltalslistor

Informellt skriver vi t.ex. L = [2, 1, 3]. Formellt använder vi symbolen cons: L = cons(2, cons(1, cons(3, []))).

cons(X, L) är listan L med talet x placerat först.

En heltalslista kan definieras med s.k. BN-notation: <IntegerList>::=[]|cons(<Integer><IntegerList> I denna definition är [] basfallet.

Funktioner på listor

Längd

Vi kan definiera len(L) = antalet element i L rekursivt:

len([])         = 0
len(cons(A, L)) = 1 + len(L)

Exempel:

len([7, 3]) = len(cons(7, cons(3, [])))
= 1 + len(cons(3, [])) = 1 + 1 + len([]) = 1 + 1 + 0 = 2

Append

app([], L) = L
app(cons(A, L1), L2) = cons(A, app(L1, L2))

Exempel:

app([1, 2], [3, 4]) = cons(1, app([2], [3, 4]))
= cons(1, cons(2, app([], [3, 4])))
= cons(1, cons(2, [3, 4])))
= [1, 2, 3, 4]

Exempel på strukturell induktion

Visa att len(app(A, B)) = len(A) + len(B) för alla listor A och B.

Basfall []: len(app([], B)) = len(B) = 0 + len(B) = len([]) + len(B)

Induktionsantagande: Antag len(app(A, B)) = len(A) + len(B)

Induktionssteg cons(X, A): len(app(cons(X, A), B) = len(cons(X, app(A, B))) = 1 + len(app(A, B)) = 1 + len(A) + len(B) = len(cons(X, A)) + len(B)

Binära träd

Binära träd definieras i BN-notation: <Btree> ::= leaf | t(<Btree>, <Btree>)

Exempel: t(leaf, t(leaf, leaf))

Funktioner på (binära) träd

Höjden på ett träd:

height(leaf) = 0
height(t(A, B)) = 1 + max(height(A), height(B))

Föreläsning 13 (4/11-2024)

"Vanlig" induktion

Exempel: Visa att \(n^5-n\) är delbart med 5 för alla heltal \(n\geq0\).

Sätt \(P(n):"n^5-n\text{ är delbart med 5}"\).
\(P(0):0^5-0=0\) vilket är delbart med 5. \(\therefore P(0)\) sant.
Antag att \(P(k)\) är sant: \(k^5-k\) är delbart med 5.
Vi vill visa att \(P(k+1)\) är sant:
\((k+1)^5-(k+1)=k^5+5k^4+10k^3+10k^2+5k+1-(k+1)=k^5-k+5(k^4+2k^3+2k^2+k)\)
Eftersom \(k^5-k\) är delbart med 5, dvs. \(k^5-k=5c\) för något \(c\), kan vi skriva: \(=5(c+k^4+2k^3+2k^2+k)\), dvs. \(P(k+1)\) sant för alla \(n\geq0\).

Stark induktion

Principen för stark induktion:

1. Bevisa basfallet \(P(0)\).
2. Induktionsantagande: \(P(k)\) för alla \(0\leq k\leq n\).
3. Induktionssteg: Visa \(P(n)\) med hjälp av antagandet.
4. Slutsats: \(\forall xP(x)\).

Flera basfall: För såväl vanlig som stark induktion kan ibland flera basfall krävas.

Stark induktion kan översättas till vanlig induktion:

Låt \(Q(n)\) beteckna \(P(0)\land\dots\land P(n)\). Då är \(Q(0)=P(0)\), dvs. basfallet är likadant för \(Q\) och \(P\). Induktionssteget blir

\[Q(n)\rarr P(n+1)\]

vilket är ekvivalent med \(Q(n)\rarr Q(n+1)\).

Strukturell induktion

Exempel: Bevisa att n(T) ≤ 2ʰᵉⁱᵍʰᵗ⁽ᵀ⁾⁺¹-1 för alla binära träd T.

n(leaf) = 1
n(t(A, B)) = 1 + n(A) + n(B)

• Basfall: n(leaf) = 1 ≤ 2¹-1 = 2ʰᵉⁱᵍʰᵗ⁽ˡᵉᵃᶠ⁾⁺¹-1
• Antagande: Antag n(A) ≤ 2ʰᵉⁱᵍʰᵗ⁽ᴬ⁾⁺¹-1 och n(B) ≤ 2ʰᵉⁱᵍʰᵗ⁽ᴮ⁾⁺¹-1
• Induktionssteg: TODO...TODO...TODO...etc!!!............... ᴬ𝇄 ᵍ

Vilken ordning gör vi induktionen över?
Träden är ordnade med delträdsrelationen: T1 ≤ T2 om antingen T2 = t(T1, X) eller T2 = t(X, T1) för något X, eller antingen T2 = t(U, X) eller T2 = t(X, U) så att T1 ≤ U.

Föreläsning 14 (11/11-2024)

Möjliga utvidgningar av satslogik

• Vi kan utöka sanningsvärdena med ett tredje värde "?".
• Modallogik: I vanlig satslogik är alla sanningar "lika sanna". T.ex. kan "det regnar" ses som en "tillfällig sanning", medan "1+3=4" är en nödvändig sanning.
  • En nödvändig sanning betecknas \(\square{}q\).
  • Om \(p\) är en icke-nödvändig sanning, är det alltså möjligt att \(p\) är falskt. Detta skrivs i modallogik som \(◇\lnot p\).
  • Symbolen \(◇\) ("möjligt") kan definieras som \(◇\phi\equiv\lnot\square{}\lnot\phi\), där HL betyder att det inte är nödvändigt (\(\lnot\square{}\)) att \(\lnot\phi\).

Operatorn \(◇\) bör rimligen uppfylla vissa regler:

• \(◇(p\rarr q)\implies◇p\rarr◇q\) verkar rimligt
• \(\square{}p\rarr p\) verkar rimligt

Kripkes semantik för modallogik: Antar att det finns flera världar.
Ur denna syn betyder \(\square{}\phi\) att "\(\phi\) är sann i vår värld och alla världar vi kan föreställa oss", medan \(◇\phi\) betyder att "vi kan föreställa oss en värld där \(\phi\) är sann".

Detta ger upphov till olika former av modallogik:

• S4: \(\square{}\phi\rarr\phi,\square{}\phi\rarr\square{}\square{}\phi\)
• S5: \(\square{}\phi\rarr\phi,\square{}\phi\rarr\square{}\square{}\phi,◇\phi\rarr\square{}◇\phi\)

Introduktion till temporallogik

Vi vill analysera s.k. rigorös systemutveckling, dvs. skapa bevisbart korrekta system.

Funktionsbeteende: Bevisa att, givet korrekt indata, ges korrekt utdata. T.ex. beräkningsprogram.
Interaktionsbeteende: Bevisa att önskvärda egenskaper gäller i alla möjliga interaktionssekvenser. T.ex. servrar.

Modellbaserad systemutveckling

• Väsentliga beteendeegenskaper hos ett system beskrivs med en specifikation (kan vara logiska formler).
• En abstrakt modell av beteendet kan skapas med t.ex. automater.
• Man kan då verifiera att modellen har specificerade egenskaper med t.ex. en modellprovare. Modellen kan slutligen ligga till grund för implementationen.

Ett enkelt system med temporallogik

Snöar: Har olika sanningsvärde beroende på dag.

\[\begin{smallmatrix}&\circ&\rarr&\circ&\rarr&\circ&\rarr&\circ&\rarr&\cdots\\\text{nov}&16&&17&&18&&19\end{smallmatrix}\]

Låt säga att formeln \(F\text{ snöar}\) betyder att det snöar idag eller någon kommande dag, och att \(G\text{ snöar}\) betyder att det snöar idag och alla kommande dagar. Om det snöar idag, är alltså \(F\) sann, medan \(G\) är falsk.

Med dessa modaliteter får vi följande ekvivalenser:

\[\lnot G\phi\equiv F\lnot\phi\\\lnot F\phi\equiv G\lnot\phi\]

\(F\phi\) och \(G\phi\) är definierade alla dagar, men kan variera. Exempel: Om \(\phi\) är sant på, och endast på, första dagen, är \(F\phi\) sant på denna dag, men inga senare dagar.

Exempel: Presidentvalet 2020

Med ett mer icke-deterministisk syn kan man tänka sig två möjliga utvecklingar:

\[\begin{smallmatrix}&&&&\lnot T&&\lnot T&\\&&&&\bigcirc&\rarr&\bigcirc&\rarr\\\lnot T&&\lnot T&↗&^\text{9 nov}&&^\text{10 nov}&\\\bigcirc&\rarr&\bigcirc\\^\text{7 nov}&&^\text{8 nov}&↘&T&&T\\&&&&\bigcirc&\rarr&\bigcirc&\rarr\\&&&&^\text{9 nov}&&^\text{10 nov}\end{smallmatrix}\]

där \(T:\) Trump vald.

Vi tänker oss fyra temporallogiska formler:

• \(\text{AG}\ \phi:\) Oavsett utveckling, gäller \(\phi\) alltid.
• \(\text{EG}\ \phi:\) Det finns någon utveckling där \(\phi\) alltid gäller.
• \(\text{AF}\ \phi:\) Oavsett utveckling, kommer \(\phi\) någon gång att gälla.
• \(\text{EF}\ \phi:\) Det finns minst en möjlig utveckling då \(\phi\) någon gång gäller.

\(\text{AG, EG, AF, EF}\) kallas för temporala kvantifierare och uttrycker sanning över sekvenser av valueringar (utvecklingar).

Definition av begreppet system

Ett system betecknas \(M\) (modell). 3 komponenter:

• En lista med tillstånd \(s_1,s_2,\dots\). Dessa motsvaras av noder i en tillståndsgraf.
• En övergångsrelation \("\rarr"\) som anger möjliga övergångar mellan tillstånd.
• En lista med satsvariabler \(p_1,p_2,\dots\).
• En funktion \(L:\text{tillstånd }s_i\rarr\text{sanna satsvariabler}\)
  • \(L\) kallas för en sanningstilldelning

Computational Tree Logic (CTL)

CTL = satslogik + temporala kvantifierare

• Vägkvantifierare: \(\text A\) (över alla vägar), \(\text E\) (över någon väg).
• Tillståndskvantifierare: \(\text X\) (för nästa tillstånd på vägen), \(\text G\) (för alla tillstånd på vägen), \(\text F\) (för något tillstånd på vägen).

I denna kurs

Atomerna i en modell är de satslogiska variabler som finns i specifikationen.
En modell \(M\) består av en mängd \(S\) av tillstånd, en övergångsrelation och en sanningstilldelning.

Formell semantik

\[\small{\begin{align}&\mathcal M,s\vDash p&\enspace&\text{om }p\in L(s)\\&\mathcal M,s\vDash\lnot\phi&&\text{om \underline{inte} }\mathcal M,s\vDash\phi\\&\mathcal M,s\vDash\phi\land\psi&&\text{om}\ \mathcal M,s\vDash\phi\text{ och }\mathcal M,s\vDash\psi\end{align}}\]

Tolkning: T.ex. (1) betyder att "modellen \(\mathcal M\) i tillståndet \(s\) har konsekvens \(p\) om \(p\in L(s)\).

\[\scriptsize{\begin{align}&\mathcal M,s\vDash\text{AX}\ \phi&\enspace&\text{om }\mathcal M,s'\vDash\phi\text{ för alla efterföljare }s'\text{ till }s&\\&\mathcal M,s\vDash\text{AG}\ \phi&&\text{om, f.a. vägar }s_1\rarr s_2\rarr\dots\text{ fr. }s\text{, gäller att }\mathcal M,s_i\vDash\phi\text{ f. alla }i&\\&\mathcal M,s\vDash\text{AF}\ \phi&&\text{om, f.a. vägar }s_1\rarr s_2\rarr\dots\text{ fr. }s\text{, gäller att }\mathcal M,s_i\vDash\phi\text{ f. \underline{något} }i&\end{align}}\]

\[\scriptsize{\begin{align}&\mathcal M,s\vDash\text{EX}\ \phi&\enspace&\text{om }\mathcal M,s'\vDash\phi\text{ för ngn efterföljare }s'\text{ till }s&\\&\mathcal M,s\vDash\text{EG}\ \phi&&\text{om, f. någon väg }s_1\rarr s_2\rarr\dots\text{ fr. }s\text{, gäller att }\mathcal M,s_i\vDash\phi\text{ f. alla }i&\\&\mathcal M,s\vDash\text{EF}\ \phi&&\text{om, f. någon väg }s_1\rarr s_2\rarr\dots\text{ fr. }s\text{, gäller att }\mathcal M,s_i\vDash\phi\text{ f. \underline{något} }i&\end{align}}\]

Viktiga ekvivalenser

De Morgans lagar för CTL:

\[\begin{align*}&\lnot\text{AX}\ \phi&\equiv&&&\text{EX}\ \lnot\phi\\&\lnot\text{AG}\ \phi&\equiv&&&\text{EF}\ \lnot\phi\\&\lnot\text{AF}\ \phi&\equiv&&&\text{EG}\ \lnot\phi\end{align*}\]

Föreläsning 15 (13/11-2024)

Vårt språk

Vi har modeller \(M=(S,\rarr,L)\) där \(S\) är tillstånd, \(\rarr\) övergångar och \(L\) tillståndsvariabler (sanna i olika tillstånd).

Exempel: En server.
Vi kan beskriva en server med fyra tillstånd: entry (s₁), active (s₂), active request (s₃) och active response (s₄).
Följande övergångar är givna:
entry->active, active->entry, active->active request, active request->active response, active response->active.

Formell notation: \(M,S_i\vDash\phi\) betyder att, i vår modell \(M\), i tillståndet \(S_i\), är \(\phi\) sann. Ofta arbetar man bara i en modell, och då behöver inte \(M\) skrivas ut.

Två nya modaliteter: * \(S_i\vDash AX\phi\): I alla nästa tillstånd från S_i gäller \(\phi\). * \(S_i\vDash EX\phi\): I något nästa tillstånd från \(S_i\) gäller \(\phi\).

Modaliteter, symboler: (se föregående föreläsning)
\(AX\): I nästa tillstånd gäller...
\(AG\): Alla kommande tillstånd, samt det nuvarande, gäller...
\(AF\): Så småningom gäller...
\(EX\): I något nästa tillstånd gäller...
\(EG\): Det finns en väg där alltid gäller...
\(EF\): Det finns en väg där det så småningom gäller...

Gäller följande formler i S₁?

• \(AX\ \text{active}\) Ja.
• \(AG\ \text{active}\) Nej (falskt i t.ex. S₁ självt)
• \(AG(\text{active}\lor\text{entry})\) Ja.
• \(AF\ \text{request}\) Nej. (t.ex. alternering mellan entry och active).

Mer avancerade modaliteter

\(S_1\vDash AGAF\phi\ \ [\text{tolkas som }AG(AF\phi)]\)
Informellt: "Om vi startar från S₁, kommer säkert \(\phi\) att vara sann ett oändligt antal gånger."

\(S_1\vDash AGEF\phi\)
"Om vi startar från S₁, kommer \(\phi\) alltid att vara nåbar."

\(S_1\vDash AFAG\phi\)
"Så småningom stabilt \(\phi\)."

Exempel

Gäller följande i s₁?

• \(AGAF\ \text{active}\)
• \(AGAF\ \text{entry}\) Nej (går att undvika entry).
• \(AGEF\ \text{entry}\) Ja (går alltid att komma till entry).
• \(AFAG\ \text{active}\) Nej.

Bra ekvivalenser: (användbara i vissa fall)

• \(\lnot AX\phi\iff EX\lnot\phi\)
• \(\lnot AG\phi\iff EF\lnot\phi\)
• \(\lnot AF\phi\iff EG\lnot\phi\)

Vissa modaliteter kan alltså definieras med andra, och alla modaliteter är således inte nödvändiga.

Rekursiv verifiering av temporallogiska uttryck

Grundidé: Tänker oss att vi har ett tillstånd S samt en lista över alla efterföljande tillstånd.

Värdet av en temporallogisk formel \(T\) bestäms av \(T\):s värde i S₁,...,S_n.

Försök: Vi tittar på \(EF\phi\).
Följande verkar vara sant:

1. Om \(\phi\) är sant i S så gäller \(EF\phi\) i S.
2. Om \(\phi\) är gäller i något nästa tillstånd S_i, så gäller \(EF\phi\) i S.

Formellt kan detta uttryckas:

1. \(\frac{S\vDash\phi}{S\vDash EF\phi}\)
2. \(\frac{S_i\vDash\phi}{S\vDash EF\phi}\) S_i är efterföljare till S.

Fungerar det här? Nej!

Test: TODO... (se inspelad föreläsning, även gällande avsnittet nedan om AG) + förra föreläsningen

AG

Regeln AG definieras av

\[\begin{cases}AG1:\frac{-}{S\vdash_u AG\phi}\\AG2:\frac{S\vdash\phi\quad S_1\vdash_{U,s}AG\phi,\dots,S_k\vdash_{U,s}AG\phi}{S\vdash_UAG\phi}\end{cases}\]