Hoppa till innehÄllet

Predikatlogik

FrÄn Wikipedia
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 , om och Àr satser), kan man i predikatlogiken resonera om företeelser och deras egenskaper. För att uttrycka A och B, kan man i predikatlogiken anvÀnda predikat. Exempelvis kan representera Àr udda sÄ att betyder Àr udda. Man kan ocksÄ bilda flerstÀlliga relationer , 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 , 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.

  • innebĂ€r att alla har egenskapen .
  • innebĂ€r att nĂ„got har egenskapen .

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: . 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 , 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.

Viktiga definitioner

[redigera | redigera wikitext]

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, det vill sÀga alla variabler Àr termer,
  2. c1, c2, 
 Àr termer, det vill sÀga 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

[redigera | redigera wikitext]

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)

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 ∀ och ∃

[redigera | redigera wikitext]

Vi kan skriva ”ingen forskare Ă€lskar Anna” som:

(Det finns inte nÄgot x, sÄdant att x har egenskapen Q och x relaterar till 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:

PÄ detta sÀtt kan vi visa att:

Vilket vi kan utveckla till:

PÄ detta sÀtt har vi sÄledes upptÀckt att:

Formalisering

[redigera | redigera wikitext]

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.

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

  • Satstyp A: "Alla svanar Ă€r vackra".
  • Satstyp E: "Inga svanar Ă€r vackra".
  • Satstyp I: "NĂ„gra svanar Ă€r vackra".
  • Satstyp O: "NĂ„gra svanar Ă€r inte vackra".

Satstyperna A och O Àr kontradiktoriska och det Àr Àven satstyperna I och E. De kan inte bÄda vara sanna och ej heller bÄda vara falska.

Satstyperna A och E Àr kontrÀra. De kan inte bÄda vara sanna, men bÄda vara falska.

Satstyperna I och O Àr subkontrÀra. De kan bÄda vara sanna, men inte bÄda vara falska.

AnvÀndningsomrÄden

[redigera | redigera wikitext]

Nedan nÀmns ett par omrÄden dÀr predikatlogiken anvÀnds.

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

[redigera | redigera wikitext]

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

[redigera | redigera wikitext]

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]

  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

Vidare lÀsning

[redigera | redigera wikitext]
  • Barwise, Jon & Etchemendy, John, Language, proof and logic (1999)
  • Geoffrey Hunter, Metalogic, MacMillan 1971.