Propositielogica

De propositielogica is een tak van logica die zich bezighoudt met het redeneren met proposities. Proposities zijn uitspraken of beweringen die ofwel waar, ofwel onwaar zijn. Voorbeelden hiervan zijn

De Winkler Prins is een encyclopedie

en

Wicky heeft een noormannenhelm op.

In de propositielogica kunnen uitspraken alleen waar of onwaar zijn, dit in tegenstelling tot meerwaardige logica's waarbij uitspraken ook andere waarden kunnen hebben.

In vergelijking met andere types van logica is de propositielogica eenvoudig van opbouw (structuur, grammatica) maar beperkt in uitdrukkingsmogelijkheid.

Informele inleidingBewerken

De propositielogica gaat over het redeneren met proposities. Een propositie is een uitspraak die waar of onwaar kan zijn. Proposities kunnen enkelvoudig zijn ("Morgen schijnt de zon" of "We gaan morgen picknicken") maar ook zijn samengesteld uit twee of meer andere proposities met behulp van (logische) voegwoorden, in deze context connectieven (soms ook voegtekens) genoemd ("Morgen schijnt de zon en we gaan morgen picknicken", "Als morgen de zon schijnt, dan gaan we morgen picknicken.").

In de propositielogica worden de volgende connectieven gebruikt om proposities samen te stellen:

  • negatie (ontkenning):   of ~  (lees als: niet  ).
  • conjunctie:   (lees als:   en  ).
  • disjunctie:   (lees als:   of  ).
  • implicatie (gevolgtrekking):   (lees als: als   dan  ).
  • equivalentie (gelijkwaardigheid):   (lees als:   dan en slechts dan als  ).

Verder is er één propositieconstante, genaamd falsum en aangeduid met  , die staat voor een altijd onware propositie.

In de propositielogica hangt de waarheid van samengestelde proposities alleen af van het gebruikte connectief en van de waarheid van de samenstellende delen. Zo is   waar als   en   beide waar zijn, terwijl   waar is als   waar is,   waar is of zowel   als   waar zijn.

Stel bijvoorbeeld dat   voor de enkelvoudige propositie "Morgen schijnt de zon" staat en   voor "We gaan morgen picknicken". Dan geldt:

  •   is de uitspraak: Morgen schijnt de zon of we gaan morgen picknicken. Deze uitspraak is waar als morgen inderdaad de zon schijnt of als we gaan picknicken of allebei, en onwaar als morgen de zon niet schijnt en we ook niet gaan picknicken.
  •   is de uitspraak: Morgen schijnt de zon en we gaan morgen picknicken. Deze uitspraak is waar als morgen de zon schijnt en we ook gaan picknicken. Als de zon morgen niet schijnt of als we niet gaan picknicken of allebei (als de zon morgen niet schijnt en we niet gaan picknicken), dan is de uitspraak onwaar.
  •   is de uitspraak: Als morgen de zon schijnt, dan gaan we morgen picknicken. Aangezien de waarheid van deze uitspraak alleen mag afhangen van de waarheid van de samenstellende delen, vinden veel mensen de implicatie tegenintuïtief. Als de zon schijnt en we niet gaan picknicken, is de uitspraak uiteraard niet waar. In alle andere gevallen, als de zon niet schijnt of als de zon wel schijnt en we ook gaan picknicken, is de uitspraak waar. Zo komen we tot de conclusie dat de uitspraak hetzelfde betekent als Morgen schijnt de zon niet of we gaan morgen picknicken.
  •   is de uitspraak: Morgen schijnt de zon niet. Deze uitspraak is waar als de zon morgen niet schijnt en onwaar als de zon dan wel schijnt.

De bewering   is waar als ten minste een van de twee beweringen waar is. De bewering is dus ook waar als beide beweringen waar zijn, iets wat in natuurlijke taal vaak niet zo bedoeld wordt. Dus er geldt:

  is waar,
  is waar, maar
  is niet waar.

Hoewel waarheid een basisbegrip van de propositielogica is, richt ze zich ook vooral op geldigheid en onvervulbaarheid. Een propositie is geldig (een tautologie) als ze altijd waar is, onafhankelijk van welke waarheidswaarden aan de enkelvoudige proposities wordt toegekend. Zo is de propositie   altijd waar. Een propositie is onvervulbaar als ze altijd onwaar is.

Ook onderzoekt de logica de geldigheid van redeneerstappen. Als   een ware propositie is en   is dat ook, dan is   eveneens een ware propositie. Dit geldt voor alle waarheidswaarden van   en  . Uit de premissen   en   kan dus de conclusie   worden afgeleid. Deze redeneerregel wordt modus ponens genoemd.

Syntaxis en semantiekBewerken

Als men over propositielogica spreekt, heeft men het meestal over de klassieke propositielogica. Hieronder wordt de syntaxis en semantiek van deze logica gegeven.

FormulesBewerken

Laat een aftelbaar oneindige verzameling van enkelvoudige proposities, ook propositievariabelen genoemd, gegeven zijn. Dan definiëren we de verzameling van formules als de kleinste verzameling waarvoor geldt:

  • propositievariabelen: als   een propositievariabele is, dan is   ook een formule;
  • conjunctie: als   en   formules zijn, dan is ook   een formule;
  • disjunctie: als   en   formules zijn, dan is ook   een formule;
  • negatie: als   een formule is, dan is ook   een formule.

Bovendien definiëren we de volgende afkortingen:

  • implicatie:   betekent:  .
  • equivalentie:   betekent:  .

Bewerkingsvolgorde: We spreken af dat negatie ( ) het sterkste bindt, daarna conjunctie ( ), daarna disjunctie ( ), en daarna implicatie ( ) en bi-implicatie ( ). Bovendien spreken we af dat de implicatie van rechts naar links associatief is. Dat betekent dat we   mogen schrijven in plaats van  .

ValuatiesBewerken

Om de semantiek (d.w.z. de betekenis) van een formule te definiëren, hebben we het begrip valuatie nodig. Een valuatie v is een functie die aan (een deel van) de propositievariabelen een waarheidswaarde, waar (1) of onwaar (0), toekent. Op basis van de waarheidswaarden van de propositievariabelen die in een formule voorkomen, kunnen we dan de waarheidswaarde van de volledige formule bepalen. Daarvoor breiden we het begrip valuatie uit zodat ook aan formules waarheidswaarden worden toegekend, en wel als volgt:

  •  
  •  
  •  

Geldigheid en vervulbaarheidBewerken

Een formule   is vervulbaar als er ten minste één valuatie   bestaat zodat  . Een formule is onvervulbaar als ze niet vervulbaar is; met andere woorden, als er geen valuatie   bestaat zodat   is.

Een formule   is geldig (is een tautologie) als voor alle valuaties   geldt dat  . Een geldige formule wordt ook wel een logische wet genoemd. Het feit dat een formule   geldig is, wordt genoteerd als  . Voorbeelden van geldige formules zijn:

  •  
  •  
  •   (wet van de uitgesloten derde; deze geldt bij de klassieke propositielogica, maar niet bij de intuitionistische propositielogica)
  •   en   (de wetten van De Morgan)
  •   (contrapositie)

Een gevolgtrekking heeft een aantal hypotheses en een conclusie. Een gevolgtrekking is geldig als in alle valuaties waarin de hypotheses waar zijn de conclusie ook waar is. De notatie   geeft aan dat de gevolgtrekking met hypotheses   en conclusie   geldig is. In de klassieke propositielogica geldt   dan en slechts dan als   geldig is.

Twee formules   en   zijn logisch equivalent als   en   waar zijn in precies dezelfde valuaties. Dat betekent dat voor alle valuaties   moet gelden dat als   is, dan ook  , en dat als   is, dan ook  . In de klassieke propositielogica zijn   en   dan en slechts dan logisch equivalent, als   een geldige formule is.

IdentiteitswetBewerken

Zijn   en   proposities met   en  , dan is:

  •  
  •  

Deze equivalenties vormen de identiteitswet van de propositielogica.

WaarheidstabellenBewerken

  Zie Waarheidstabel voor het hoofdartikel over dit onderwerp.

Waarheidstabellen vormen een methode om te onderzoeken of een formule geldig of vervulbaar is. Bovendien kunnen waarheidstabellen worden gebruikt om te weten te komen of een gevolgtrekking geldig is, alsook om te achterhalen of twee formules logisch equivalent zijn. In een waarheidstabel worden alle mogelijke waarheidswaarden van propositievariabelen opgesomd. Elke rij in de tabel correspondeert met een valuatie, terwijl elke kolom correspondeert met een formule. In de tabel wordt dan opgenomen of de formule onder de gegeven valuatie waar is of niet. Een voorbeeld van een waarheidstabel met enkele eenvoudige formules:

             
0 0 1 0 0 1 1
0 1 1 0 1 1 0
1 0 0 0 1 0 0
1 1 0 1 1 1 1

Een formule is geldig als er in de waarheidstabel alleen maar 1'en in de kolom eronder staan. De formule is vervulbaar als er minstens één 1 in de kolom staat. Zo blijkt uit de bovenstaande waarheidstabel dat  ,  ,  ,   en   allemaal vervulbaar maar niet geldig zijn.

Bij het onderzoeken van een complexe logische stelling zoals A → (B ∧ ¬C) zal het aantal mogelijke combinaties van de verschillende variabelen (hier A, B en C) exponentieel toenemen met het aantal variabelen in de stelling. De waarheidstabel van een stelling met n variabelen telt immers 2n rijen. Voor een formule met 3 of zelfs 4 variabelen is dat met de hand nog wel te doen (de tabel telt 8 of 16 rijen), maar bij veel praktische toepassingen ontstaan formules met honderden of zelfs duizenden propositievariabelen. In zulke gevallen is het zelfs met de computer praktisch niet meer mogelijk de volledige waarheidstabel uit te rekenen en moeten andere methoden worden gevonden om te beslissen of een formule geldig of vervulbaar is.

BewijssystemenBewerken

In tegenstelling tot waarheidstabellen, waar de betekenis van de logische connectieven een belangrijke rol speelt, wordt in een bewijssysteem slechts gewerkt met syntactische constructies. Formules worden aan de hand van regels omgeschreven in andere formules totdat een bepaalde voorwaarde is vervuld en men concludeert dat de formule geldig (of in sommige gevallen onvervulbaar) is. Belangrijke eigenschappen die een bepaald bewijssysteem moet hebben zijn correctheid (als een formule met het bewijssysteem bewezen kan worden is ze ook geldig) en volledigheid (als een formule geldig is kan ze ook bewezen worden).

Voor de propositielogica bestaan verschillende correcte en volledige bewijssystemen.

Bewijssysteem in de stijl van HilbertBewerken

Een bewijssysteem in de stijl van Hilbert bestaat uit een aantal axioma's en een aantal inferentieregels. Een bewijs in zo'n systeem is een eindig rijtje formules dat eindigt in de formule die bewezen moet worden, zodat voor elk element van het rijtje geldt dat het ofwel een axioma is, ofwel door een inferentieregel volgt uit formules die eerder in het rijtje voorkomen (en daardoor al bewezen zijn). Anders dan de meeste andere bewijssystemen die met inferentieregels werken, zoals natuurlijke deductie, introduceren inferentieregels in een Hilbert-systeem geen aannames. Omdat daardoor de structuur van bewijssystemen in de stijl van Hilbert heel eenvoudig is, worden zulke bewijssystemen vaak gebruikt in de bewijstheorie, waar formele bewijzen niet alleen een manier zijn om de waarheid van uitspraken te bepalen, maar zelf ook het onderwerp van studie zijn. (Dat de structuur van een bewijssysteem eenvoudig is, betekent overigens niet dat het ook eenvoudig is een bewijs erin op te stellen.)

Het bekendste Hilbert-bewijssysteem voor de propositielogica bevat de volgende inferentieregels:

  • modus ponens: uit   en   volgt   (hierbij staan   en   voor willekeurige propositielogische formules);
  • uniforme substitutie: uit   volgt  , de formule die ontstaat door in   alle voorkomens van de propositie   te vervangen door  .

Bovendien bevat het de volgende axioma's:

  • P1:  
  • P2:  
  • P3:  
  • P4:  

De bovenstaande axioma's zijn voldoende voor formules die alleen de logische connectieven   en   bevatten. Voor formules die conjuncties ( ) en disjuncties ( ) bevatten, kunnen we de volgende axioma's toevoegen:

  •  
  •  
  •  
  •  
  •  
  •  

Het axioma P1 is eigenlijk niet nodig, omdat het op de volgende manier uit de axioma's P2 en P3 kan worden afgeleid:

1.   (P3)
2.   Uniforme substitutie uit 2,  
3.   (P2)
4.   Modus ponens uit 2, 3
5.   Uniforme substitutie uit 4,  
6.   Modus ponens uit 3, 5

Toch wordt P1 meestal wel in de axioma's van dit bewijssysteem opgenomen.

Semantische tableausBewerken

  Zie Semantisch tableau voor het hoofdartikel over dit onderwerp.

Een semantisch tableau onderzoekt een stelling door de implicaties van een stelling te ontleden. Als een stelling waar is, wat betekent dat dan voor de waarheidswaarde van de variabelen in de stelling? Als A∧B waar is, dan moeten zowel A als B waar zijn. Als A→B waar is, dan is A onwaar en maakt de waarde van B niet uit of dan moeten A en B allebei waar zijn. Op deze manier kan een boom getekend worden die een complexe formule opsplitst in steeds kleinere delen, totdat duidelijk is welke waarden de variabelen aan moeten nemen om de stelling waar te maken. Semantische tableaus worden vaak gebruikt in combinatie met het bewijs uit het ongerijmde om te bewijzen dat een stelling volgt uit een aantal hypothesen.

Natuurlijke deductieBewerken

  Zie Natuurlijke deductie voor het hoofdartikel over dit onderwerp.

Natuurlijke deductie is een door Gerhard Gentzen ontwikkeld bewijssysteem dat gebaseerd is op een natuurlijke manier van redeneren. Kenmerkend aan natuurlijke deductie is dat bewijzen een boomstructuur hebben en dat aannames ingevoerd en weer teruggetrokken kunnen worden. Daardoor ontstaat een natuurlijke notie van deelbewijs. Elk logisch connectief heeft een regel die vastlegt hoe gewenste conclusies die dit connectief als hoofdconnectief hebben, bewezen kunnen worden (de zogenaamde introductieregels), en een regel die vastlegt hoe aannames die dit connectief als hoofdconnectief hebben, kunnen worden gebruikt (de zogenaamde eliminatieregels).

ResolutieBewerken

  Zie Resolutie (logica) voor het hoofdartikel over dit onderwerp.

Met de bewijsmethode resolutie kan van formules in conjunctieve normaalvorm de onvervulbaarheid worden aangetoond. Resolutie is gebaseerd op de geldige gevolgtrekking

 

Er wordt geprobeerd door steeds deze gevolgtrekking toe te passen op de conjuncten van de formule de lege disjunctie af te leiden. Als dat is gelukt, is de formule niet vervulbaar. Resolutie wordt vaak toegepast in automatische stellingbewijzers.

ComplexiteitstheorieBewerken

Het probleem om van een gegeven propositielogische formule na te gaan of het vervulbaar is, wordt het vervulbaarheidsprobleem genoemd (meestal afgekort tot SAT, van het Engelse satisfiability). SAT is beslisbaar. We kunnen namelijk voor elke formule automatisch de waarheidstabel opstellen en kijken of de formule in één rij daarvan waar is. Het aantal rijen in de waarheidstabel neemt echter exponentieel toe in verhouding met het aantal propositievariabelen dat in de formule voorkomt. Al voor een relatief klein aantal propositievariabelen is het in de praktijk niet meer mogelijk om de gehele waarheidstabel op te stellen. Aangezien SAT NP-volledig is, bestaat er op dit moment geen algoritme dat van alle formules efficiënt kan achterhalen of ze vervulbaar zijn of niet. Er bestaan echter algoritmes die in de praktijk voortreffelijke resultaten boeken.