Alla begrepp som kalkylatorn, guiderna och övningarna använder, definierade på ett ställe.
Slå upp ett begrepp, se dess notation och öppna exemplet i kalkylatorn för att se det i arbete. Begrepp härifrån markeras första gången de förekommer i en guide.
Alla 62 begrepp
Grunder
logik
Studiet av vilka slutsatser som verkligen följer av vilka antaganden.
Logiken studerar resonemangets form snarare än dess innehåll. Formell logik byter ut satser mot symboler, så att frågan om en slutsats följer kan avgöras enbart av argumentets form och kontrolleras mekaniskt.
Ett påstående som är antingen sant eller falskt, men inte både och.
En sats är ett påstående med exakt ett sanningsvärde. ”Det regnar” är en sats; en fråga eller en befallning är det inte, eftersom det inte finns något hos dem som kan vara sant eller falskt.
Ett av de två värden en sats kan ha: sant eller falskt.
Klassisk logik ger varje sats exakt ett av två sanningsvärden, skrivna ⊤ och ⊥ (eller 1 och 0). Varje rad i en sanningstabell är en tilldelning av värden till variablerna och det värde formeln får där.
En atomär sats kan inte delas i mindre satser: den innehåller varken negation, konjunktion eller något annat konnektiv. Allt annat är sammansatt, byggt av atomer, och dess sanningsvärde bestäms av deras.
En bokstav som p eller A som står för en godtycklig sats.
En satsvariabel är en platshållare för vilken sats som helst. Kalkylatorn tar enstaka bokstäver som variabler och ger var och en en kolumn i sanningstabellen, med en rad för varje möjlig kombination av värden.
En teckensträng som språkets grammatik faktiskt tillåter.
En välformad formel byggs enligt reglerna: en variabel är en, och det är även varje formel som bildas av mindre formler med ett konnektiv. ”p ∧ ∨ q” är det inte, och därför rapporterar kalkylatorn ett fel i stället för att gissa.
En tilldelning av sanningsvärden till alla variabler i en formel.
En tolkning säger vad varje variabel är värd och fastställer därmed hela formelns värde. En formel med n variabler har 2ⁿ tolkningar – precis raderna i dess sanningstabell.
Ett argument hävdar att dess slutsats följer av premisserna. Skriv in ett i kalkylatorn med ett följdtecken – premisser före, slutsats efter – så granskas varje rad efter ett fall där premisserna håller och slutsatsen brister.
Ett påstående som ett argument antar för att nå sin slutsats.
Premisserna är argumentets utgångspunkt. Giltighet frågar bara om slutsatsen håller överallt där alla premisser håller; om de faktiskt är sanna är en annan fråga, den som hållbarhet lägger till.
Slutsatsen är det premisserna ska stödja. I kalkylatorn är den uttrycket efter följdtecknet, och ett argument är giltigt när ingen tolkning gör premisserna sanna och slutsatsen falsk.
En symbol som bygger en sammansatt sats av enklare satser.
Ett konnektiv som ¬, ∧, ∨, → eller ↔ förenar satser till en större vars sanningsvärde bara beror på deras. Det är precis det beroendet en sanningstabell registrerar, en rad per kombination av insatsvärden.
Vänder ett sanningsvärde: ¬p är sann precis när p är falsk.
Negationen är satslogikens enda enställiga konnektiv. Skriven ¬p, ~p eller !p gör den sant till falskt och falskt till sant, så två negationer ger tillbaka den ursprungliga satsen.
En konjunktion hävdar båda sina delar, konjunkterna. Den är sann i exakt en rad av sin sanningstabell – den där båda konjunkterna är sanna – vilket gör den till det strängaste av de tvåställiga konnektiven.
Disjunktionen är i logiken inklusiv: p ∨ q är sann när p är sann, när q är sann och när båda är det. Den exklusiva läsningen av ”eller”, sann endast när delarna skiljer sig, är ett eget konnektiv.
Exklusiv disjunktion, skriven ⊕ eller XOR, håller när delarna skiljer sig och brister när de stämmer överens. Den är negationen av bikonditionalen och kan skrivas som (p ∨ q) ∧ ¬(p ∧ q).
Den materiella konditionalen säger inget mer än ”inte: förled sant och efterled falskt”, och håller därför automatiskt så snart förledet brister. Därför är p → q ekvivalent med ¬p ∨ q.
p ↔ q, sann när båda delarna har samma sanningsvärde.
Bikonditionalen hävdar vardera sidan under villkor av den andra: den är sann när båda delarna är sanna och när båda är falska. En bikonditional som är en tautologi uttrycker precis en logisk ekvivalens.
Förledet är det villkor en konditional beror av. När det är falskt är hela konditionalen sann oavsett efterledet, och därifrån kommer de flesta överraskningarna i tabellen för →.
Efterledet är det en konditional påstår följer om dess förled håller. Ett sant efterled gör konditionalen sann, men gör inte förledet sant: att sluta sig till det är ett formellt felslut.
Den omvända till p → q är q → p, och de två är inte ekvivalenta: kalkylatorn hittar en rad där den ena håller och den andra brister. Att behandla dem som utbytbara är att bejaka efterledet.
¬q → ¬p, som alltid har samma sanningsvärde som p → q.
Kontrapositionen negerar båda delarna av en konditional och byter plats på dem. Till skillnad från den omvända är den verkligen ekvivalent med originalet, och det är därför bevis genom kontraposition är legitimt i matematiken.
Negationen av en konjunktion: sann utom när båda ingångarna är sanna.
NAND, skriven ↑, är ¬(p ∧ q). Den är funktionellt fullständig: varje annat konnektiv kan byggas av enbart NAND, vilket gör den till en arbetshäst i digital kretskonstruktion.
Vilket konnektiv som binder först när parenteser saknas.
Negationen binder hårdast, sedan konjunktion, disjunktion, konditional och sist bikonditional. Så läses ¬p ∧ q ∨ r som ((¬p) ∧ q) ∨ r; parenteser åsidosätter ordningen när den avsedda läsningen är en annan.
En rad per värdetilldelning, med formelns värde i varje.
En sanningstabell räknar upp alla 2ⁿ tolkningar av en formels n variabler och beräknar dess värde i var och en. Eftersom den är uttömmande avgör den varje semantisk fråga i satslogiken: ekvivalens, giltighet, uppfyllbarhet och resten.
En tautologi är sann i varje rad av sin sanningstabell och säger därför inget om världen: p ∨ ¬p är sann vad p än är. Två formler är ekvivalenta precis när bikonditionalen mellan dem är en tautologi.
En motsägelse som p ∧ ¬p är falsk i varje rad av sin sanningstabell. Att härleda en ur en uppsättning antaganden visar att de inte alla kan hålla, vilket är motorn i motsägelsebeviset.
En formel som är sann under vissa tolkningar och falsk under andra.
En kontingent formel är varken tautologi eller motsägelse: dess sanningstabell har minst en sann och minst en falsk rad. De flesta formler någon skriver är kontingenta, och det är just det som gör dem informativa.
En formel är uppfyllbar när minst en rad i dess sanningstabell är sann, och den raden är en modell av den. Att avgöra uppfyllbarhet är SAT-lösarnas centrala problem och därmed en stor del av automatiserat resonerande.
Ekvivalenta formler stämmer överens under varje tolkning, så den ena kan ersätta den andra överallt utan att innehållet ändras. Sätt ett likhetstecken mellan två uttryck så jämför kalkylatorn deras kolumner rad för rad.
Slutsatsen håller i varje tolkning där premisserna håller.
Skriven Γ ⊨ φ är logisk följd det som ett giltigt argument gör anspråk på. Den kontrolleras genom att söka ett motexempel: en tolkning som gör alla premisser sanna och slutsatsen falsk. Finns inget sådant håller följden.
Ingen tolkning gör premisserna sanna och slutsatsen falsk.
Giltighet är en egenskap hos argumentets form, inte hos fakta: ett giltigt argument får ha falska premisser och en falsk slutsats. Vad det inte kan ha är sanna premisser jämte en falsk slutsats.
Ett giltigt argument vars premisser dessutom är sanna.
Hållbarhet lägger ett sakpåstående till ett formellt: argumentet är giltigt och dess premisser håller. Logiken ensam avgör första halvan; den andra hör till det argumentet handlar om.
En tolkning som gör premisserna sanna och slutsatsen falsk.
En motmodell bevisar att ett argument är ogiltigt – en rad räcker. Kalkylatorn visar den rad den hittar, vilket förvandlar ”detta följer inte” till en konkret tilldelning som går att kontrollera för hand.
Någon tolkning gör alla påståenden i mängden sanna samtidigt.
En mängd premisser är konsistent när de alla kan hålla tillsammans. Inkonsistenta premisser medför vad som helst, så ett argument byggt på dem är tekniskt giltigt och värt ingenting.
Literalerna är normalformernas atomer: en klausul är en disjunktion av literaler och en minterm en konjunktion av dem. En literal är positiv när variabeln står bar och negativ när den är negerad.
En klausul är en av de parentesgrupper som en konjunktiv normalform består av. Eftersom en konjunktion bara är sann när varje del är det, håller en KNF-formel precis när alla dess klausuler håller.
Ett ELLER av OCH: en disjunktion av konjunktioner av literaler.
Varje formel har en disjunktiv normalform, och den kan läsas direkt ur sanningstabellen: en konjunktion per sann rad, förenade med ∨. Kalkylatorn ger också en minimerad DNF, som säger samma sak med färre literaler.
Konjunktiv normalform läses ur sanningstabellens falska rader, en klausul per rad. Det är det indataformat SAT-lösare förväntar sig, vilket gör omskrivning till KNF till ett rutinsteg i automatiserat resonerande.
En konjunktion som pekar ut exakt en rad i sanningstabellen.
En minterm nämner varje variabel en gång, negerad eller ej, så att precis en tolkning uppfyller den. Att samla mintermerna för de sanna raderna och förena dem med ∨ ger formelns disjunktiva normalform.
En disjunktion som utesluter exakt en rad i sanningstabellen.
En maxterm nämner varje variabel en gång och är falsk i en enda tolkning. Att ta maxtermen för varje falsk rad och förena dem med ∧ ger formelns konjunktiva normalform.
Negation gör ∧ till ∨ och ∨ till ∧: ¬(p ∧ q) ≡ ¬p ∨ ¬q.
De Morgans lagar trycker in en negation över en konjunktion eller disjunktion och vänder konnektivet på vägen. Så drivs en formel mot en normalform, och så förenklas negationer i kod och i kretsar.
Dubbelnegationen gäller i klassisk logik åt båda hållen, så ¬¬p och p kan alltid bytas ut mot varandra. Intuitionistisk logik behåller bara riktningen från p till ¬¬p, och där skiljs de två systemen åt.
Algebran med två värden och ∧, ∨ och ¬ som operationer.
Boolesk algebra är satslogik skriven som räkning med 0 och 1, med lagar – kommutativitet, distributivitet, absorption, De Morgan – som låter uttryck skrivas om och förenklas. Det är den matematik digitala kretsar konstrueras i.
Ett rutnät över sanningstabellen som gör förenklingar synliga.
Ett Karnaughdiagram ordnar raderna så att grannrutor skiljer sig i en variabel, och kanterna hänger ihop. Det skrivs också K-diagram, K-map eller kmap. Rektangulära grupper av intilliggande ettor av storlek 1, 2, 4 eller 8 läses då direkt som termer i ett minimalt uttryck.
En implikant är en konjunktion av literaler som tvingar formeln att vara sann; den är prim när borttagande av vilken literal som helst skulle förstöra det. I ett Karnaughdiagram är primimplikanterna de maximala rektanglarna av ettor.
När en etta i diagrammet hör till bara en maximal grupp måste den gruppen ingå i varje minimal täckning och tas därför först. Det som återstår är den del av täckningen som verkligen måste sökas.
Ett kretselement som beräknar ett konnektiv på sina ingångar.
AND-, OR-, NOT-, NAND-, NOR- och XOR-grindar är konnektivens motsvarighet i hårdvara. En formel och en krets är samma objekt ritat två gånger, och därför kan kalkylatorn visa ett uttryck som ett grindschema.
Ett tillåtet steg från redan härledda formler till en ny.
En slutledningsregel är ett mönster som modus ponens, tillämpligt så snart formler av rätt form finns. Bevissystem byggs av en handfull sådana, valda så att bara slutsatser som följer kan härledas.
Modus ponens är konditionalens grundregel: givet en konditional och dess förled följer efterledet. Giltigheten syns i sanningstabellen – den enda raden med båda premisserna sanna har också slutsatsen sann.
Modus tollens går baklänges genom en konditional: brister efterledet kan förledet inte ha hållit. Det är kontrapositionen i arbete och formen hos varje argument som vederlägger en hypotes genom att pröva dess förutsägelser.
Den hypotetiska syllogismen kedjar samman konditionaler, vilket är det som gör långa härledningar möjliga: varje länk för argumentet ett steg längre utan att någon premiss hävdas.
Den disjunktiva syllogismen stryker det uteslutna alternativet: håller ett av två alternativ och det första inte gör det, måste det andra göra det. Det är regeln bakom uteslutningsresonemang.
Att bevisa en slutsats genom att tillämpa regler steg för steg.
Naturlig deduktion härleder en slutsats ur premisser med introduktions- och elimineringsregler för varje konnektiv, och tillåter tillfälliga antaganden som senare avlägsnas. Den bevisar det som en sanningstabell kontrollerar, utan att gå igenom varje rad.
Anta motsatsen, härled en motsägelse, dra den ursprungliga slutsatsen.
För att bevisa φ antar man ¬φ och härleder något av formen ψ ∧ ¬ψ. Eftersom ingen tolkning gör en motsägelse sann kan antagandet inte hålla, och φ följer. Så går bevis för irrationalitet och oändlighet vanligen till.
Ett sant efterled fastställer inte förledet: något annat kan ha åstadkommit det. Kalkylatorn visar motmodellen – p falsk, q sann – vilket är den rad som skiljer detta från modus ponens.
En konditional säger inget om vad som händer när dess förled brister, så att utesluta förledet lämnar efterledet öppet. Motmodellen är den rad där p är falsk och q sann.
Logik som ser in i satser, på objekt och deras egenskaper.
Predikatlogiken lägger till predikat, termer och kvantorer, så att ”varje primtal större än två är udda” blir en formel i stället för en enda bokstav. Den är strikt mer uttrycksfull än satslogiken, och ingen sanningstabell kan avgöra den.
En symbol som säger hur många objekt ett predikat gäller för.
De två klassiska kvantorerna är ∀ (alla) och ∃ (minst en), och var och en är den andras negation med negerad kropp. Variabeln som en kvantor binder är det som skiljer predikatlogik från satslogik.
Ett universellt påstående vederläggs av ett enda motexempel och håller tomt över en tom domän. ∀x φ är ekvivalent med ¬∃x ¬φ, kvantorernas motsvarighet till De Morgans lagar.
Ett existenspåstående fastställs genom att visa ett vittne. ∃x φ är ekvivalent med ¬∀x ¬φ, så vardera kvantorn kan definieras utifrån den andra tillsammans med negationen.
Logik utvidgad med ”nödvändigtvis” (□) och ”möjligen” (◇).
Modallogiken utvärderar formler i möjliga världar i stället för i en enda tolkning: □φ håller när φ håller i varje åtkomlig värld, ◇φ när den håller i någon. Att variera vad ”åtkomlig” betyder ger de olika modalsystemen.