You are here: TUCS > PUBLICATIONS > Publication Search > Matematik med lite logik: Intr...
Matematik med lite logik: Introduktion till strukturerade härledningar
Ralph-Johan Back, Matematik med lite logik: Introduktion till strukturerade härledningar. TUCS Lecture Notes 7, Turku Centre for Computer Science, 2008.
Abstract:
Vi ger i den här artikeln en översikt av strukturerade härledningar som ett format för matematiska bevis och härledningar. Formatet tillåter noggranna bevis av vanliga matematiska påståenden med en liten dos logik. Avsikten är att bevisen som konstrueras skall vara lätta att förstå och överblicka, och att det skall vara lätt att kontrollera om bevisen är riktiga, både för den som själv utför beviset och för den som läser beviset för första gången.
En central målsättning med strukturerade härledningar är att öka användningen av formell logisk argumentering och matematiska bevis på gymnasienivå. Det här sker på två olika plan. Dels så skrivs strukturerade härledningar med ett fast bevisformat, en syntes av Dijkstras linjära härledningar och Gentzen-liknande bevissystem. Dels så använder vi logisk notation och logiska slutledningsregler på samma sätt som vi använder aritmetik och algebra, som ett systematiskt och logiskt sätt att räkna fram resultat.
Möjligheterna att använda logik i skolmatematiken, för att förenkla och systematisera argumenteringen och härledningarna, verkar vara praktiskt taget obegränsade. Den notation som används inom matematiken och matematikundervisningen i dag är mycket traditionell. Den har utvecklats under många århundraden, och har inte nämnvärt påverkats av det senaste 150 årens forskning inom matematisk logik. Detta har lett till att samma logiska begrepp beskrivs på olika sätt och med olika notation inom olika delområden av matematiken. Enkla och grundläggande logiska inferensregler skrivs heller aldrig ut explicit, utan eleven förväntas förstå och lära sig tillämpa dessa genom någon slags osmotisk process, där lärarens förståelse överförs till eleven via en samling exempel. Kort sagt, dagens gymnasiematematik presenteras på ett onödigt invecklat och osystematiskt sätt.
Samtidigt vill vi inte gå för långt i formaliseringen av bevisen. Det vanliga sättet att introducera logik är att börja med syntaxen för termer och formler i systemet, sedan beskriver man den axiomatiska metoden med sina bevisregler och teoribegreppet, och till slut introduceras sanningsbegreppet och modeller för teorier. Under vägen bevisar man ett antal metateorem om axiomatiska bevissystem, av mer eller mindre avancerad natur. Problemet med den här angreppssättet är att det gör något som i sig själv är ganska enkelt och intuitivt till en avancerad matematisk teori. De flesta studerande upplever matematisk logik som svår, och ser inte heller hur den kan användas i praktiken. Framställningssättet implicerra att en strängt logisk bevisföring endast kan utföras inom en fullständigt axiomatiserad teori, och att varje bevis inom en sådan teori måste vara exakt och detaljerat. I slutändan har vi en ansats till att lära ut bevisteknik som inte ger den praktiska färdighet som man önskar att de studerande skulle få.
Vi försöker därför gå en medelväg. Strukturerade härledningar är en praktisk teknik för att konstruera bevis som är rigorösa, men som inte kräver att den underliggande teorin är totalt axiomatiserad. Bevisens riktighet är då beroende av att argumenteringen i den underliggande teorin stämmer. Om så är fallet, har vi ett korrekt bevis. Det här ger oss en separation mellan å ena sidantekniken för att skriva ner bevis och å andra sidan axiomatiseringen av den underliggande teorin. Den här separationen gör att strukturerade härledningar kan användas på vilket område som helst inom matematiken.
Målsättningen med den här handledningen är att ge en allmän översikt över strukturerade härledningar, med exempel tagna från gymnasiematematiken. Artikeln kräver inga egentliga förkunskaper utöver den traditionella gymnasiematematiken. Vi börjar med att introducera de centrala egenskaperna hos strukturerade härledningar informellt, med en samling exempel, i avsnitt 2. I avsnitt 3 beskriver vi sedan strukturerade härledningar mera allmänt och ger en exakt syntax för formatet. Vi diskuterar även allmänt hur man bevisar påståenden med strukturerade härledningar. I avsnitt 4 ger vi sedan en kort översikt av metoden, dess ursprung och utveckling, våra erfarentheter av att utnyttja metoden, samt en samling pekare till litteratur på området.
Files:
Full publication in PDF-format
BibTeX entry:
@BOOKLET{Back08c,
title = {Matematik med lite logik: Introduktion till strukturerade härledningar},
author = {Back, Ralph-Johan},
number = {7},
series = {TUCS Lecture Notes},
publisher = {Turku Centre for Computer Science},
year = {2008},
}
Belongs to TUCS Research Unit(s): Learning and Reasoning Lab