Alle begrepene kalkulatoren, guidene og øvelsene bruker, definert på ett sted.
Slå opp et begrep, se notasjonen, og åpne eksempelet i kalkulatoren for å se det i arbeid. Begreper herfra uthevet første gang de dukker opp i en guide.
Alle 62 begreper
Grunnbegreper
logikk
Studiet av hvilke konklusjoner som faktisk følger av hvilke antakelser.
Logikk studerer resonnementets form heller enn innholdet. Formell logikk erstatter setninger med symboler, slik at spørsmålet om en konklusjon følger kan avgjøres av argumentets form alene og kontrolleres mekanisk.
En påstand som er enten sann eller usann, men ikke begge deler.
Et utsagn er en fortellende setning med nøyaktig én sannhetsverdi. «Det regner» er et utsagn; et spørsmål eller en ordre er det ikke, for det finnes ikke noe ved dem som kan være sant eller usant.
En av de to verdiene et utsagn kan ha: sann eller usann.
Klassisk logikk gir hvert utsagn nøyaktig én av to sannhetsverdier, skrevet ⊤ og ⊥ (eller 1 og 0). Hver rad i en sannhetstabell er én tildeling av verdier til variablene, med verdien formelen får der.
Et atomært utsagn kan ikke deles i mindre utsagn: det inneholder verken negasjon, konjunksjon eller andre konnektiver. Alt annet er sammensatt, bygget av atomer, og sannhetsverdien følger av deres.
En bokstav som p eller A som står for et vilkårlig utsagn.
En utsagnsvariabel er en plassholder for hvilket som helst utsagn. Kalkulatoren tar enkeltbokstaver som variabler og gir hver av dem en kolonne i sannhetstabellen, med én rad for hver mulige kombinasjon av verdier.
En rekke symboler som språkets grammatikk faktisk tillater.
En velformet formel bygges etter reglene: en variabel er én, og det samme er enhver formel dannet av mindre formler ved et konnektiv. «p ∧ ∨ q» er det ikke, og derfor melder kalkulatoren en feil i stedet for å gjette.
Én tildeling av sannhetsverdier til alle variabler i en formel.
En tolkning sier hva hver variabel er verdt, og fastsetter dermed verdien til hele formelen. En formel med n variabler har 2ⁿ tolkninger – nøyaktig radene i sannhetstabellen.
Premisser som føres fram til støtte for en konklusjon.
Et argument hevder at konklusjonen følger av premissene. Skriv et inn i kalkulatoren med et følgetegn – premisser før, konklusjon etter – og hver rad blir sjekket for et tilfelle der premissene holder og konklusjonen svikter.
En påstand et argument antar for å nå konklusjonen.
Premissene er argumentets utgangspunkt. Gyldighet spør bare om konklusjonen holder overalt der alle premissene holder; om de faktisk er sanne er et annet spørsmål – det holdbarhet legger til.
Konklusjonen er det premissene skal støtte. I kalkulatoren er den uttrykket etter følgetegnet, og et argument er gyldig når ingen tolkning gjør premissene sanne og konklusjonen usann.
Et symbol som bygger et sammensatt utsagn av enklere utsagn.
Et konnektiv som ¬, ∧, ∨, → eller ↔ forbinder utsagn til et større hvis sannhetsverdi bare avhenger av deres. Nettopp den avhengigheten registrerer en sannhetstabell, én rad per kombinasjon av inndata.
Snur en sannhetsverdi: ¬p er sann nettopp når p er usann.
Negasjonen er utsagnslogikkens eneste énplassige konnektiv. Skrevet ¬p, ~p eller !p gjør den sant til usant og usant til sant, slik at to negasjoner gir tilbake det opprinnelige utsagnet.
En konjunksjon hevder begge delene sine, konjunktene. Den er sann i nøyaktig én rad av sannhetstabellen – den der begge konjunktene er sanne – og er dermed det strengeste av de toplassige konnektivene.
Disjunksjonen er i logikken inklusiv: p ∨ q er sann når p er sann, når q er sann og når begge er det. Den eksklusive lesningen av «eller», sann bare når delene er forskjellige, er et eget konnektiv.
Eksklusiv disjunksjon, skrevet ⊕ eller XOR, holder når delene er forskjellige og svikter når de stemmer overens. Den er negasjonen av bikondisjonalen og kan skrives som (p ∨ q) ∧ ¬(p ∧ q).
Den materielle kondisjonalen sier ikke annet enn «ikke: forledd sant og etterledd usant», og holder derfor automatisk så snart forleddet svikter. Derfor er p → q ekvivalent med ¬p ∨ q.
p ↔ q, sann når begge delene har samme sannhetsverdi.
Bikondisjonalen hevder hver side under betingelse av den andre: den er sann når begge delene er sanne og når begge er usanne. En bikondisjonal som er en tautologi uttrykker nettopp en logisk ekvivalens.
Forleddet er betingelsen en kondisjonal avhenger av. Når det er usant, er hele kondisjonalen sann uansett etterledd, og derfra kommer de fleste overraskelsene i tabellen for →.
Etterleddet er det en kondisjonal hevder følger dersom forleddet holder. Et sant etterledd gjør kondisjonalen sann, men gjør ikke forleddet sant: å slutte det er en formell feilslutning.
Den omvendte av p → q er q → p, og de to er ikke ekvivalente: kalkulatoren finner en rad der den ene holder og den andre svikter. Å behandle dem som utbyttbare er å bekrefte etterleddet.
¬q → ¬p, som alltid har samme sannhetsverdi som p → q.
Kontraposisjonen negerer begge delene av en kondisjonal og bytter om på dem. I motsetning til den omvendte er den virkelig ekvivalent med originalen, og derfor er bevis ved kontraposisjon gyldig i matematikken.
Negasjonen av en konjunksjon: sann med mindre begge inngangene er sanne.
NAND, skrevet ↑, er ¬(p ∧ q). Den er funksjonelt fullstendig: ethvert annet konnektiv kan bygges av NAND alene, og derfor er den en arbeidshest i digital kretsdesign.
Hvilket konnektiv som binder først når parentesene mangler.
Negasjonen binder sterkest, så konjunksjon, disjunksjon, kondisjonal og til slutt bikondisjonal. Slik leses ¬p ∧ q ∨ r som ((¬p) ∧ q) ∨ r; parenteser overstyrer rekkefølgen når den tiltenkte lesningen er en annen.
Én rad per verditildeling, med formelens verdi i hver.
En sannhetstabell lister opp alle 2ⁿ tolkninger av en formels n variabler og regner ut verdien i hver. Fordi den er uttømmende, avgjør den ethvert semantisk spørsmål i utsagnslogikken: ekvivalens, gyldighet, oppfyllbarhet og resten.
En tautologi er sann i hver rad av sannhetstabellen og sier derfor ingenting om verden: p ∨ ¬p er sann uansett hva p er. To formler er ekvivalente nettopp når bikondisjonalen mellom dem er en tautologi.
En motsigelse som p ∧ ¬p er usann i hver rad av sannhetstabellen. Å utlede en av et sett antakelser viser at antakelsene ikke alle kan holde – motoren i motsigelsesbeviset.
En formel som er sann under noen tolkninger og usann under andre.
En kontingent formel er verken tautologi eller motsigelse: sannhetstabellen har minst én sann og minst én usann rad. De fleste formler noen skriver er kontingente, og nettopp det gjør dem informative.
En formel er oppfyllbar når minst én rad i sannhetstabellen er sann, og den raden er en modell av den. Å avgjøre oppfyllbarhet er SAT-løsernes sentrale problem og dermed en stor del av automatisk resonnering.
Ekvivalente formler stemmer overens under enhver tolkning, så den ene kan erstatte den andre overalt uten å endre innholdet. Sett et likhetstegn mellom to uttrykk, så sammenligner kalkulatoren kolonnene rad for rad.
Konklusjonen holder i enhver tolkning der premissene holder.
Skrevet Γ ⊨ φ er logisk følge det et gyldig argument gjør krav på. Den kontrolleres ved å lete etter et moteksempel: en tolkning som gjør alle premissene sanne og konklusjonen usann. Finnes ingen, holder følgen.
Ingen tolkning gjør premissene sanne og konklusjonen usann.
Gyldighet er en egenskap ved argumentets form, ikke ved fakta: et gyldig argument kan ha usanne premisser og en usann konklusjon. Det det ikke kan ha, er sanne premisser sammen med en usann konklusjon.
Et gyldig argument der premissene i tillegg er sanne.
Holdbarhet legger en faktisk påstand til en formell: argumentet er gyldig, og premissene holder. Logikken alene avgjør den første halvdelen; den andre hører til det argumentet handler om.
En tolkning som gjør premissene sanne og konklusjonen usann.
En motmodell beviser at et argument er ugyldig – én rad er nok. Kalkulatoren viser raden den finner, og gjør dermed «dette følger ikke» til en konkret tildeling du kan sjekke for hånd.
Noen tolkning gjør alle utsagnene i mengden sanne samtidig.
En mengde premisser er konsistent når de alle kan holde sammen. Inkonsistente premisser medfører hva som helst, så et argument bygget på dem er teknisk gyldig og verdt ingenting.
En variabel eller negasjonen av den, som p eller ¬p.
Literalene er normalformenes atomer: en klausul er en disjunksjon av literaler, og en minterm er en konjunksjon av dem. En literal er positiv når variabelen står bar og negativ når den er negert.
En klausul er en av parentesgruppene en konjunktiv normalform består av. Siden en konjunksjon bare er sann når hver del er det, holder en KNF-formel nettopp når alle klausulene holder.
Et ELLER av OG-er: en disjunksjon av konjunksjoner av literaler.
Enhver formel har en disjunktiv normalform, og den kan leses rett ut av sannhetstabellen: én konjunksjon per sann rad, forbundet med ∨. Kalkulatoren gir også en minimert DNF, som sier det samme med færre literaler.
Konjunktiv normalform leses ut av de usanne radene i sannhetstabellen, én klausul per rad. Det er inndataformatet SAT-løsere forventer, noe som gjør omskriving til KNF til et rutinesteg i automatisk resonnering.
En konjunksjon som peker ut nøyaktig én rad i sannhetstabellen.
En minterm nevner hver variabel én gang, negert eller ikke, slik at nøyaktig én tolkning oppfyller den. Å samle mintermene til de sanne radene og forbinde dem med ∨ gir formelens disjunktive normalform.
En disjunksjon som utelukker nøyaktig én rad i sannhetstabellen.
En maksterm nevner hver variabel én gang og er usann i én eneste tolkning. Å ta makstermen for hver usann rad og forbinde dem med ∧ gir formelens konjunktive normalform.
Negasjon gjør ∧ til ∨ og ∨ til ∧: ¬(p ∧ q) ≡ ¬p ∨ ¬q.
De Morgans lover skyver en negasjon innover over en konjunksjon eller disjunksjon og vender konnektivet underveis. Slik drives en formel mot en normalform, og slik forenkles negasjoner i kode og i kretser.
Dobbeltnegasjonen gjelder i klassisk logikk begge veier, så ¬¬p og p kan alltid byttes om. Intuisjonistisk logikk beholder bare retningen fra p til ¬¬p, og der skilles de to systemene.
Algebraen med to verdier og ∧, ∨ og ¬ som operasjoner.
Boolsk algebra er utsagnslogikk skrevet som regning med 0 og 1, med lover – kommutativitet, distributivitet, absorpsjon, De Morgan – som lar uttrykk skrives om og forenkles. Det er matematikken digitale kretser konstrueres i.
Et rutenett over sannhetstabellen som gjør forenklinger synlige.
Et Karnaugh-diagram ordner radene slik at naboruter skiller seg i én variabel, og kantene henger sammen. Det skrives også K-diagram, K-map eller kmap. Rektangulære grupper av naboliggende enere av størrelse 1, 2, 4 eller 8 leses da direkte som ledd i et minimalt uttrykk.
En gruppe i diagrammet som ikke kan gjøres større.
En implikant er en konjunksjon av literaler som tvinger formelen til å være sann; den er prim når fjerning av en hvilken som helst literal ville ødelegge det. I et Karnaugh-diagram er primimplikantene de maksimale rektanglene av enere.
Den eneste primimplikanten som dekker en bestemt ener.
Når en ener i diagrammet hører til bare én maksimal gruppe, må den gruppen inngå i enhver minimal dekning og tas derfor først. Det som blir igjen, er den delen av dekningen som virkelig må søkes.
Et kretselement som beregner ett konnektiv på inngangene sine.
AND-, OR-, NOT-, NAND-, NOR- og XOR-porter er konnektivenes motstykke i maskinvare. En formel og en krets er den samme gjenstanden tegnet to ganger, og derfor kan kalkulatoren vise et uttrykk som et portdiagram.
Et tillatt steg fra allerede utledede formler til en ny.
En slutningsregel er et mønster som modus ponens, som kan brukes så snart formler av rett form finnes. Bevissystemer bygges av en håndfull av dem, valgt slik at bare konklusjoner som følger kan utledes.
Modus ponens er kondisjonalens grunnregel: gitt en kondisjonal og forleddet dens følger etterleddet. Gyldigheten ses i sannhetstabellen – den eneste raden med begge premissene sanne har også konklusjonen sann.
Modus tollens går baklengs gjennom en kondisjonal: svikter etterleddet, kan forleddet ikke ha holdt. Det er kontraposisjonen i arbeid og formen på ethvert argument som gjendriver en hypotese ved å prøve dens forutsigelser.
Den hypotetiske syllogismen kjeder sammen kondisjonaler, og det er det som gjør lange utledninger mulige: hvert ledd fører argumentet ett skritt videre uten at noen premiss blir hevdet.
Den disjunktive syllogismen stryker det utelukkede alternativet: holder ett av to alternativer og det første ikke gjør det, må det andre gjøre det. Det er regelen bak utelukkelsesresonnement.
Å bevise en konklusjon ved å bruke slutningsregler steg for steg.
Naturlig deduksjon utleder en konklusjon av premisser med introduksjons- og elimineringsregler for hvert konnektiv, og tillater midlertidige antakelser som senere avvikles. Den beviser det en sannhetstabell kontrollerer, uten å gå gjennom hver rad.
Anta det motsatte, utled en motsigelse, slutt det opprinnelige.
For å bevise φ antar man ¬φ og utleder noe av formen ψ ∧ ¬ψ. Siden ingen tolkning gjør en motsigelse sann, kan antakelsen ikke holde, og φ følger. Slik går bevis for irrasjonalitet og uendelighet vanligvis fram.
Et sant etterledd godtgjør ikke forleddet: noe annet kan ha frambrakt det. Kalkulatoren viser motmodellen – p usann, q sann – som er raden som skiller dette fra modus ponens.
En kondisjonal sier ingenting om hva som skjer når forleddet svikter, så å utelukke forleddet lar etterleddet stå åpent. Motmodellen er raden der p er usann og q sann.
Logikk som ser inn i utsagn, på gjenstander og egenskapene deres.
Predikatlogikken legger til predikater, termer og kvantorer, slik at «ethvert primtall større enn to er oddetall» blir en formel og ikke én enkelt bokstav. Den er strengt mer uttrykkskraftig enn utsagnslogikken, og ingen sannhetstabell kan avgjøre den.
Et symbol som sier hvor mange gjenstander et predikat gjelder for.
De to klassiske kvantorene er ∀ (alle) og ∃ (minst én), og hver er negasjonen av den andre med negert kropp. Variabelen en kvantor binder, er det som skiller predikatlogikk fra utsagnslogikk.
En universell påstand gjendrives av ett eneste moteksempel og holder tomt over et tomt domene. ∀x φ er ekvivalent med ¬∃x ¬φ, kvantorenes motstykke til De Morgans lover.
En eksistenspåstand godtgjøres ved å vise fram ett vitne. ∃x φ er ekvivalent med ¬∀x ¬φ, så hver kvantor kan defineres ut fra den andre sammen med negasjonen.
Logikk utvidet med «nødvendigvis» (□) og «mulig» (◇).
Modallogikken vurderer formler i mulige verdener i stedet for i én tolkning: □φ holder når φ holder i enhver tilgjengelig verden, ◇φ når den holder i minst én. Å variere hva «tilgjengelig» betyr gir de ulike modalsystemene.