Predikatlogik

Från Rilpedia

Hoppa till: navigering, sök
Wikipedia_letter_w.pngTexten från svenska WikipediaWikipedialogo_12pt.gif
rpsv.header.diskuteraikon2.gif
Logik, Formellt system
Logiska system

Predikatlogik är en del av den matematiska logiken. Medan man i satslogiken bara kan sätta samman färdiga satser till mer komplicerade satser, exempelvis bilda A\land B, om A och B är satser, för att uttrycka A och B, kan man i predikatlogiken använda predikat. Exempelvis kan P representera är udda så att P(x) betyder x är udda. Man kan också bilda flerställiga relationer P(x,y), exempelvis för att representera relationen större än. I mängdteori kan hela matematiken formuleras med hjälp av predikatlogik med en enda relation \in, som uttrycker att en mängd är element i en annan. Samma logiska operationer som finns i satslogiken finns även i predikatlogiken. Dessutom finns all- och existens-kvantorer som uttrycker att något gäller för alla respektive för något objekt.

  • \forall xP(x) innebär att alla x har egenskapen P.
  • \exists xP(x) innebär att något x har egenskapen P.

Antag att vi vill uttala oss om att om någonting har två specifika egenskaper, så har det den andra av dessa egenskaper. Vi kan symbolisera det på följande sätt: \forall x((P(x) \land Q(x))\rightarrow Q(x)). Det läses: för varje x gäller, att om x har egenskapen P, och x har egenskapen Q, så har x egenskapen Q.

Ett annat exempel är \forall x\forall y ((x=y)\rightarrow(P(x)\leftrightarrow P(y))), som säger: för alla x gäller, att för alla y gäller, att om x är lika med y, så har x egenskapen P, om och endast om y har egenskapen P. Vad detta betyder är egentligen att om x och y betecknar samma föremål, så är egenskaperna för x och y lika.

Att man kan formulera predikatlogiken så att den blir fullständig bevisades av Kurt Gödel i hans doktorsavhandling.

Innehåll

Viktiga definitioner

De nedanstående definitionerna är väsentliga då övriga definitioner och bevis utgår från dem. Vidare används de också för att undersöka om en formel är välbildad eller inte.

Definition 1: Definition av term.

  1. x1, x2, … är termer, dvs alla variabler är termer,
  2. c1, c2, … är termer, dvs alla konstanter är termer,
  3. Om f är en n-ställig funktionssymbol och, t1, t2, … , tn är termer, så är f(t1, t2, … , tn) en term.

Definition 2: Definition av atomär formel.

  1. Om t1 och t2 är två termer, så är t1 = t2 en atomär formel,
  2. Om P är en n-ställig predikatsymbol, och t1, t2, … , tn är termer, så är P(t1, t2, … , tn) en atomär formel.
  3. ⊥ är en atomär formel.

Definition 3: Definition av välbildad formel (vbf).

  1. Alla atomära formler är välbildade formler,
  2. Om ϕ är en välbildad formel, så är ¬ϕ en välbildad formel,
  3. Om ϕ och ψ är välbildade formler, så är (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ) och (ϕ ↔ ψ) välbildade formler,
  4. Om ϕ är en välbildad formel och v en variabel, så är ∃vϕ och vϕ välbildade formler.

[1]

Objekt, egenskaper och relationer

Inom predikatlogik går det att dra slutsatser om objekt, egenskaper samt relationer vilket är den stora skillnaden i jämförelse med satslogiken.
Ett exempel på detta är:

John är en poet
Anna är en forskare
John är gift med Anna
Någon poet är gift med någon forskare

Vilket kan tolkas som, där a är objektet John, b är objektet Anna, P är en egenskap, Q är en annan egenskap och R ett förhållande:

a är P
b är Q
a är R till b
Något P är R till något Q

Vilket vi kan skriva som:

P(a)
Q(b)
R(a, b)
\exists a(P(a)\land \exists b(Q(b) \land R(a,b)))

vilket skulle utläsas som: Det finns ett a sådant att a är en poet och det finns ett b sådant att b är en forskare och a är gift med b

Förhållandet emellan kvantifikatorerna  \forall och  \exists

Vi kan skriva ”ingen forskare älskar Anna” som:

\neg \ \exists x(Q(x)\ \land \ R(x,b)) (Det finns inte något x, sådant att x är Q och Rx, b)

Att säga att det inte finns någon forskare som har en viss egenskap skulle vi lika gärna kunna formulera som att alla forskare istället saknar den egenskapen och på det viset kan vi då även skriva:

 \forall x(Q(x)\ \rightarrow \ \neg \ R(x,b))

På detta sättet kan vi visa att:

 \neg \ \exists x\ \leftrightarrow \ \forall x\ \neg \

Vilket vi kan utveckla till:

 \neg \ \neg \ \exists x\ \leftrightarrow \ \neg \ \forall x\ \neg \ \rightarrow \ \exists x\ \leftrightarrow \ \neg \ \forall x\ \neg \

På detta sätt har vi således upptäckt att:

 \neg \ \exists x(Q(x) \ \wedge \ R(x,b)) \leftrightarrow \
 \forall x \ \neg \ (Q(x) \wedge \ R(x, b)) \leftrightarrow \
\forall x(Q(x) \rightarrow \ \neg \ R(x,b))

Formalisering

Det är viktigt att när man försöker formalisera en språklig sats i predikatlogik att noggrant visa den logiska strukturen som existerar i den språkliga satsen. För att klara detta används två generella tekniker som kallas för bottom up och top down> (engelska för ”nerifrån upp” och ”uppifrån ner”).

  • Bottom Up: Med denna strategi lokaliserar man istället de atomära formlerna (se ovan) som bygger upp satsen och på det viset kan se satsens logiska struktur.
  • Top down: Med denna strategi är tanken att först leta reda på huvudoperatorn i en språklig sats för att på detta viset urskilja vilka delsatser som verkar på huvudoperatorn. Detta upprepas sedan på delsatserna.

Generellt är det en god idé att blanda de olika strategierna genom att börja med top down för att urskilja de atomära formlerna för att sedan använda bottom up.

Satstyper

Med verktygen presenterade ovan kan man urskilja fyra typer av satser som går att formalisera med hjälp av predikatlogik.

  • Satstyp 1, även känd som satstyp A: "Alla läkare är onda".
  • Satstyp 2, även känd som satstyp I: "Några läkare är onda".
  • Satstyp 3, även känd som satstyp E: "Några läkare är inte onda".
  • Satstyp 4, även känd som satstyp O: "Inga läkare är onda".

Ett par viktiga notiser här är att satstyp A och O är motsatser och kallas för konträr vilket innebär att båda kan vara falska, men båda kan inte vara sanna. Satstyperna I och E har en liknande relation; det kallas för subkonträr då båda kan vara sanna men båda kan inte vara falska.

Användningsområden

Nedan nämns ett par områden där predikatlogiken används.

Elektronik

För enklare kretsteknologi är satslogiken tillräcklig då den utgör grunden för den booleska algebran men inom högre nivåer av elektronik blir predikatlogik enormt viktigt då den tillåter skapandet av mera avancerade former av kretsar, mera specifikt inom området som på engelska heter ”Switching Theory” där logiskt sant representeras av 1 emedan logiskt falskt representeras av 0 [2]

Logisk programmering

I vanlig programmering är uppgiften för programmering att tolka en given specifikation, som detaljerat förklarar vad ett program ska göra, till kod som förklarar hur resultaten ska uppnås. Ett program är således instruktioner till en dator som ska generera resultatet som angivits i specifikationen.

Logisk programmering skiljer sig från detta i att istället för att instruera datorn vad den ska åstadkomma så kommer programmeraren att skapa en databas med olika påståenden och regler gällande dessa. Efter detta ställer programmeraren en direkt fråga till datorn och datorn genererar ett svar utefter logisk manipulation av det som är angivet i databasen. I bästa fall behöver logisk programmering inga instruktioner utan enbart fakta.

Idag är det mest använda programmeringsspråket för denna typ av programmering Prolog, dock är Prolog mycket omdebatterat då det gör så pass stora kompromisser i form av imperativ programmering att frågan är huruvida det är ett logiskt programmeringsspråk överhuvudtaget [3]

Artificiell intelligens

Många forskare inom området tror att en av de viktigaste delarna av mänskligt medvetande är logiskt resonemang och menar att formell logik kan stå för en av grundpelarna i skapandet av artificiell intelligens. Även detta är omdebatterat och en del forskare menar att inställningen till logiken som centrum för artificiell intelligens istället har begränsat utvecklingen snarare än att främja den. [4]

Se även

Litteratur

  • Barwise, Jon & Etchemendy, John, Language, proof and logic (1999)
  1. Sjögren, J: "Introduktion till predikatlogik", sidan 56, 2002
  2. Vingron, S.P: "Switching Theory - Insight through predicate logic", förord, 2004
  3. Galton, A: "Logic for Information Technology", sidan 3. 1990
  4. Galton, A: "Logic for Information Technology", sidan 4. 1990
Personliga verktyg