Övning 1: Bevisa: P ∧ Q ⊢ Q ∧ P (kommutativitet för konjunktion)

1. P ∧ Q (antagande) 2. Q (från 1, ∧E-höger) 3. P (från 1, ∧E-vänster) 4. Q ∧ P (från 2,3, ∧I) Svar: Q ∧ P följer genom eliminering och återinförande av konjunktion

Övning 2: Bevisa: P → (Q → (P ∧ Q))

Övning 3: Bevisa: (P → Q) → ((Q → R) → (P → R)) (transitivitet)

Övning 4: Bevisa: P ∨ Q ⊢ ¬¬P ∨ Q

Övning 5: Bevisa en av De Morgans lagar: ¬P ∨ ¬Q ⊢ ¬(P ∧ Q)

Medel

Naturlig deduktion

Formella bevis med naturlig deduktion och bevisträd.

naturlig deduktion bevisträd antagande härledning bevis

Tänk dig att du ska övertyga någon om att en påstående är sant. Du kan inte bara säga 'för att jag säger det' - du måste bygga upp ditt argument steg för steg, där varje steg är så självklart att ingen kan ifrågasätta det. Detta är essensen av naturlig deduktion. Istället för att bara använda färdiga slutledningsregler som modus ponens, bygger vi bevis från grunden genom att göra antaganden, härleda konsekvenser och sedan 'kasta bort' antaganden när vi inte längre behöver dem. Det är som att bygga en ställning för att nå en hög hylla - vi sätter upp strukturer tillfälligt för att komma dit vi vill, och tar sedan bort dem när vi är klara.

Fördjupning

Naturlig deduktion är ett bevissystem utvecklat av Gerhard Gentzen som formaliserar hur matematiker faktiskt konstruerar bevis. Till skillnad från axiomatiska system som börjar med färdiga sanningar, eller slutledningstabeller som bara verifierar giltighet, låter naturlig deduktion oss systematiskt konstruera bevis genom att göra antaganden och sedan avsluta (discharge) dem. Systemet har införande- och elimineringsregler för varje logisk operator. Det är 'naturligt' eftersom det speglar vårt intuitiva sätt att resonera och är grunden för många moderna bevissystem och programverifieringsverktyg.

Grundprinciper och bevisträd

I naturlig deduktion skriver vi bevis som träd där varje gren representerar en logisk slutledning. Vi använder antaganden som 'löv' och bygger upp mot roten som är vår slutsats.

Grundläggande bevisstruktur

Antaganden placeras överst (löven)

Slutledningsregler appliceras nedåt

Slutsatsen är roten av trädet

Antaganden kan 'avslutas' (discharged) under bevisets gång

Enkelt bevis: P ∧ Q ⊢ P

P ∧ Q (antagande)

——————

P (∧-eliminering)

Detta läses: 'Från antagandet P ∧ Q kan vi härleda P genom konjunktionseliminering'

Visuell representation av bevisträd med antaganden, regler och slutsatser

Regler för konjunktion (∧)

Konjunktion har två regler: införande (hur vi skapar ∧) och eliminering (hur vi använder ∧). Dessa speglar vår intuition om 'och'.

Konjunktionsinförande (∧I)

Om vi kan bevisa P och vi kan bevisa Q

Då kan vi bevisa P ∧ Q

Regel: P Q / P ∧ Q

Vi 'sammansätter' två separata bevis

Konjunktionseliminering (∧E)

Om vi kan bevisa P ∧ Q

Då kan vi bevisa P (vänster eliminering)

Eller vi kan bevisa Q (höger eliminering)

Regler: P ∧ Q / P och P ∧ Q / Q

Fullständigt bevis: (P ∧ Q) ∧ R ⊢ P ∧ R

1. (P ∧ Q) ∧ R (antagande)

2. P ∧ Q (från 1, ∧E-vänster)

3. R (från 1, ∧E-höger)

4. P (från 2, ∧E-vänster)

5. P ∧ R (från 4,3, ∧I)

Regler för implikation (→)

Implikationsreglerna är kärnan i naturlig deduktion. Införande av implikation kräver att vi gör antaganden och sedan 'släpper' dem.

Implikationseliminering (→E) - Modus ponens

Om vi har P → Q och vi har P

Då kan vi härleda Q

Regel: P → Q P / Q

Detta är precis modus ponens!

Implikationsinförande (→I)

För att bevisa P → Q:

1. Antag P (tillfälligt antagande)

2. Härleda Q från P

3. 'Släpp' antagandet P

4. Slutsats: P → Q

Bevis av identitetslag: ⊢ P → P

1. | P (antagande för →I)

| P (samma som rad 1)

2. P → P (från 1, →I, avsluta antagandet)

Detta bevisar att 'om P så P' utan att förutsätta något!

Illustration av hur implikationsregler används med antaganden som avslutas

Regler för disjunktion (∨)

Disjunktionsregler hanterar 'eller'. Införande är enkelt, men eliminering kräver fallanalys.

Disjunktionsinförande (∨I)

Om vi kan bevisa P, då kan vi bevisa P ∨ Q

Om vi kan bevisa Q, då kan vi bevisa P ∨ Q

Regler: P / P ∨ Q och Q / P ∨ Q

Vi kan alltid 'lägga till' fler alternativ

Disjunktionseliminering (∨E) - Fallanalys

Om vi har P ∨ Q och vill bevisa R:

1. Antag P och bevisa R

2. Antag Q och bevisa R

3. Då kan vi dra slutsatsen R

Vi måste hantera alla möjliga fall

Bevis av kommutativitet: P ∨ Q ⊢ Q ∨ P

1. P ∨ Q (antagande)

2. | P (antagande för ∨E)

3. | Q ∨ P (från 2, ∨I-höger)

4. | Q (antagande för ∨E)

5. | Q ∨ P (från 4, ∨I-vänster)

6. Q ∨ P (från 1,2-3,4-5, ∨E)

Regler for negation (¬)

Negationsregler hanterar motsägelser. I klassisk logik använder vi ofta bevis genom motsägelse (reductio ad absurdum).

Negationsinförande (¬I) - Reductio ad absurdum

För att bevisa ¬P:

1. Antag P

2. Härleda en motsägelse (⊥)

3. Slutsats: ¬P

Om P leder till motsägelse, måste ¬P vara sant

Negationseliminering (¬E)

Om vi har ¬P och P

Då får vi en motsägelse ⊥

Regel: ¬P P / ⊥

Detta upptäcker logiska inkonsistenser

Klassisk regel: Lagen om uteslutet tredje

Bevis av ⊢ P ∨ ¬P:

1. | ¬(P ∨ ¬P) (antagande för ¬I)

2. | | P (antagande för ¬I)

3. | | P ∨ ¬P (från 2, ∨I-vänster)

4. | | ⊥ (från 1,3, ¬E)

5. | ¬P (från 2-4, ¬I)

6. | P ∨ ¬P (från 5, ∨I-höger)

7. | ⊥ (från 1,6, ¬E)

8. P ∨ ¬P (från 1-7, ¬I avsluta dubbel negation)

Komplexa bevis och strategier

Riktiga bevis kombinerar alla regler och kräver strategiskt tänkande om vilka antaganden som behövs och när de ska avslutas.

Bevisstrategi

Titta på målformeln - vilken huvudoperator har den?

För P → Q: använd →I, antag P och bevisa Q

För P ∧ Q: använd ∧I, bevisa P och Q separat

För P ∨ Q: använd ∨I, bevisa antingen P eller Q

För ¬P: använd ¬I, antag P och härleda motsägelse

Bevis av De Morgans lag: ¬(P ∧ Q) ⊢ ¬P ∨ ¬Q

1. ¬(P ∧ Q) (antagande)

2. | ¬(¬P ∨ ¬Q) (antagande för ¬I)

3. | | P (antagande för ¬I)

4. | | | Q (antagande för ¬I)

5. | | | P ∧ Q (från 3,4, ∧I)

6. | | | ⊥ (från 1,5, ¬E)

7. | | ¬Q (från 4-6, ¬I)

8. | | ¬P ∨ ¬Q (från 7, ∨I-höger)

9. | | ⊥ (från 2,8, ¬E)

10. | ¬P (från 3-9, ¬I)

11. | ¬P ∨ ¬Q (från 10, ∨I-vänster)

12. | ⊥ (från 2,11, ¬E)

13. ¬P ∨ ¬Q (från 2-12, ¬I)

Visuell representation av ett komplext bevis med flera nivåer av antaganden

Vanliga misstag

❌ Glömma avsluta antaganden

Studenter gör antaganden men glömmer att 'släppa' dem med rätt regel

Exempel: Att anta P för att bevisa P → Q men glömma använda →I för att avsluta antagandet

❌ Använda antaganden utanför deras räckvidd

Ett antagande som avslutats kan inte användas senare i beviset

Exempel: Efter att ha avslutat antagandet P med →I, försöka använda P igen på nästa rad

❌ Förväxla införande och eliminering

Använda fel riktning på reglerna

Exempel: Försöka gå från P till P ∧ Q utan att ha Q (fel användning av ∧I)

❌ Ofullständig fallanalys vid ∨E

Glömma hantera alla fall när man eliminerar disjunktion

Exempel: Från P ∨ Q bara bevisa målet under antagandet P, men glömma fallet Q

Tillämpningar

Programverifiering

Moderna bevissystem som Coq och Lean använder naturlig deduktion för att verifiera programkorrekthet

Exempel: Att bevisa att en sorteringsalgoritm alltid producerar en sorterad lista

Matematiska bevis

Naturlig deduktion formaliserar hur matematiker faktiskt konstruerar bevis

Exempel: Bevis av matematiska satser genom antaganden och härledningar

Logisk programmering

Språk som Prolog bygger på principer från naturlig deduktion

Exempel: Prologregler motsvarar implikationer och queries kör 'bakåt' bevis

Automatiska bevisverktyg

Många AI-system för automatisk bevisföring använder naturlig deduktion

Exempel: Verktyg som hjälper matematiker att konstruera och verifiera komplexa bevis

Typteori och funktionella språk

Typkontroll i språk som Haskell och ML bygger på naturlig deduktion

Exempel: Curry-Howard correspondence: typer motsvarar propositioner, program motsvarar bevis

Övningar

1 Lätt

Bevisa: P ∧ Q ⊢ Q ∧ P (kommutativitet för konjunktion)

Tips

Använd ∧E för att få ut P och Q separat, sedan ∧I för att sätta ihop dem i omvänd ordning

Visa facit

1. P ∧ Q (antagande)
2. Q (från 1, ∧E-höger)
3. P (från 1, ∧E-vänster)
4. Q ∧ P (från 2,3, ∧I)

Svar: Q ∧ P följer genom eliminering och återinförande av konjunktion

2 Medel

Bevisa: P → (Q → (P ∧ Q))

Tips

Du behöver använda →I två gånger - först för yttre implikationen, sedan för inre

Visa facit

1. | P (antagande för →I)
2. | | Q (antagande för →I)
3. | | P ∧ Q (från 1,2, ∧I)
4. | Q → (P ∧ Q) (från 2-3, →I)
5. P → (Q → (P ∧ Q)) (från 1-4, →I)

Svar: Beviset kräver nästlade antaganden för båda implikationerna

3 Medel

Bevisa: (P → Q) → ((Q → R) → (P → R)) (transitivitet)

Tips

Tre nivåer av →I krävs. Börja med att anta P → Q, sedan Q → R, sedan P

Visa facit

1. | P → Q (antagande för →I)
2. | | Q → R (antagande för →I)
3. | | | P (antagande för →I)
4. | | | Q (från 1,3, →E)
5. | | | R (från 2,4, →E)
6. | | P → R (från 3-5, →I)
7. | (Q → R) → (P → R) (från 2-6, →I)
8. (P → Q) → ((Q → R) → (P → R)) (från 1-7, →I)

Svar: Beviset använder tre nästlade antaganden och modus ponens

4 Svår

Bevisa: P ∨ Q ⊢ ¬¬P ∨ Q

Tips

Använd ∨E för fallanalys. I P-fallet behöver du bevisa ¬¬P, i Q-fallet har du redan Q

Visa facit

1. P ∨ Q (antagande)
2. | P (antagande för ∨E)
3. | | ¬P (antagande för ¬I)
4. | | ⊥ (från 2,3, ¬E)
5. | ¬¬P (från 3-4, ¬I)
6. | ¬¬P ∨ Q (från 5, ∨I-vänster)
7. | Q (antagande för ∨E)
8. | ¬¬P ∨ Q (från 7, ∨I-höger)
9. ¬¬P ∨ Q (från 1,2-6,7-8, ∨E)

Svar: Fallanalys där vi behöver bevisa dubbel negation i ena fallet

5 Svår

Bevisa en av De Morgans lagar: ¬P ∨ ¬Q ⊢ ¬(P ∧ Q)

Tips

Använd ¬I - antag P ∧ Q och härleda motsägelse. Du behöver fallanalys på ¬P ∨ ¬Q

Visa facit

1. ¬P ∨ ¬Q (antagande)
2. | P ∧ Q (antagande för ¬I)
3. | | ¬P (antagande för ∨E)
4. | | P (från 2, ∧E-vänster)
5. | | ⊥ (från 3,4, ¬E)
6. | | ¬Q (antagande för ∨E)
7. | | Q (från 2, ∧E-höger)
8. | | ⊥ (från 6,7, ¬E)
9. | ⊥ (från 1,3-5,6-8, ∨E)
10. ¬(P ∧ Q) (från 2-9, ¬I)

Svar: Bevis genom motsägelse med fallanalys

Sammanfattning

Naturlig deduktion är ett kraftfullt bevissystem som formaliserar systematisk bevisföring genom antaganden och härledningar. Varje logisk operator har införande- och elimineringsregler: ∧I/∧E för konjunktion, ∨I/∨E för disjunktion, →I/→E för implikation, och ¬I/¬E för negation. Nyckelkonceptet är att göra tillfälliga antaganden och sedan 'avsluta' dem när vi konstruerat önskade slutsatser. Systemet speglar hur matematiker faktiskt resonerar och är grunden för moderna bevissystem och programverifieringsverktyg. Viktiga tekniker inkluderar fallanalys för disjunktion och bevis genom motsägelse för negation. Naturlig deduktion är både intuitivt och formellt rigoröst.