Det formella systemet som en riktad graf
Ett formellt axiomatiskt system definierar en riktad graf:
- Noder: alla välformade formler som kan konstrueras från systemets symboler
- Kanter: inferenssteg — en formel följer från andra genom en inferensregel
- Axiomer: särskilda källnoder utan inkommande kanter
- Satser: alla noder som är nåbara från axiomuppsättningen
Ett bevis för sats T: en riktad väg från axiomuppsättningen till T. Beviset är en sekvens av noder A₁, A₂, ..., Aₙ = T där varje steg följer av en inferensregel.
Två grundläggande egenskaper för ett formellt system, uttryckta geometriskt:
Konsistens: ingen formel F och dess negation ¬F är båda nåbara från axiomerna. Geometriskt: satsnoden F och satsnoden ¬F är inte båda nåbara. Ingen 'explosion'-väg existerar.
Fullständighet: varje formel F eller ¬F är en sats (nåbar). Geometriskt: grafen är starkt sammanhängande i den meningen att för varje nod F har minst en av F eller ¬F en väg från axiomerna.
Gödels ofullständighetsteorem som en geometrisk egenskap
Kurt Gödel bevisade 1931 att alla konsistenta formella system som är tillräckligt kraftfulla för att uttrycka grundläggande aritmetik är ofullständiga: det finns formler G sådana att varken G eller ¬G är bevisbar.
Geometriskt: i varje tillräckligt rik konsistent formellt system finns det noder i formelgrafen som inte är nåbara från axiomerna — varken noden G eller noden ¬G har en väg från axiomuppsättningen.
Gödels konstruktion: han kodade en formel G som säger, i praktiken, 'Jag är inte bevisbar.' Om G vore bevisbar, skulle systemet vara inkonsistent (ett sant påstående säger att det inte är bevisbart). Om ¬G vore bevisbar, skulle systemet vara inkonsistent (G skulle vara falskt men systemet bevisar det). Så varken G eller ¬G är bevisbar — G är en onåbar nod i ett konsistent system.
Ofullständigheten är inte en brist i de valda axiomerna: Gödel visade att det är en strukturell egenskap för alla konsistenta system som är tillräckligt expressiva för att hantera aritmetik. De onåbara noderna kan inte tas bort genom att lägga till fler axiomer utan att generera nya.
Matematiska objekt som punkter i ett rum
Den platonska synen på matematik kan formaliseras geometriskt: matematiska objekt bebor ett abstrakt rum vars punkter är själva objekten och vars struktur ges av relationerna mellan dem.
Betrakta de naturliga talen ℕ = {0, 1, 2, 3, ...}. Delbaarhetsrelationen definierar en partiell ordning: m delar n omm m | n. Denna partiella ordning definierar en geometri — Hasse-diagrammet för delbarhetsgittret.
Varje primtal sitter vid en minimal position ovanför 1. Varje sammansatt tal sitter ovanför sina primfaktorer. Strukturen för detta rum kodar all talteori.
Vad gör detta platonsk: strukturen existerar oavsett om någon sinne studerar den. Det faktum att 7 är primtal — att 7 inte har några delare mellan 1 och 7 — är ett faktum om positionen för 7 i delbarhetsgittret, oberoende av notation, kultur eller civilisation.
Vilken civilisation som helst som undersöker räkning och delbaarhet kommer att upptäcka samma struktur. Talystemets geometri är universell.
Navigera i delbarhetsgittret
I delbarhetsgittret motsvarar minsta gemensamma multipel (mgm) av två tal deras join (lägsta övre gräns) och största gemensamma delare (sgd) motsvarar deras meet (största nedre gräns).
Sgd kan beräknas via Euklides algoritm: sgd(a, b) = sgd(b, a mod b), avslutas när b = 0.
Vad abstraktion tar bort
Geometrisk abstraktion: projicering av ett högt-dimensionellt objekt på ett lågt-dimensionellt delrum. Projektionen förlorar information (koordinater som inte är i delrummet) men behåller delrummets struktur perfekt.
Matematisk abstraktion fungerar på samma sätt. En grupp är en mängd med en binär operation som uppfyller fyra axiomer. Att abstrahera till gruppstruktur tar bort: de specifika elementen, den specifika operationens beräkningsregel, all ytterligare struktur (ordning, metrik, topologi). Vad som återstår: skeletten av fyra axiomer.
Nyttan: varje teorem om grupper gäller för ALLA grupper — heltal under addition, rotationer under komposition, permutationer under komposition, symmetrier av en molekyl, Galois-grupper av polynomekvationer — samtidigt. Det abstrakta teoremet är bevisbart en gång; dess instanser är gratis.
Det är därför rena matematiker motsätter sig att lägga till domänspecifika antaganden: varje tillagt antagande begränsar teoremets tillämplighet. Ett teorem om fält (som kräver multiplikativ invers) gäller färre strukturer än ett teorem om ringar (som inte kräver multiplikativ invers).
Avvägningen mellan precision och generalitet
Det finns en avvägning: mer abstrakta teorem gäller mer allmänt men säger mindre om specifika instanser. Ett teorem om vektorrum över en kropp säger mindre om ℝ^n än ett teorem särskilt om ℝ^n (där avstånd och vinkel definieras).
Hammings underförstådda regel: abstrahera så långt som möjligt medan du behåller de egenskaper du behöver. Abstrahera för långt och dina teorem blir trivialt allmänna ('vilken mängd som helst med vilken operation som helst uppfyller...'). Abstrahera för lite och dina teorem misslyckas att överföra till nya applikationer.