Matematisk logik

Matematisk logik ( teoretisk logik [1] , symbolsk logik [2] ) er en gren af ​​matematikken , der studerer matematisk notation , formelle systemer , bevisbarhed af matematiske domme , arten af ​​matematiske bevis generelt, beregnelighed og andre aspekter af matematikkens grundlag. [3] .

I bredere forstand betragtes det som en matematisk gren af ​​formel logik [4]  - " logik efter emne, matematik efter metode " [5] , " logik udviklet ved hjælp af matematiske metoder " [6] .

Historie

De første forsøg på at matematisere logiske operationer blev foretaget ved overgangen til det 13.-14. århundrede af Raymond Lull , som designede en speciel "logisk maskine" til at mekanisere processen med logisk slutning, som han beskrev i sin afhandling "Ars Magna" (" stor kunst"). Hans bil bestod af syv koncentriske cirkler, hvorpå vilkår og bogstaver var markeret. For at opnå kombinationer brugte Lull to koncentriske cirkler opdelt i sektorer af radiale linjer. Han roterede den inderste cirkel og modtog en tabel med forskellige kombinationer. Selvfølgelig var dette forsøg ufuldkomment, men spillede en rolle i den videre udvikling af ideen om matematisering af logiske slutninger.

Det første arbejde med formel logik , der er kommet ned til os , er Aristoteles  's første analyse 384-322 f.Kr.). Den omhandler det grundlæggende i syllogistik  - reglerne for at udlede nogle udsagn fra andre. Så ud fra udtalelserne "Alle mennesker er dødelige" og "Sokrates er en mand" kan vi konkludere, at "Sokrates er dødelig." Men i praksis er sådanne ræsonnementer yderst sjældne.

Spørgsmålet om at skabe symbolsk logik som et universelt videnskabeligt sprog blev overvejet af Leibniz i 1666 i hans værk The Art of Combinatorics ( De arte combinatoria ). Han tænkte på at skrive udsagn på et særligt sprog, så han derefter kunne beregne andres sandhed efter logiske love. I midten af ​​det 19. århundrede udkom de første værker om algebraisering af aristotelisk logik, som dannede det grundlæggende grundlag for sætningsregningen ( Buhl , de Morgan , Schroeder ). I 1847 udgav J. Boole The Mathematical Analysis of Logic, og i 1854, An Investigation of the Laws of Thought, An Investigation of the Laws of Thought. I dem skitserede Boole grundlaget for sin logiske algebra, hvor han anvendte algebraisk symbolik til at registrere logiske operationer og logiske konklusioner. Boolsk algebra for logik i form af klasseregning var det første system af matematisk logik. Hovedresultatet af boolsk algebra er, at de nu ikke er begrænset til anvendelsen af ​​symbolik på logik, men bygger specielle logiske beregninger; logiske love optræder i logikkens algebra som et nødvendigt element i formaliserede systemer; enhver dom betragtes som en udtalelse om klassernes lighed; ræsonnementsprocessen reduceres til at løse logiske ligheder. Men som Jevons bemærkede , var subtraktionsoperationen i denne logiske algebra ikke helt bekvem og førte nogle gange til misforståelser. Booles algebra for logik blev forbedret af W. S. Jevons og E. Schroeder. Jevons selv i sin bog "Ren Logik" kritiserede overdreven matematisering, boolske algebraer for logik og foreslog sin teori baseret på substitutionsprincippet, det vil sige erstatning af lige med lige.

I 1877 udgav Schröder en bog om matematisk logik, Der Operationskreis des Logikkalkuls, hvori han systematisk lagde grundlaget for matematisk logik. Et stort bidrag til udviklingen af ​​matematisk logik blev ydet af den russiske astronom, logiker og matematiker, professor ved Kazan University P. S. Poretsky . Ved at opsummere Boole, Jevons og Schroeder's resultater, på grundlag af mange års uafhængig forskning, skabte han et meningsfuldt værk "Om metoderne til at løse logiske ligheder og om den omvendte metode til matematisk logik", hvori han markant fremmede udviklingen af logikkens algebras apparat. P. S. Poretskys værker overgår ikke kun hans kollegers værker - samtidige, men også med hensyn til logikkens algebra overgår de de tilsvarende sektioner af Whitehead og Russell. PS Poretsky var den første i Rusland, der begyndte at forelæse om matematisk logik. Matematisk logik, sagde han, "i sit emne er logik, men i sin metode er det en matematiker." Han så den matematiske logiks opgave i at "konstruere en slutningsteori", men samtidig bestemte han nøjagtigt forbindelsen og grænsen mellem matematik og matematisk logik. "Hvis de former, der studeres af algebra, er kvantitative," skrev han, "så er de former, som logik omhandler, kvalitative, det vil sige væsentligt forskellige fra de første. Denne forskel mellem de nærmeste undersøgelsesobjekter af algebra og logik gør det umuligt direkte at overføre , dvs. den direkte anvendelse af algebras principper og teknikker til emnet logik. Men tilpasningen af ​​disse teknikker (med fuld bevarelse af deres nøjagtighed) til studiet af kvalitative former er ganske muligt. P. S. Poretskys store bidrag til matematisk logik var den komplette teori om kvalitative former, han foreslog. Han udviklede teorien om logiske ligheder, foreslog den mest generelle, udtømmende metode til at finde alle ækvivalente former for præmisser, alle deres konsekvenser, alle de enkleste uopløselige præmisser hvori et system af lokaler kan nedbrydes.

I værkerne af Frege og Peirce (slutningen af ​​1870'erne - begyndelsen af ​​1880'erne), blev objektvariabler , kvantificerere introduceret i logikken , og derved blev prædikatregning grundlagt . I 1879 præsenterede Frege i sin bog The Calculus of Concepts sin teori om propositionalregning, som blev den første gren af ​​moderne matematisk logik. Heri præsenterede Frege den første aksiomatiske konstruktion af propositionel logik , introducerede begrebet en kvantifier i matematisk logik, som Peirce derefter introducerer i den logiske videnskabs hverdag. Frege introducerede også begrebet sandhedsværdi, foreslået for at skelne mellem egenskaber og relationer som værdier, henholdsvis et-steds og mange-steds propositionelle funktioner . Men Freges ideer fandt ikke umiddelbart tilhængere, og sætningsregningen udviklede sig, som A. Church bemærker, på grundlag af et ældre synspunkt, som det kan ses i Peirce, Schroeder og andres værker.

I slutningen af ​​1880'erne anvendte Dedekind og Peano disse værktøjer i et forsøg på at aksiomatisere aritmetik, mens Peano skabte et bekvemt notationssystem, der er blevet forankret i moderne matematisk logik. Han introducerede symboler i matematisk logik: ∈ er et tegn på at tilhøre en mængde, ⊂ er et tegn på inklusion, ⋃ er et tegn på forening, ∩ er et tegn på skæring af mængder; udviklet et system af aksiomer til aritmetikken af ​​naturlige tal . Men vigtigst af alt, Peano, ved hjælp af den symbolske kalkulus, han opfandt, forsøgte at udforske de grundlæggende matematiske begreber, som var det første skridt i den praktiske anvendelse af matematisk logik til studiet af matematikkens grundlag. I sit fembinds Formulaire de Mathematiques (1895-1905) viste Peano, hvordan matematiske discipliner ved hjælp af symbolsk regning kan konstrueres aksiomatisk.

Whitehead og Russell skriver Principia Mathematica i 1910-1913 . Dette arbejde bidrog væsentligt til udviklingen af ​​matematisk logik langs vejen for yderligere aksiomatisering og formalisering af den propositionelle beregning, klasser og prædikater. B. Russell og A. Whitehead så vejen ud af den krise, som matematikken befandt sig i, i forbindelse med opdagelsen af ​​paradokser i mængdelæren i at reducere al ren matematik til logik . Dette var begrebet logicisme . Til dette formål byggede de et formaliseret logisk-matematisk system, hvor alle meningsfuldt sande sætninger ifølge dem kan bevises. Men det blev hurtigt klart, at B. Russells og A. Whiteheads forsøg på at reducere al ren matematik til logik ikke blev kronet med succes. I 1930-1931 fastslog K. Godel , at ikke kun systemet udviklet af B. Russell og A. Whitehead, men også ethvert system af formaliseret matematik er ufuldstændigt, det vil sige, at ikke alle meningsfuldt sande sætninger kan bevises i det.

Begrebet intuitionisme og intuitionistisk logik introducerede deres vej ud af matematikkens krise og videreudviklingen af ​​logikken ( Brauer , 1908 ). Matematik, sagde de, er matematiske konstruktioner. Et matematisk objekt eksisterer, hvis man ved, hvordan man konstruerer det. Matematikeren beskæftiger sig med en verden af ​​mentale objekter, hvoraf nogle kun kan skabes i grænsen for en ubegrænset rækkefølge af trin, som aldrig slutter og er i konstant tilblivelse. Fra intuitionismens synspunkt er begrebet faktisk, eksisterende uendelighed, som blev overholdt af repræsentanter for det mængdeteoretiske matematikbegreb, fejlagtigt. Derfor undersøger intuitionistisk logik kun konstruktive objekter; eksistensen af ​​sådanne objekter anses for bevist, hvis og kun hvis den endelige måde at konstruere dem på er angivet. Denne logik benægter anvendeligheden af ​​loven om udelukket mellem i operationer med uendelige mængder. Den konstruktive logik , der senere opstod, opfattede kritisk det objektive indhold af intuitionistisk logik og accepterede ikke dens filosofiske og metodiske grundlag.

En stor rolle i udviklingen af ​​matematisk logik blev spillet af Hilbert og W. Ackermans arbejde "The Main Features of Theoretical Logic" (1928), udgivet i Rusland på russisk under titlen "Fundamentals of Theoretical Logic" i 1947, i hvor et program blev skabt til at underbygge matematik gennem aksiomatisk formalisering ved brug af strengt begrænsede midler, der ikke fører til modsætninger. I deres arbejde talte de om det nye inden for matematisk logik: "De logiske forbindelser, der eksisterer mellem domme , begreber osv.," skrev de, "finder deres udtryk i formler, hvis fortolkning er fri for tvetydigheder, der let kunne opstå. med verbalt udtryk. Overgangen til logiske konsekvenser, som sker gennem inferens , dekomponeres i sine sidste elementer og præsenteres som en formel transformation af de oprindelige formler efter kendte regler, som ligner tællereglerne i algebra; logisk tænkning vises i logisk regning. Denne beregning gør det muligt med succes at dække problemer over for hvilke rent meningsfuld logisk tænkning er grundlæggende magtesløs. Hilbert var imod intuitionisme. Han protesterede mod det faktum, at intuitionister benægtede loven om den udelukkede tredjedel i operationer med sæt. "Forbuddet mod eksistenssætninger og loven om den udelukkede midterste  ," skrev han, "er ensbetydende med en fuldstændig afvisning af matematisk videnskab." I sin formaliseringsmetode foreslog Hilbert at omdanne al matematik til et sæt formler, hvori elementer er forbundet ved hjælp af logiske tegn. Grundlaget for matematikkens konstruktion er baseret på bestemte specifikke formler, som kaldes aksiomer. Som sådanne aksiomer tog Hilbert aksiomer fra den matematiske logiks propositionelregning, de matematiske lighedsaksiomer og talaksiomer , hvorfra han fik nye, afledte aksiomer ved hjælp af slutningsregler. Konklusionen blev kun opnået på grundlag af formen af ​​symboler og tegn, bag hvilken der ikke var noget indhold. Formaliseret teori i sin struktur var ikke længere et system af meningsfulde sætninger, men et system af symboler, betragtet som en sekvens af udtryk. Det vigtigste krav, som Hilbert stillede, da han definerede begrebet "eksistens" af et matematisk objekt, var at bevise dets konsistens. Hvis det i et eller andet system viser sig, at A og ikke-A kan udledes i det, så skal et sådant system afvises. Hilbert og hans skole forsøgte kun at retfærdiggøre matematik aksiomatisk, uden at gå ud over logik og matematik.

I trediverne og fyrrerne af det XX århundrede begynder udviklingen af ​​metalogik , hvis emne er studiet af systemet af bestemmelser og begreber af matematisk logik selv, som bestemmer grænserne for denne logik, studerer bevisteorien. De vigtigste sektioner af metalogik er logisk syntese og logisk semantik , studiet af betydningen af ​​sprogudtryk, fortolkninger af logiske beregninger. Metalogisk forskning fokuserer på analyse af forskellige egenskaber ved formaliserede sprog, som senere dannede grundlaget for elektroniske maskiner til automatisering af videnskabelige slutninger. Inden for logisk semantik er værkerne af A. Tarski "On the concept of truth and formalized languages" fra 1933, såvel som værkerne af R. Carnap "Studies in Semantics" fra 1942-1947 anerkendt som de mest betydningsfulde . Også vigtige i udviklingen af ​​matematisk logik var værker inden for logik med mange værdier, hvor udsagn tildeles ethvert endeligt eller uendeligt sæt af sandhedsværdier. Det første sådan system af tre-værdi propositionel logik blev udviklet og foreslået af J. Lukasevich . I 1954 foreslog J. Lukasevich et logiksystem med fire værdier og derefter logik med uendelig værdi. Problemer med logik med mange værdier blev også behandlet af så velkendte matematikere og logikere som E. Post , S. Yaskovsky , D. Webb, A. Geyting , A. N. Kolmogorov , D. A. Bochvar, V. I. Shestakov , H. Reichenbach , S K. Kleene og andre. En af de største tendenser inden for matematisk logik er blevet teorien om matematiske beviser , som opstod fra anvendelsen af ​​logisk beregning på spørgsmål om matematikkens grundlag. Det opstod fra det nittende århundredes logiks algebra, hvis undersøgelse var endelige objekter. Teorien om matematiske beviser beskæftiger sig hovedsageligt med problemet med uendelighed. En af den matematiske logiks hovedopgaver, der bruges i matematikkens regnestykke, er problemet med at etablere konsistens, det vil sige, at det anses for at være konsistent, hvis det er umuligt at udlede formlen A sammen med formlen Ā (ikke-A) ) i det. Ved hjælp af bevisformaliseringsmetoden hjalp matematisk logik matematik med at løse problemerne med bevisbarhed og konsistens i aksiomatiske teorier. Fordelen ved matematisk logik er, at det symbolske apparat, det bruger, gør det muligt strengt at udtrykke de mest komplekse ræsonnementer, koncepter til algoritmisk behandling af computersystemer.

Grundlæggende

Matematisk logik er, ligesom traditionel logik, formel i den forstand, at den abstraherer fra mening og bedømmer forholdet, relationerne og overgangene fra en sætning (udsagn) til en anden og den resulterende konklusion fra disse sætninger ikke på grundlag af deres indhold, men kun på baggrund af sætningsrækkefølgens form.

Brugen af ​​matematiske metoder i logikken bliver mulig, når domme er formuleret i et eksakt sprog. Sådanne præcise sprog har to sider: syntaks og semantik. Syntaks er et sæt regler for konstruktion af sprogobjekter (normalt kaldet formler). Semantik er et sæt af konventioner, der beskriver vores forståelse af formler (eller nogle af dem) og giver os mulighed for at betragte nogle formler som sande og andre ikke.

En vigtig rolle i matematisk logik spilles af begreberne deduktiv teori og calculus . En calculus er et sæt slutningsregler, der gør det muligt at betragte visse formler som afledelige. Inferensregler er opdelt i to klasser. Nogle af dem kvalificerer direkte visse formler som afledelige. Sådanne slutningsregler kaldes aksiomer. Andre tillader os at betragte som afledbare formler , der er syntaktisk relateret på en forudbestemt måde til endelige sæt af afledbare formler. En meget brugt regel af den anden type er modus ponens-reglen: hvis formlerne og er afledelige , så er formlen også afledelig .

Forholdet mellem calculi og semantik udtrykkes i form af semantisk egnethed og semantisk fuldstændighed af calculus. En calculus siges at være semantisk egnet til et sprog, hvis en formel afledt af sproget er sand. På samme måde siges en calculus at være semantisk komplet i et sprog, hvis en gyldig sprogformel kan udledes i .

Mange af de sprog, der betragtes i matematisk logik, har semantisk fuldstændige og semantisk nyttige beregninger. Især er Kurt Gödels resultat kendt, at den klassiske prædikatregning er semantisk komplet og semantisk velegnet til sproget i klassisk førsteordens prædikatlogik ( Gödels fuldstændighedssætning ). På den anden side er der mange sprog, hvor konstruktionen af ​​en semantisk fuldstændig og semantisk egnet kalkulus er umulig. På dette område er det klassiske resultat Gödels ufuldstændighedssætning , der angiver umuligheden af ​​en semantisk fuldstændig og semantisk brugbar regning for sproget i formel aritmetik.

I praksis er mange elementære logiske operationer en obligatorisk del af instruktionssættet for alle moderne mikroprocessorer og er følgelig inkluderet i programmeringssprog . Dette er en af ​​de vigtigste praktiske anvendelser af matematiske logiske metoder, der er studeret i moderne computervidenskabelige lærebøger.

Sektioner

I den matematiske fagklassifikation er matematisk logik kombineret til en sektion på øverste niveau med matematikkens grundlag , hvor følgende afsnit er fremhævet: [7]

Noter

  1. Hilbert, Ackerman, 1947 , s. 5.
  2. Brodsky, 1972 , s. 3.
  3. matematisk logik: definition af matematisk logik i Oxford ordbog (amerikansk engelsk) . Hentet 7. februar 2014. Arkiveret fra originalen 23. februar 2014.
  4. N. I. Kondakov, Logisk ordbogsopslagsbog , M .: "Nauka", 1975, s. 259.
  5. Ifølge definitionen af ​​den første forfatter af værker om matematisk logik på russisk, Platon Poretsky
  6. S. K. Kleene, Mathematical Logic , M., 1973, s.12.
  7. MSC2020-Matematik emneklassifikationssystem . Hentet 22. maj 2021. Arkiveret fra originalen 14. juli 2020.

Litteratur