{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "b9745d4b",
   "metadata": {},
   "source": [
    "(deduction)=\n",
    "(argumentationDeductive)=\n",
    "(proofDeduction)=\n",
    "(deductiveProof)=\n",
    "(proofDeductive)=\n",
    "# ⤓ Deduktiv argumentasjon"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "44f0eace",
   "metadata": {},
   "source": [
    "## Forutsetninger og læringsmål<span class=map></span>\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "745ce7a5",
   "metadata": {},
   "source": [
    "##  Introduksjon<span class=introduction></span>\n",
    "\n",
    "**Deduksjon** er å bruke regler til å utlede at en konklusjon er sann gitt premisser.  Noen vil si at bare deduktiv argumentasjon fortjener å kalles **bevis**.\n",
    "\n",
    "````{margin}\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "  ranksep=\"0.01\"\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      Premiss [label=\"x² = 5 − 4x\"]\n",
    "      a [label=\"x² + 4x - 5 = 0\"]\n",
    "      Konklusjon [label=\"x = 1 ∨ x = -5\"]\n",
    "      Premiss -> a [label=\"Bytt og flytt\"]\n",
    "      a -> Konklusjon [label=\"abc-regelen\"]\n",
    "}\n",
    "```\n",
    "```` \n",
    "En <span class=example>deduksjon</span> kan altså være \n",
    "* En likningsløsning (f.eks. hvor premisset er påstanden $x^2 = 5 - 4x$ og konklusonen er påstanden $x = 1 ∨ x = -5$; aktuelle regler kan være [likningsregler](equation) og [abc-formelen](abcFormula)).\n",
    "* Et bevis, f.eks. for at det finnes uendelig mange primtall\n",
    "\n",
    "### Premiss og konklusjon<span class=introduction></span>\n",
    "````{margin}\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "    size=5;\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      Premiss\n",
    "      { node [shape=point]\n",
    "          a\n",
    "          b\n",
    "          c\n",
    "      }\n",
    "      Konklusjon\n",
    "      Premiss -> a\n",
    "      a -> b\n",
    "      b -> c\n",
    "      c -> Konklusjon\n",
    "}\n",
    "```\n",
    "```` \n",
    "\n",
    "Bevis starter i et (eller flere) påstander som kalles **premiss**, og ender med en påstand som er **konklusjonen**.  [Regler](ruleStatement) fra premiss til konklusjon gjør at man (om argumentasjonen er gyldig, da) kan være sikker på at om premissene er sanne er også konklusjonen sann.\n",
    "\n",
    "````{margin} Bevis med flere premiss\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "    size=5;\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      p1 [label=\"Premiss 1\"]\n",
    "      p2 [label=\"Premiss 2\"]\n",
    "      p3 [label=\"Premiss 3\"]\n",
    "      { node [shape=point]\n",
    "          a\n",
    "          b\n",
    "          c\n",
    "      }\n",
    "      Konklusjon\n",
    "      p1  -> a\n",
    "      p2 -> a\n",
    "      p3 -> b\n",
    "      a -> b\n",
    "      b -> c\n",
    "      c -> Konklusjon\n",
    "}\n",
    "```\n",
    "```` \n",
    "\n",
    "Har vi flere premisser må vi selvsagt være sikker på at alle premissene er sanne før vi kan garantere at konklusjonen er sann.\n",
    "\n",
    "\n",
    "\n",
    "(inni)=\n",
    "### Et bevis bruker/inneholder tidligere kjente regler<span class=introduction></span>\n",
    "Et bevis bruker regelen vi tror på fra før.\n",
    "\n",
    "(abcFormla)=\n",
    "(abcRuleProof)=\n",
    "<span class=example>Eksempel: *abc*-regelen</span>\n",
    "Vi kan bevise [*abc*-regelen](abcRule) på liknende måte.  Vi begynner med en utregning som bruker kjente regler inni.  Når vi vet at vi kan gå fra premisset (her: $ax^2 + bx + c = 0$) til konklusjonen (her: $x = \\frac{-b ±\\sqrt{b^2 - 4ab}}{2a}$) kan vi så gjøre det til en generell regel.\n",
    "\n",
    "$ax^2 + bx + c = 0$<br/>\n",
    "$\\small ↓$<br/>\n",
    "$x^2 + \\frac{b}{a}x + \\frac{c}{a} = 0$<br/>\n",
    "$\\small ↓$<br/>\n",
    "$x^2 + \\frac{b}{a}x = −\\frac{c}{a}$<br/>\n",
    "$\\small ↓$ Vi legger altså til $ \\left(\\frac{b}{2a}\\right)²$ for å \"fullføre kvadratet\"<br/>\n",
    "$x^2 + \\frac{b}{a}x + \\left(\\frac{b}{2a}\\right)² =  −\\frac{c}{a} + \\left(\\frac{b}{2a}\\right)²$ <br/>\n",
    "$\\small ↓$ Lettere å se om man regner baklengs?<br/>\n",
    "$\\small ↓$$\\left(x + \\frac{b}{2a}\\right)² =  \\frac{-c}{a} + \\left(\\frac{b}{2a}\\right)²$ <br/> \n",
    "$\\small ↓$ Utvider brøker<br/>\n",
    "$\\left(x + \\frac{b}{2a}\\right)² =  \\frac{-4ac}{4a²} + \\frac{b²}{4a²}$<br/>\n",
    "$\\small ↓$<br/>\n",
    "$\\left(x + \\frac{b}{2a}\\right)² =  \\frac{b² -4ac}{4a²}$ <br/>\n",
    "$\\small ↓$ Kvadratrot på begge sider<br/>\n",
    "$x + \\frac{b}{2a} =  ±\\sqrt{\\frac{b² -4ac}{4a²}}$<br/>\n",
    "$\\small ↓$<br/>\n",
    "$x  = -\\frac{b}{2a} + \\frac{±\\sqrt{b² -4ac}}{\\sqrt{4a²}}$ <br/>\n",
    "$\\small ↓$<br/>\n",
    "$x  = -\\frac{b}{2a} + \\frac{±\\sqrt{b² -4ac}}{2a}$ <br/>\n",
    "$\\small ↓$<br/>\n",
    "$x = \\frac{-b ±\\sqrt{b^2 - 4ab}}{2a}$\n",
    "\n",
    "(Mange vil oppleve at utregningen ser grei ut, om vi følger det ledd for ledd; men det er vanskelig å forstå prosessen med å komme fram til den.  Det er kanskje enklest å komme fram til utregningen om man regner baklengs.  Mer om dette om prosessen TODO)\n",
    "\n",
    "### Et bevis kan bli til en ny regel<span class=introduction></span>\n",
    "\n",
    "\n",
    "````{sidebar} 1. kvadratsetning\n",
    ":class: width50\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "  compound=true;\n",
    "  ranksep=\"0.02\"\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "  subgraph cluster_manual{      \n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      manualTitle [label=\"Utregning\\nbevis\" shape=plaintext fontsize=20]\n",
    "      manualStart [label=\"(a + b)²\"]\n",
    "      manual1 [label=\"(a + b)×(a + b)\"]\n",
    "      manual2 [label=\"a(a + b) + b(a + b)\"]\n",
    "      manual3 [label=\"a×a + a×b + b×a + b×b\"]\n",
    "      manual4 [label=\"a² + ab + ab + b²\"]\n",
    "      manualEnd [label=\"a² + 2ab + b²\"]\n",
    "      /* Edges */\n",
    "      manualTitle -> manualStart [style=invis]\n",
    "      manualStart -> manual1 [label=\"A² → A×A\"]\n",
    "      manual1 -> manual2 [label=\"Distributiv lov\"]\n",
    "      manual2 -> manual3 [label=\"Distributiv lov\\n2 ganger\\l\"]\n",
    "      manual3 -> manual4 [label=\"A×A → A²\\lkommutativ ×\\l\"]\n",
    "      manual4 -> manualEnd [label=\"A + A → 2A\"]\n",
    "  }\n",
    "  subgraph cluster_rule{      \n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      ruleTitle [label=\"Regel\" shape=plaintext fontsize=20]\n",
    "      ruleStart [label=\"(a + b)²\"]\n",
    "      ruleEnd [label=\"a² + 2ab + b²\"]\n",
    "      ruleTitle -> ruleStart [style=invis]\n",
    "      ruleStart -> ruleEnd [label=\"Ny regel!\"]\n",
    "  }\n",
    "  {\n",
    "        edge[penwidth=3 constraint=false arrowhead=vee fontsize=12]\n",
    "      manualTitle -> ruleTitle[ltail=cluster_manual lhead=cluster_rule color=\"blue\"  minlen=2 label=\"\" fontcolor=blue]         \n",
    "    }\n",
    "\n",
    "}\n",
    "```\n",
    "```` \n",
    "\n",
    "<span class=example>Eksempel: 1. kvadratsetning</span>\n",
    "\n",
    "```{figure} ../images/static/kvadratsetning1.png\n",
    "---\n",
    "width: 100%\n",
    "align: right\n",
    "figclass: margin\n",
    "```\n",
    "\n",
    "Vi kan bevise [1. kvadratsetning](kvadratsetning) på måten vist til høyre.  Vi tar utgangspunkt i en utregning som bruker kjente regler.  Denne kan så forkortes til en ny regel.\n",
    "\n",
    "Reglene vi startet med er på en måte \"inni\" den nye regelen.  Vi kaller det noen ganger *inni-regler*.  Noen ganger hender det at vi glemmer inni-regler og bare bruker den nye regelen; men helst bør en lærer kunne gå tilbake og forklare inni-reglene når det trengs. \n",
    "\n",
    "### Regel → bevis → regel\n",
    "Vi ser at bevis har regler [inni](inni) seg (under: Tegnet mot venstre) og kan \"bli til\" nye bevis (under: tegnet mot høyre).  Vi kan få kjeder av slike bevis, hvor de simpleste er lengst til venstre mens de mest konkrete er til høyre.\n",
    "\n",
    "Forsøksvis(!) kan vi tegne opp dette slik:\n",
    "\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "  compound=true;\n",
    "  ranksep=\"0.02\"\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "  subgraph cluster_distributive{\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      distributiveName [label=\"Distributiv lov\" fontsize=20]\n",
    "      distributivePremise [label=\"a×(b + c)\"]\n",
    "      distributiveConclusion [label=\"a×b + a×c\"]\n",
    "      distributiveName -> distributivePremise [style=invis]\n",
    "      distributivePremise -> distributiveConclusion\n",
    "  }\n",
    "  subgraph cluster_rule{      \n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      ruleTitle [label=\"1. kvadratsetning\" shape=plaintext fontsize=20]\n",
    "      ruleStart [label=\"(a + b)²\"]\n",
    "      ruleEnd [label=\"a² + 2ab + b²\"]\n",
    "      ruleTitle -> ruleStart [style=invis]\n",
    "      ruleStart -> ruleEnd [label=\"Ny regel\\l1. □setning\\l\"]\n",
    "  }\n",
    "  subgraph cluster_abc{\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      abcName [label=\"abc-regelen\" fontsize=20]\n",
    "      abcMiddle [shape=point]\n",
    "      abcPremise [label=\"ax^2 + bx + c = 0\"]\n",
    "      abcConclusion [label=\"x = (-b - √(b² - 4ac))/2a\\n∨\\nx = (-b + √(b² - 4ac))/2a\"]\n",
    "      abcName -> abcPremise [style=invis]\n",
    "      abcPremise -> abcMiddle\n",
    "      abcMiddle -> abcConclusion\n",
    "  }\n",
    "  subgraph cluster_equation{\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      equationName [label=\"Vår likning\" fontsize=20]\n",
    "      equationPremise [label=\"1x^2 + 4x − 5 = 0\"]\n",
    "      equationConclusion [label=\"x = −5 ∨ x = 1\"]\n",
    "      equationName -> equationPremise [style=invis]\n",
    "      equationPremise -> equationConclusion\n",
    "  }\n",
    "  subgraph cluster_manual{      \n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      manualTitle [label=\"Utregning\\nbevis\" shape=plaintext fontsize=20]\n",
    "      manualStart [label=\"(a + b)²\"]\n",
    "      manual1 [label=\"(a + b)×(a + b)\"]\n",
    "      manual2 [label=\"a(a + b) + b(a + b)\"]\n",
    "      manual3 [label=\"a×a + a×b + b×a + b×b\"]\n",
    "      manual4 [label=\"a² + ab + ab + b²\"]\n",
    "      manualEnd [label=\"a² + 2ab + b²\"]\n",
    "      /* Edges */\n",
    "      manualTitle -> manualStart [style=invis]\n",
    "      manualStart -> manual1 [label=\"A² → A×A\"]\n",
    "      manual1 -> manual2 [label=\"Distributiv lov\"]\n",
    "      manual2 -> manual3 [label=\"Distributiv lov\\n2 ganger\\l\"]\n",
    "      manual3 -> manual4 [label=\"A×A → A²\\lkommutativ ×\\l\"]\n",
    "      manual4 -> manualEnd [label=\"A + A → 2A\"]\n",
    "  }\n",
    "  {\n",
    "        edge[penwidth=3 constraint=false arrowhead=vee fontsize=12 color=blue fontcolor=blue label=\"Applikasjon\\nInnsetting\"]\n",
    "        distributiveName -> manual2\n",
    "        distributiveName -> manual3\n",
    "        ruleTitle -> abcMiddle\n",
    "        abcName -> equationName\n",
    "  }\n",
    "  {\n",
    "        edge[penwidth=3 constraint=false arrowhead=vee fontsize=12]\n",
    "      manualTitle -> ruleTitle[ltail=cluster_manual lhead=cluster_rule color=\"blue\"  minlen=2 label=\"\" fontcolor=blue]         \n",
    "    }\n",
    "\n",
    "}\n",
    "```\n",
    "\n",
    "Hva har vi så helt til venstre?  Her kan vi ha\n",
    "* Aksiom (f.eks. [Peanos aksiomer](peano))\n",
    "* [Handlinger i representasjonsspråk](actionProof); men hvordan er så representasjonsspråkene utviklet?\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4c40605a",
   "metadata": {},
   "source": [
    "## \"Bevistyper\"<span class=introduction></span>\n",
    "Noen ganger snakker man om *bevistyper*; induksjonsbevis, indirekte bevis etc.  Ellef mener det er mer fruktbart å snakke om bevis utifra hvilke regler de bruker.  Bevistypene kan defineres slik:\n",
    "* Induksjonsbevis: Bruker [induksjonsregelen](induction)\n",
    "* Indirekte bevis: Bruker en av de [indirekte](indirect) reglene\n",
    "* Direkte bevis: Bruker ikke en av de indirekte reglene\n",
    "* Uttømming-bevis: Bruker regelen om [uttømming](exhaustion)\n",
    "\n",
    "### Implikasjon og ekvivalens<span class=uttrykk></span>\n",
    "\n",
    "Argument og regler med `⇒` kalles **implikasjon**.  Argument og regler med `⇔`, som går begge veier, kalles **ekvivalens**.  <span class=example>$x = 2 ⇒ x^2 = 4$ er en implikasjon, men ikke en ekvivalens: Det finnes et tilfelle der $x^2 = 4$ er sann (vi snakker om tilfellet at <var>x</var> er −2) men $x = 2$ er usann, så det blir helt feil om noen påstår at $x^2 = 4 ⇒ x = 2$.</span>\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2707b250",
   "metadata": {},
   "source": [
    "## Representasjoner<span class=representation></span>\n",
    "### Navn<span class=representation></span>\n",
    "Mange kaller altså dette *bevis*, til forskjell fra annen argumentasjon.\n",
    "\n",
    "* {cite}`balacheff1988`, {cite}`balacheff1991`: Mathematical proof (démonstration)\n",
    "\n",
    "### Ord<span class=representation></span>\n",
    "* Premiss\n",
    "* Konklusjon\n",
    "\n",
    "\n",
    "### Formelspråket<span class=representation></span>\n",
    "```{figure} proofList.png\n",
    "---\n",
    "figclass: margin\n",
    "align: right\n",
    "width: 100%\n",
    "```\n",
    "\n",
    "<!--````{sidebar}\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "    node[shape=rectangle]\n",
    "    premise [label=\"Premiss\\n(a + b)²\"]\n",
    "    b [label=\"(a + b)(a + b)\"]\n",
    "    c [label=\"a(a + b) + b(a + b)\"]\n",
    "    d [label=\"a·a + a·b + b·a + b·b\"]\n",
    "    e [label=\"Konklusjon\\na² + 2ab + b²\"]\n",
    "    premise -> b [label=\"Eksisterende regel\"]\n",
    "    b -> c [label=\"Distributiv lov\"]\n",
    "    c -> d [label=\"Distributiv lov 2 ganger\"]\n",
    "    d -> e\n",
    "}\n",
    "```\n",
    "```` -->\n",
    "\n",
    "````{sidebar} 1. kvadratsetning\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "    size=5;\n",
    "  ranksep=\"0.01\"\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "      bgcolor=\"#FFEEFA\"\n",
    "      /* Nodes */\n",
    "      manualStart [label=\"(a + b)²\"]\n",
    "      manual1 [label=\"(a + b)×(a + b)\"]\n",
    "      manual2 [label=\"a(a + b) + b(a + b)\"]\n",
    "      manual3 [label=\"a×a + a×b + b×a + b×b\"]\n",
    "      manual4 [label=\"a² + ab + ab + b²\"]\n",
    "      manualEnd [label=\"a² + 2ab + b²\"]\n",
    "      /* Edges */\n",
    "      manualStart -> manual1 [label=\"A² → A×A\"]\n",
    "      manual1 -> manual2 [label=\"Distributiv lov\"]\n",
    "      manual2 -> manual3 [label=\"Distributiv lov\\n2 ganger\\l\"]\n",
    "      manual3 -> manual4 [label=\"A×A → A²\\lkommutativ ×\\l\"]\n",
    "      manual4 -> manualEnd [label=\"A + A → 2A\"]\n",
    "}\n",
    "```\n",
    "```` \n",
    "\n",
    "Fra før vet vi at påstander kan inneholde  objekt med tegnet `=` mellom.  <br/>\n",
    "Argumenter kan inneholde påstander med tegnet `⇒` mellom.  Andre tegn (som `⇔` `⇐`) gir andre typer påstander.\n",
    "\n",
    "\n",
    "Dette kan vi vise tydelig ved bokser.  I følgende eksempel har vi tre nivå bokser: Den ytterste er et argument, den midterste to påstander og de innerste er fire objekt.  Legg merke til at `=` setter sammen to objekt til en påstand og at `⇒` setter sammen to påstander til et argument.<br/>\n",
    "$\\fbox{\\(\n",
    "  \\fbox{\\(\n",
    "     \\fbox{2 + \\(x\\)}\\) = \\(\n",
    "     \\fbox{\\(x^2\\) - 4}\n",
    "   \\)}\n",
    " ⇒ \n",
    "  \\fbox{\\(\n",
    "     \\fbox{2 + \\(x\\)} + 4\\) = \\(\n",
    "     \\fbox{\\(x^2\\)}\n",
    "   \\)}\n",
    " \\)}$\n",
    "\n",
    "I noen tradisjoner <span class=nerd>(Naturlig deduksjon, Gentzen)</span> skriver man en argumentasjon eller regel med vannrett strek, f.eks. $\\frac{2 + x = x^2 - 4}{2 + x + 4 = x^2}$.  Problemet med syntaksen er at den kan forveksles med brøk.  Vi vil derfor heller velge å uttrykke tilsvarende med loddrett strek eller pil:   {rule}`2 + x = x^2 - 4, 2 + x + 4 = x^2`.  Det kan også tenkes at vi vil uttrykke at argumentasjonen gjelder begge veier:  {rule-equals}`2 + x = x^2 - 4, 2 + x + 4 = x^2`\n",
    "\n",
    "I noen skolesammenhenger setter man to streker under konklusjonen.  Det er mulig praksisen holder på å forsvinne siden den var enkel med teknologien “blyant og linjal” men vanskelig med en del digitale skriveprogram.\n",
    "\n",
    "\n",
    "\n",
    "(proofPointArrow)=\n",
    "(pointArrow)=\n",
    "### Bokser og piler<span class=representation></span>\n",
    "\n",
    "````{sidebar} Induksjonsbevis\n",
    "```{graphviz-source}\n",
    "digraph G{\n",
    "  size=5;\n",
    "  ranksep=\"0.4\"\n",
    "  bgcolor=\"#FFEEFA\"\n",
    "  node[shape=\"plaintext\" fontsize=14]\n",
    "  edge [fontsize=10 arrowhead=vee]\n",
    "  grunn1 [label=\"Premiss 1\\n1 = 1\"]\n",
    "  grunn2 [label=\"1 ≥ 1\"]\n",
    "  grunnsteg [label=\"Grunnsteg\\n{n |-> 1}\\n1² ≥ 1\"]\n",
    "  induksjonssteg [label=\"Induksjonssteg\\n{n |→ k} => {n |→ k+1}\\nk² ≥ k  =>  (k+1)² ≥ k+1\"]\n",
    "  induksjon1a [label=\"k² ≥ k  =>  k² ≥ k\"]\n",
    "  induksjon1b [label=\"2k > 0\"]\n",
    "  induksjon2 [label=\"k² ≥ k  =>  k² + 2k ≥ k\"]\n",
    "  induksjon3 [label=\"k² ≥ k  =>  k² + 2k + 1 ≥ k + 1\"]\n",
    "  conclusion [label=\"Konklusjon\\nn² ≥ n, n ∈ ℕ\"]\n",
    "  grunn1 -> grunn2 [label=\"a = a → a ≥ a\"]\n",
    "  grunn2 -> grunnsteg [label=\"1 → 1²\"]\n",
    "  induksjon1a -> induksjon2\n",
    "  induksjon1b -> induksjon2\n",
    "  induksjon2 -> induksjon3 \n",
    "  induksjon3 -> induksjonssteg\n",
    "  grunnsteg -> conclusion:n\n",
    "  induksjonssteg -> conclusion:n [label=\"Selve induksjonsregelen\"]\n",
    "}\n",
    "```\n",
    "```` \n",
    "\n",
    "\n",
    "Man kan representere påstander med for eksempel formelspråk og omskrivingene mellom dem med for eksempel piler som dem vi har brukt som regler.  Pilenes retning er typisk mot høyre eller nedover.  Da får man en representasjon som den til høyre.\n",
    "\n",
    "\n",
    "````{sidebar} Bevisgraf fra artikkel\n",
    "```{image} Proof-graph-for-the-example-proof.png\n",
    "---\n",
    "width: 300px\n",
    "```\n",
    "[Fra (Balser et al., 2004)](https://www.researchgate.net/publication/220744198_Interactive_Verification_of_UML_State_Machines)\n",
    "```` \n",
    "\n",
    "\n",
    "#### Teknologier for bokser og piler<span class=representation></span>\n",
    "\n",
    "* [Graphviz](graphviz) (som er brukt i de fleste slike diagram i Mashov).  \n",
    "* Word Smart Art\n",
    "* PowerPoint\n",
    "* Papir og blyant, evt. sammen med mobilkamera\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a4ce6e59",
   "metadata": {},
   "source": [
    "## Algoritmer<span class=algorithm></span>\n",
    "\n",
    "\n",
    "### Evaluere bevis<span class=algorithm></span>\n",
    "Finne om et bevis er sant.\n",
    "\n",
    "Om vi snakker om en rekke påstander bundet sammen av regler kan vi i prinsippet sjekke alle regel-applikasjonene (alle overgangene mellom linjer).  Har reglene forutsetninger vi må passe på?\n",
    "\n",
    "<span class=example>Sjekk</span> for eksempel følgende utregning:\n",
    "\n",
    "$a = b$ &nbsp; (forutsetning) </br>\n",
    "$a^2 = ab$ &nbsp; (ganger med $a$ på begge sider</br>\n",
    "$a^2 - b^2 = ab - b^2$ &nbsp; (trekker fra $b^2$ på begge sider)</br>\n",
    "$(a + b)(a - b) = b(a - b)$ &nbsp; (faktoriserer, [konjugatsetningen](conjugat) og [distributivitet](distributivity))</br>\n",
    "$a + b = b$ &nbsp; (deler på $(a - b)$ på begge sider i [likningen](equation))</br>\n",
    "$b + b = b$ &nbsp; (siden vi har forutsatt $a = b$ kan vi [sette inn](substitution) $\\{a ↦ b\\}$)</br>\n",
    "$2 = 1$ &nbsp; (deler på $b$ på begge sider)\n",
    "\n",
    "Vi har altså bevist at $2 = 1$.  Det er jo mildt sagt overraskende og slår beina vekk under det meste av det vi holder på med.  Hva er feil?\n",
    "\n",
    "```{dropdown} Løsningsforslag\n",
    "Heldigvis kan vi avsløre feilen.  Den ligger i linja der vi deler på $a-b$ på begge sider.  Siden $a = b$ er nemlig $a - b$ lik 0.  Vi kan ikke dele på 0 på begge sider.  Det må vi alltid passe på når vi deler på begge sider!\n",
    "```\n",
    "\n",
    "\n",
    "### Finne / lage bevis<span class=algorithm></span>\n",
    "Dette er mye vanskeligere!  Vi snakker mer om dette under [prosess](columnProcess), som er neste [kolonne](column).\n",
    "\n",
    "Vi har en del standard triks om [problemløsing](problemSolution), bl.a. fra Polya.  Noen av dem er:\n",
    "* Bruk eksempler først\n",
    "* Representer alt du vet, både om premissene og svaret\n",
    "* Arbeid både fra premissene og fra konklusjonen (\"overfra og nedenfra\")\n",
    "\n",
    "Som lærere er det vel sjelden vi får i oppgave å lage \"store\" bevis.  Men det er vanlig at vi må \"bevise\" vanlige regler.  Noen bevis kan man huske, men man bør også kunne lage noen nye.\n",
    "\n",
    "Når elevene lager utregninger bruker de også mange av de samme teknikkene.\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "#### <span class=task>Oppgaver</span>\n",
    "TODO flytte?\n",
    "\n",
    "<span class=task>Oppgave: Bevis at 2 + 3 = 5.</span>\n",
    "\n",
    "<span class=task>Oppgave: Bevis at summen av to oddetall alltid er et partall.</span>\n",
    "\n",
    "<span class=task>Bevis at  $∀(n + 1) = p^2 + q^2$</span>\n",
    "\n",
    "\n",
    "Oppgave: “Bevis at ethvert oddetall kan skrives som en sum av to kvadrattall”.\n",
    "\n",
    "Hva er objektene?  Hvordan kan de representeres?\n",
    "\n",
    "Hva er påstanden du skal bevise?\n",
    "\n",
    "Forsøk å lage et bevis, og observer prosessen.  Om dere er en gruppe kan tre stk lage bevis og én observere.  Legg for eksempel merke til om dere beviser fra premisset til konklusjon eller om dere beviser baklengs.\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "### Løfte elever til regelbasert deduksjon<span class=\"algorithm\"></span>\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "84846784",
   "metadata": {},
   "source": [
    "## Aspekt\n",
    "\n",
    "\n",
    "\n",
    "Argumentet $x - 1 = 2 ⇒ x = 2 + 1$ kan forståes på flere måter:\n",
    "* En påstand om at om premisset $x - 1 = 2$ er sann må konklusjonen $x = 2 + 1$ være sann.\n",
    "* I alle verdener hvor premisset $x - 1 = 2$ er sann må konklusjonen $x = 2 + 1$ være sann.\n",
    "* Mengden av alle verdener hvor premisset $x - 1 = 2$ er sann er delmengde $⊂$ av alle verdener hvor konklusjonen $x = 2 + 1$ er sann.\n",
    "* En regel / redskap.  Om vi tilfeldigvis vet at premisset er sant kan vi bruke regelen til å påstå at konklusjonen er sann.\n",
    "* En mulig omskriving: Vi kan skrive om $x - 1 = 2$ til $x = 2 + 1$: {rule}`x - 1 = 2, x = 2 + 1`."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1f44f7c9",
   "metadata": {},
   "source": [
    "## Læring<span class=learning></span>\n",
    "Tilsvarer sannsynligvis viktige måter å [generalisere](general) på.\n",
    "\n",
    "\n",
    "\n",
    "## Datatyper\n",
    "\n",
    "Skissemessig, dette er muligens utenfor MA302; men Ellef synes det er interessant!\n",
    "\n",
    "Objekt:\n",
    "* 1, 2, 3: ℕ\n",
    "* ¼, ⅓, ½: ℚ\n",
    "* π, <var>e</var>, √2: ℝ\n",
    "* +, −, ×, ÷: ℝ × ℝ → ℝ (altså: de tar to reelle tall som argument og gir et nytt reelt tall)\n",
    "* √: ℝ > 0 → ℝ\n",
    "\n",
    "Påstander:\n",
    "* =, <, ≠: ℝ × ℝ → 𝔹 (altså: de tar to reelle tall som argument og gir en sannhetsverdi)\n",
    "* ∧, ∨: 𝔹 × 𝔹 → 𝔹 (∧ betyr og, ∨ betyr eller)\n",
    "* ¬: 𝔹 → 𝔹\n",
    "\n",
    "Argument:\n",
    "* ⇒, ⇔: 𝔹 × 𝔹 → 𝔹\n",
    "\n",
    "\n",
    "\n",
    "Objekt er typisk av typene ℕ eller ℝ.  Påstander (sannhetsverdier) er sanne eller usanne — typen 𝔹?"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.16"
  },
  "toc": {
   "base_numbering": 1,
   "nav_menu": {},
   "number_sections": true,
   "sideBar": true,
   "skip_h1_title": false,
   "title_cell": "Table of Contents",
   "title_sidebar": "Contents",
   "toc_cell": false,
   "toc_position": {},
   "toc_section_display": true,
   "toc_window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}