Satslogik

Från Wikipedia
Hoppa till: navigering, sök
Logik, Formellt system
Logiska system
Deduction symbols2.gif
Satslogiska härledningsregler

Satslogiken är ett formellt logiskt system med väldefinierad syntax, avsett att symboliskt hantera språkliga satser, vilka uttrycker påståenden, och från dessa med giltiga slutledningar dra slutsatser. Att det satslogiska systemet är formellt, innebär att dess teori, regler och definitioner inte hänvisar till symbolernas eller de språkliga uttryckens betydelser, utan endast till relationer mellan de symboler av vilka de språkliga uttrycken är uppbyggda. Satslogikens logiska syntax innehåller en systematisk framställning av giltiga slutledningsregler.

Till grundläggarna av den formella logiken, särskilt satslogiken, räknas George Boole, Gottlob Frege och Bertrand Russell.

I vardagsspråket används en mängd olika ord för att sammanbinda ("connect") satser. Dessa ord kallas konnektiv. I satslogiken är konnektiven väldefinierade och de fem, som företrädesvis används är:

icke, och, eller, om... så... och om och endast om. Symbolerna för dessa uttryck är respektive  \neg , \land , \lor, och .

Påståenden i form av atomära satser eller elementarsatser, betecknas med en bokstav. Den implikation, som förekommer i satslogiken och som symboliseras med tecknet, →, är en så kallad materiell implikation, vars innebörd ofta missförstås. Det förtjänar att påpekas att satsen: om p så q, och som skrivs p → q, inte är en implikation i den bemärkelsen att det skulle råda något logiskt eller kausalt samband mellan p och q. Den kan heller inte tolkas så, att q kan härledas från p. Att en sats materiellt implicerar en annan, betyder i satslogiken endast att det icke är så, att den första satsen är sann och den andra falsk.

Satslogiken har formaliserats till algebraisk kalkyl i den Booleska algebran.

Exempel på satslogiska påståenden[redigera | redigera wikitext]

p : Min klocka går rätt.
q : Tåget är försenat.
¬p : Min klocka går inte rätt.
p \land q : Min klocka går rätt och tåget är försenat.
p \lor q : Min klocka går rätt eller tåget är försenat.
pq : Om min klocka går rätt så är tåget försenat.
pq : Min klocka går rätt om och endast om tåget är försenat.

Härledning[redigera | redigera wikitext]

I satslogiken är begreppet tautolog implikation fundamentalt och definieras nedan:

  • En formel F sägs tautologt implicera en formel G, om och endast om implikationen F → G är en tautologi.
  • En satslogisk slutledning är giltig, om och endast om konjunktionen av premisserna tautologt implicerar slutsatsen.

Ett exempel på en giltig slutledningsregel är Modus Tollendo Tollens, vilken kan tillämpas enligt följande:


\begin{array}{c}
p \rightarrow q \\
\neg q \\
\hline
\neg p
\end{array}

Att slutsatsen är korrekt och således grundad på en giltig slutledning, följer av att ((p → q) \land\neg q)\neg p är en tautolog implikation. Man säger att slutsatsen är en satslogisk eller syntaktisk konsekvens av premisserna. Om F betecknar konjunktionen av premisserna och G slutsatsen, skriver man F \vdash G.

Konnektivens fullständighet[redigera | redigera wikitext]

Det finns satskonnektiv i det naturliga språket, som inte representerar sanningsfunktioner. De har därför inte någon motsvarighet i det satslogiska språket. Man har visat att de ovan införda fem konnektiven kan ersättas med endast ett par av dessa. Med exempelvis konnektiven \neg och \land eller \neg och → kan man binda ihop alla de satser, som kan konstrueras med de fem konnektiven. Ett prov på detta är, att satsen p → g kan skrivas \neg p \lor q.

Axiomatiskt system och satslogiskt bevis[redigera | redigera wikitext]

Satslogikens formella språk brukar betecknas med bokstaven P. I det fall då man strikt bygger upp det satslogiska systemet med ett antal axiom och minst en slutledningsregel, refererar man till detta med beteckningen PS. I detta system är en formel A logiskt giltig om den kan bevisas med hjälp av axiomen, tidigare bevisade teorem och givna härledningsregler i systemet och kallas då för ett teorem. Ett bevis i PS är också en härledning i PS, men det omvända gäller inte.

Definition. En formel A är en syntaktisk konsekvens i PS av en mängd formler G i språket P, om och endast om det finns en härledning i PS av A från G, vilket skrivs G \vdash_{PS} A. Om formlerna i G inte är teorem så är härledningen således inte ett bevis.

Källor[redigera | redigera wikitext]

  • G.H. von Wright, Logik, filosofi och språk, Berlingska, Lund 1957.
  • Geoffrey Hunter, Metalogic. An Introduction to the Metatheory of Standard First-order Logic, MacMillan, 1971.

Se även[redigera | redigera wikitext]