Övning 1: Bevisa intuitionistiskt: A → (B → A)

Antag A (för att bevisa A → (B → A)) Nu vill vi bevisa B → A Antag B (för att bevisa A) Men vi har redan A från första antagandet Så vi kan härleda A Därmed B → A (implikationsintroduktion) Därmed A → (B → A) (implikationsintroduktion) Svar: Beviset använder nested implikationsintroduktion

Övning 3: Konstruera en Kripke-modell där ¬¬A är sant men A är falskt

W = {w₀, w₁} med w₀ ≤ w₁ w₀ ⊭ A (A gäller inte i w₀) w₁ ⊨ A (A gäller i w₁) Kontrollera ¬A i w₀: ¬A skulle kräva att A inte gäller i alla v ≥ w₀ Men w₁ ≥ w₀ och w₁ ⊨ A, så w₀ ⊭ ¬A Kontrollera ¬¬A i w₀: detta kräver att ¬A inte gäller i alla v ≥ w₀ Vi såg att w₀ ⊭ ¬A, så w₀ ⊨ ¬¬A Alltså: w₀ ⊨ ¬¬A men w₀ ⊭ A Svar: Modell med två världar som visar skillnaden mellan ¬¬A och A

Avancerad

Intuitionistisk logik

Konstruktiv logik utan lagen om uteslutet tredje.

intuitionistisk konstruktiv uteslutet tredje BHK-tolkning

Föreställ dig att du är en detektiv som löser ett mysterium. I klassisk logik skulle du kunna säga 'antingen är butlern skyldig eller så är han oskyldig' - även innan du har bevis. Men som detektiv vill du bara acceptera påståenden du faktiskt kan bevisa. Intuitionistisk logik fungerar som en noggrann detektiv: den accepterar bara påståenden som kan konstruktivt bevisas. Detta betyder att vissa 'självklara' regler från klassisk logik, som lagen om utesluten mitt (A ∨ ¬A), inte längre gäller automatiskt. Istället måste vi visa att vi faktiskt kan bevisa A eller bevisa ¬A.

Fördjupning

Intuitionistisk logik utvecklades av L.E.J. Brouwer och formaliserades av Arend Heyting som en konstruktiv tolkning av matematik och logik. Till skillnad från klassisk logik kräver intuitionistisk logik konstruktiva bevis - för att bevisa ett existenspåstående måste man ge ett konkret exempel, för att bevisa en disjunktion måste man bevisa någon av delarna. Lagen om utesluten mitt (A ∨ ¬A) och dubbel negation (¬¬A → A) gäller inte generellt. BHK-interpretationen (Brouwer-Heyting-Kolmogorov) ger konstruktiv semantik, och Kripke-modeller formaliserar intuitionistisk semantik.

Konstruktiv vs klassisk tolkning

Intuitionistisk logik kräver konstruktiva bevis - vi måste kunna visa hur vi bygger upp sanningen, inte bara att vi inte kan motbevisa den.

Skillnader i tolkning

Klassisk logik: A ∨ ¬A är alltid sant (lagen om utesluten mitt)

Intuitionistisk logik: A ∨ ¬A är sant bara om vi kan bevisa A eller bevisa ¬A

Klassisk logik: ∃x.P(x) är sant om P(x) gäller för något x

Intuitionistisk logik: ∃x.P(x) kräver att vi kan konstruera ett specifikt x

Dubbel negation

Klassisk logik: ¬¬A ⟷ A (dubbel negation är ekvivalent)

Intuitionistisk logik:

· A → ¬¬A gäller alltid (om A är sant kan vi visa att ¬A är falskt)

· ¬¬A → A gäller INTE generellt

Motivering: ¬¬A betyder bara 'det leder till motsägelse att förneka A', vilket inte ger oss ett konstruktivt bevis för A.

Jämförelse mellan klassisk och konstruktiv bevisförståelse

BHK-interpretationen

Brouwer-Heyting-Kolmogorov-interpretationen ger konstruktiv betydelse åt logiska konnektiv genom att beskriva vad som krävs för att bevisa varje typ av påstående.

BHK för logiska konnektiv

Ett bevis för A ∧ B är ett par (p,q) där p bevisar A och q bevisar B

Ett bevis för A ∨ B är antingen (1,p) där p bevisar A, eller (2,q) där q bevisar B

Ett bevis för A → B är en funktion som omvandlar bevis för A till bevis för B

Ett bevis för ¬A är en funktion som omvandlar bevis för A till en motsägelse

BHK för kvantifikatorer

∃x.P(x) (existens):

Ett bevis är ett par (a, p) där a är ett specifikt objekt och p är ett bevis för P(a)

∀x.P(x) (universal):

Ett bevis är en funktion som för varje objekt a ger ett bevis för P(a)

Skillnad från klassisk: vi måste faktiskt konstruera objektet i existensbevis.

BHK-interpretationen av logiska konnektiv

Intuitionistiska bevisregler

Intuitionistisk logik har samma introduktions- och elimineringsregler som klassisk logik, men vissa klassiska teorem gäller inte.

Giltiga intuitionistiska regler

Konjunktion:

· A, B ⊢ A ∧ B (introduktion)

· A ∧ B ⊢ A (eliminering vänster)

· A ∧ B ⊢ B (eliminering höger)

Disjunktion:

· A ⊢ A ∨ B (introduktion vänster)

· B ⊢ A ∨ B (introduktion höger)

· A ∨ B, A → C, B → C ⊢ C (eliminering)

Implikation och negation

A → B introduktion: från A ⊢ B, härleda ⊢ A → B

A → B eliminering: från A → B och A, härleda B (modus ponens)

¬A definition: ¬A ≡ (A → ⊥) där ⊥ är falskt

ex falso: från ⊥ kan vi härleda vad som helst

Regler som INTE gäller intuitionistiskt

· Lagen om utesluten mitt: A ∨ ¬A

· Dubbel negation eliminering: ¬¬A → A

· Pierce's lag: ((A → B) → A) → A

· Reductio ad absurdum i full form

Dessa kan bara användas om de specifikt bevisats för det aktuella fallet.

Kripke-modeller för intuitionistisk semantik

Kripke-modeller ger en formell semantik för intuitionistisk logik genom partiellt ordnade mängder av 'kunskapstillstånd'.

Kripke-struktur

K = (W, ≤, ⊨) där:

W = mängd av världar (kunskapstillstånd)

≤ = partiell ordning (informationsökning)

⊨ = tvingande relation (vad som gäller i varje värld)

Persistens: om w ⊨ p och w ≤ v, så v ⊨ p

Semantik för konnektiv

w ⊨ A ∧ B iff w ⊨ A och w ⊨ B

w ⊨ A ∨ B iff w ⊨ A eller w ⊨ B

w ⊨ A → B iff för alla v ≥ w: om v ⊨ A så v ⊨ B

w ⊨ ¬A iff för alla v ≥ w: v ⊭ A

Intolerans är nyckelskillnaden - vi kan inte 'gå bakåt' i kunskap.

Kripke-modell som visar intuitionistisk semantik

Konstruktiv matematik

Intuitionistisk logik leder till konstruktiv matematik där existensbevis måste ge explicita konstruktioner.

Konstruktiva existensbevis

Klassiskt bevis att √2 är irrationellt:

Antag √2 = p/q i lägsta termer. Då 2q² = p², så p är jämnt...

Motsägelse ⟹ √2 är irrationellt.

Konstruktivt: detta bevisar bara ¬(√2 är rationellt), inte att √2 existerar som reellt tal. För konstruktivt bevis måste vi visa explicit konstruktion av √2.

Konstruktiv analys

Kontinuitet: funktioner måste vara uniformt kontinuerliga

Kompakthet: ändliga övertäckningar måste konstrueras

Välordning: välordningsprincipen gäller inte generellt

Mellanvärdessatsen: kräver konstruktiva bevis

Relation till datavetenskap

Intuitionistisk logik har starka kopplingar till datavetenskap genom Curry-Howard-isomorfin och typteori.

Curry-Howard-korrespondens

Propositioner ↔ Typer

Bevis ↔ Program

Bevis för A → B ↔ Funktion från typ A till typ B

Modus ponens ↔ Funktionsapplikation

Konstruktiva typteori

Martin-Löf typteori:

· Dependent types: typer som beror på värden

· Propositions as types: propositioner är typer

· Proof objects: bevis är program av rätt typ

Detta används i bevissassistenter som Coq, Agda, Lean.

Curry-Howard-korrespondensen mellan logik och programmering

Vanliga misstag

❌ Använda lagen om utesluten mitt okritiskt

A ∨ ¬A gäller inte automatiskt i intuitionistisk logik

Exempel: Fel: anta P(n) ∨ ¬P(n) för godtyckligt n utan att bevisa någon av delarna

❌ Förväxla ¬¬A med A

Dubbel negation eliminering gäller inte generellt intuitionistiskt

Exempel: ¬¬(P ∨ ¬P) är sant, men detta bevisar inte P ∨ ¬P

❌ Använda icke-konstruktiva existensbevis

Intuitionistiska existensbevis måste ge konkreta exempel

Exempel: Fel: bevisa ∃x.P(x) genom att visa ¬∀x.¬P(x) utan att ge specifikt x

Tillämpningar

Konstruktiv matematik

Matematik där alla existensbevis ger explicita konstruktioner

Exempel: Konstruktiv analys, algoritmisk talteori, konstruktiv geometri

Programverifiering

Formell verifiering av program genom Curry-Howard-korrespondensen

Exempel: Coq, Agda, Lean - bevissassistenter för programkorrekthet

Typteori och funktionell programmering

Dependent types och avancerade typsystem

Exempel: Haskell, ML, Idris - språk med uttrycksfulla typsystem

Kryptografi och säkerhet

Konstruktiva säkerhetsbevis som ger konkreta algoritmer

Exempel: Zero-knowledge bevis, säkra protokoll med explicita konstruktioner

Övningar

1 Lätt

Bevisa intuitionistiskt: A → (B → A)

Tips

Använd implikationsintroduktion två gånger

Visa facit

Antag A (för att bevisa A → (B → A))
Nu vill vi bevisa B → A
Antag B (för att bevisa A)
Men vi har redan A från första antagandet
Så vi kan härleda A
Därmed B → A (implikationsintroduktion)
Därmed A → (B → A) (implikationsintroduktion)

Svar: Beviset använder nested implikationsintroduktion

2 Medel

Förklara varför ¬¬(P ∨ ¬P) är sant intuitionistiskt men P ∨ ¬P inte nödvändigtvis är det

Tips

Visa att antagandet ¬(P ∨ ¬P) leder till motsägelse

Visa facit

För att bevisa ¬¬(P ∨ ¬P), antag ¬(P ∨ ¬P)
Detta betyder: varken P eller ¬P gäller
Från 'inte P' får vi ¬P
Men då skulle P ∨ ¬P gälla (höger disjunkt)
Motsägelse med vårt antagande
Alltså ¬¬(P ∨ ¬P)
Men för P ∨ ¬P måste vi bevisa antingen P eller ¬P konkret

Svar: ¬¬(P ∨ ¬P) kan bevisas konstruktivt men P ∨ ¬P kräver specifikt bevis

3 Svår

Konstruera en Kripke-modell där ¬¬A är sant men A är falskt

Tips

Använd två världar där A inte gäller i den första men det inte finns sätt att bevisa ¬A

Visa facit

W = {w₀, w₁} med w₀ ≤ w₁
w₀ ⊭ A (A gäller inte i w₀)
w₁ ⊨ A (A gäller i w₁)
Kontrollera ¬A i w₀: ¬A skulle kräva att A inte gäller i alla v ≥ w₀
Men w₁ ≥ w₀ och w₁ ⊨ A, så w₀ ⊭ ¬A
Kontrollera ¬¬A i w₀: detta kräver att ¬A inte gäller i alla v ≥ w₀
Vi såg att w₀ ⊭ ¬A, så w₀ ⊨ ¬¬A
Alltså: w₀ ⊨ ¬¬A men w₀ ⊭ A

Svar: Modell med två världar som visar skillnaden mellan ¬¬A och A

Sammanfattning

Intuitionistisk logik kräver konstruktiva bevis och accepterar bara påståenden som kan bevisas genom explicit konstruktion. BHK-interpretationen ger konstruktiv semantik där bevis måste visa hur sanningar byggs upp. Lagen om utesluten mitt och dubbel negation gäller inte generellt. Kripke-modeller formaliserar intuitionistisk semantik genom partiellt ordnade kunskapstillstånd. Intuitionistisk logik har starka kopplingar till datavetenskap genom Curry-Howard-korrespondensen och används inom konstruktiv matematik, programverifiering och typteori.