Att det satslogiska systemet ärformellt, 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 giltigaslutledningsregler.Till grundläggarna av den formella logiken, särskilt satslogiken, räknasGeorge Boole,Gottlob Frege ochBertrand Russell.
I vardagsspråket används en mängd olika ord för att sammanbinda ("connect") satser. Dessa ord kallaskonnektiv. I satslogiken är konnektiven väldefinierade och de fem, som företrädesvis används är:
Påståenden i form av atomära satser ellerelementarsatser, betecknas med en bokstav. Den implikation, som förekommer i satslogiken och som symboliseras med tecknet,, är en så kalladmateriell 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 ellerkausalt 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.
Emil L. Post visade att det satslogiska systemet PS med språket P ärsemantisktfullständigt. Således är varjetautologi A, i språket P ettteorem i systemet PS, vilket symboliskt kan uttryckas enligt följande: Om så.[1][2].
Satslogiken har formaliserats till algebraisk kalkyl i denBooleska algebran.
I satslogiken är begreppettautolog implikation fundamentalt och definieras nedan:
En formel F sägs tautologt implicera en formel G, om och endast om implikationen F → G är entautologi.
En satslogisk slutledning är giltig, om och endast om konjunktionen av premisserna tautologt implicerar slutsatsen.
Ett exempel på en slutledningsregel ärModus Tollendo Tollens, vilken kan tillämpas enligt följande:
vilket betyder att av tvåpremisser, där den ena är enmateriell implikation och den andra är negationen av implikationens andra led, följer negationen av implikationens första led.
Från premisserna P→Q ochQ kan såledesslutsatsenP dras
Att slutsatsen är korrekt och således grundad på en giltig slutledning, följer av att
är en tautolog implikation. Man säger att slutsatsen är en satslogisk ellersyntaktisk konsekvens av premisserna. Formellt skriver man:
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 och eller och → kan man binda ihop alla de satser, som kan konstrueras med de fem konnektiven. Exempelvis kan satsen p → q skrivas.
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 slutledningssregler i systemet och kallas då för ett teorem. Ett bevis i PS är också enhä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. Om formlerna i G inte är teorem så är härledningen således inte ett bevis.