Førsteordens logikk

Turlaget vil ha en regel: alle medlemmer som har gått en lang tur, får et merke. I utsagnslogikk trenger du én regel per medlem og ett symbol for hvert par av medlem og tur, som GikkAneGausta og GikkBoGausta og så videre. Med 200 medlemmer blir det 200 regler som sier det samme. Utsagnslogikk kan ikke si «alle» eller «noen», og den ser ikke at de to symbolene handler om samme tur.

Førsteordens logikk (first-order logic, FOL) løser det ved å endre hva språket sier at verden består av. Det kalles en ontologisk forpliktelse (ontological commitment): FOL antar at verden har objekter, relasjoner mellom dem og funksjoner. Et objekt (object) kan være Ane eller Gausta. «Gikk» er en relasjon mellom en person og en tur, «er medlem» en egenskap, altså en relasjon med ett argument, og «guiden på» en funksjon som gir én person for hver tur. Regelen blir én setning:

Språket er deklarativt: du skriver hva som er sant, ikke hvordan det skal regnes ut, og den samme kunnskapsbasen kan svare på spørsmål ingen tenkte på da den ble skrevet. Det er også komposisjonelt: betydningen av en setning følger av betydningen av delene. Begge egenskapene har FOL felles med utsagnslogikk, men nå kan delene være objekter.

Hva agenten kan tro om en setning, er det samme som før: den er sann eller usann, og agenten kan vite det eller ikke. Sannsynlighetsteori endrer det, og andre logikker legger til tid eller hendelser som egne ting, men det er utenfor dette kapitlet.

Setninger i FOL bygges av tre slags symboler. Et konstantsymbol (constant symbol) navngir ett objekt: $\text{Ane}$, $\text{Gausta}$. Et predikat (predicate symbol) står for en relasjon og gir en setning: $\text{Medlem}(\text{Ane})$, $\text{Gikk}(\text{Ane},\text{Gausta})$. Et funksjonssymbol (function symbol) gir et objekt: $\text{Guide}(\text{Gausta})$ er personen som guidet Gausta-turen. Navn skrives med stor forbokstav og variabler med liten.

Det viktigste skillet går mellom termer og setninger. En term peker på et objekt: en konstant, en variabel eller en funksjon brukt på termer. En atomær setning (atomic sentence) er et predikat brukt på termer, eller en likhet mellom to termer, og den er sann eller usann. $\text{Guide}(\text{Gausta})$ er en term, mens $\text{Leder}(\text{Guide}(\text{Gausta}))$ er en setning. En setning kan aldri stå som argument.

Hvert symbol har et fast antall argumenter. $\text{Gikk}$ tar alltid to, først personen og så turen, og en funksjon gir alltid nøyaktig ett objekt. $\text{Guide}(t)$ forutsetter derfor at hver tur har én guide. Har en tur ingen eller flere guider, er en relasjon $\text{Guidet}(x,t)$ et bedre valg.

Om en setning er sann, avgjøres av en modell og en tolkning (interpretation). Modellen har en mengde objekter, og tolkningen sier hvilket objekt hver konstant peker på, hvilke tupler hver relasjon holder for og hva hver funksjon gir. Tabellen viser en liten modell for turlaget.

I denne modellen er $\text{Gikk}(\text{Guide}(\text{Byrunden}),\text{Byrunden})$ sann: $\text{Guide}(\text{Byrunden})$ er Cato, og $(\text{Cato},\text{Byrunden})$ står i $\text{Gikk}$. Sammensatte setninger bygges med de samme konnektivene som før, så $\text{Leder}(\text{Bo})\vee \text{Medlem}(\text{Bo})$ er sann fordi Bo er medlem.

En KB i FOL har vanligvis svært mange modeller: antall objekter er ikke fast, og det kan være uendelig mange. Derfor kan du ikke avgjøre logisk konsekvens ved å gå gjennom alle modellene, slik sannhetstabellen gjorde i utsagnslogikk. Kapittel 14 viser hvordan inferensreglene løftes til FOL i stedet.

En universell kvantor (universal quantifier), $\forall x$, sier at setningen etter er sann for hvert objekt $x$ kan stå for. En eksistensiell kvantor (existential quantifier), $\exists x$, sier at den er sann for minst ett. Kvantoren binder variabelen, og en setning uten frie variabler er sann eller usann i en modell.

Kvantorene går over alle objektene i modellen, også dem du ikke tenker på. Derfor hører $\forall$ sammen med $\Rightarrow$, som i ƒmønsteret «alle P er Q», og $\exists$ med $\wedge$, som i ƒmønsteret «noen P er Q»:

Den første sier noe bare om medlemmene: for et objekt som ikke er medlem, er implikasjonen sann uansett. Skriver du $\forall x(\text{Medlem}(x)\wedge \text{Betalt}(x))$, sier du at alt er et medlem som har betalt, også Gausta-turen. Skriver du $\exists x(\text{Medlem}(x)\Rightarrow \text{Leder}(x))$, blir setningen sann så snart ett objekt ikke er medlem, og det er nesten alltid tilfelle.

I en endelig modell kan du tenke på $\forall$ som en lang konjunksjon og $\exists$ som en lang disjunksjon. Med objektene Ane, Bo og Gausta er $\forall x\text{Medlem}(x)$ det samme som $\text{Medlem}(\text{Ane})\wedge \text{Medlem}(\text{Bo})\wedge \text{Medlem}(\text{Gausta})$, og $\exists x\text{Medlem}(x)$ det samme med $\vee$. Det forklarer også dualiteten i neste steg: De Morgan bytter $\wedge$ og $\vee$, og derfor bytter negasjonen $\forall$ og $\exists$.

Tabellen viser de fire mønstrene du oftest skal formalisere, med den vanlige feilen ved siden av.

«Ingen P er Q» og «ikke alle P er Q» ligner hverandre på norsk, men er forskjellige. Den første sier at ingen P er Q, den andre bare at minst én P ikke er det.

Med flere kvantorer avgjør rekkefølgen betydningen, og da snakker vi om nøstede kvantorer (nested quantifiers). Like kvantorer kan bytte plass: $\forall x\forall y$ er det samme som $\forall y\forall x$. En $\forall$ og en $\exists$ kan generelt ikke:

Den første sier at alle kjenner noen, og hver kan kjenne en ny. Den andre sier at det finnes én person som alle kjenner. Den andre medfører den første, men ikke omvendt. Tabellen viser en modell der alle kjenner noen, uten at noen kjennes av alle.

Les nøstede kvantorer fra venstre, som et spill: ved $\forall$ velger motstanderen et objekt, ved $\exists$ velger du. I $\forall x\exists y$ får du se $x$ før du velger $y$, mens du i $\exists y\forall x$ må velge $y$ først.

import random

antall_personer = 4  # @param 2..6
seed = 3  # @param 0..20

random.seed(seed)
personer = ["Ane", "Bo", "Cato", "Dina", "Eli", "Frid"][:antall_personer]
# En modell er bare en tabell: hvert par (x, y) er med eller ikke, også (x, x).
kjenner = {(x, y) for x in personer for y in personer if random.random() < 0.45}

alle_kjenner_noen = all(any((x, y) in kjenner for y in personer) for x in personer)
noen_kjent_av_alle = any(all((x, y) in kjenner for x in personer) for y in personer)

print(f"Par i Kjenner: {len(kjenner)} av {len(personer) ** 2}")
print(f"∀x ∃y Kjenner(x, y): {'sann' if alle_kjenner_noen else 'usann'}")
print(f"∃y ∀x Kjenner(x, y): {'sann' if noen_kjent_av_alle else 'usann'}")
if not alle_kjenner_noen:
    x = next(x for x in personer if not any((x, y) in kjenner for y in personer))
    print(f"Moteksempel: {x} kjenner ingen, så ∀x ∃y faller")
elif not noen_kjent_av_alle:
    mangler = [f"{y} (ikke av {next(x for x in sorted(personer, key=lambda x: x == y) if (x, y) not in kjenner)})" for y in personer]
    print(f"Moteksempel: ingen kjennes av alle: {', '.join(mangler)}")
else:
    y = next(y for y in personer if all((x, y) in kjenner for x in personer))
    print(f"Moteksempel: ingen; alle kjenner {y}, så begge er sanne")

Negasjon flyttes forbi en kvantor ved å bytte den, etter ƒdualiteten mellom kvantorene:

«Ikke alle er med» er det samme som «noen er ikke med», og «ingen er med» det samme som «for hver x: x er ikke med». Pass på hvor langt en kvantor rekker: den gjelder så langt til høyre som mulig. $\forall x\text{Medlem}(x)\Rightarrow \text{Betalt}(x)$ leses som $\forall x(\text{Medlem}(x)\Rightarrow \text{Betalt}(x))$, så skriv parenteser når du mener noe annet, som $(\forall x\text{Medlem}(x))\Rightarrow \text{Betalt}(\text{Ane})$. Inne i parentesen gjelder reglene fra utsagnslogikk: $\neg (A\Rightarrow B)$ blir $A\wedge \neg B$, og De Morgan bytter $\wedge$ og $\vee$.

Symbolet for likhet (equality) er $=$, og $t_1=t_2$ er sann når de to termene peker på samme objekt. Det trengs fordi to variabler, og to konstanter, kan peke på det samme. En formel for minst to ledere (ƒminst to) er derfor

og uten $\neg (x=y)$ er formelen sann med én leder, satt inn for både $x$ og $y$. Formelen for nøyaktig én leder (ƒnøyaktig én) sier at det finnes en leder, og at enhver leder er den samme:

Vanlig førsteordens logikk er forsiktig. Står $\text{Medlem}(\text{Ane})$ og $\text{Medlem}(\text{Bo})$ i KB, vet du ikke at Ane og Bo er to personer, og du vet ikke om det finnes flere medlemmer. Databaser og logikkprogrammer bruker en strengere databasesemantikk med tre antagelser:

• •Med antagelsen om unike navn (unique-names assumption) peker ulike konstanter på ulike objekter.
• •Med antagelsen om lukket verden (closed-world assumption) er det som ikke står i KB og ikke følger av den, usant.
• •Med domenelukning (domain closure) finnes det ingen andre objekter enn dem konstantene navngir.

Med alle tre har KB-en over nøyaktig to medlemmer, og en tabell blir lest slik du er vant til fra databaser. Uten dem må du skrive de samme opplysningene med likhet og kvantorer.

Å formalisere er å oversette norsk til FOL, og det går i to trinn: først vokabularet, så setningene. Vokabularet er predikatene, funksjonene og konstantene du trenger, med betydningen og hvilken plass hvert argument har. $\text{Gikk}(x,t)$ må bety «person $x$ gikk tur $t$» hver gang, ikke av og til omvendt.

Å bygge en hel kunnskapsbase for et domene heter kunnskapsingeniørarbeid (knowledge engineering). Figuren viser de sju stegene for turlagets nøkkelsystem for hyttene.

Vokabularet er ontologien for domenet, og det styrer resten. Skal en hytte være en konstant ($\text{Lia}$) eller et predikat ($\text{ErLia}(h)$)? Skal «har betalt» være et predikat eller en funksjon som gir beløpet? Velg slik at reglene blir korte og generelle: én regel om alle medlemmer er bedre enn én per medlem. Hold de generelle reglene og forekomsten adskilt, så samme regler kan brukes med nye fakta. Skriv også ned spørsmålene KB-en skal svare på før du begynner, så du vet når den er god nok. Når et spørsmål gir feil svar, ligger feilen oftest i en regel som mangler eller er for svak, ikke i inferensen.

To feil går igjen i vokabularer. Den første er å bruke samme predikat med ulikt antall argumenter, som $\text{Gikk}(x)$ ett sted og $\text{Gikk}(x,t)$ et annet. Den andre er å gjøre en egenskap til en konstant, som Ane_Medlem, slik at du ikke kan kvantifisere over den. Spør deg selv for hvert symbol: er det et objekt, en egenskap eller en relasjon, og hvilke objekter tar det?