Propositielogica

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

De propositielogica is een tak van logica die zich bezighoudt met geldige redeneringen in de vorm van 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 inleiding[bewerken]

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 samengesteld zijn uit twee of meer andere proposities met behulp van voegwoorden, in deze context ook connectieven genoemd ("Morgen schijnt de zon en we gaan morgen picknicken", "Als morgen de zon schijnt, gaan we morgen picknicken").

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

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 AB waar, als A en B beide waar zijn, terwijl AB waar is, als A waar is, B waar is, of zowel A als B waar zijn.

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

AB 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.
AB 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 het niet het geval is dat we gaan picknicken, is de uitspraak onwaar.
AB is de uitspraak: Als morgen de zon schijnt, gaan we morgen picknicken. Aangezien de waarheid van deze uitspraak alleen af mag hangen 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".
¬A is de uitspraak: Morgen schijnt de zon niet. Deze uitspraak is waar als de zon niet schijnt, en onwaar als de zon wel schijnt.

De bewering AB 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:

"1=1" \lor "2=2" is waar,
"1=1" \lor "1=2" is waar, maar
"1=2" \lor "2=1" is niet waar.

Hoewel waarheid een basisbegrip van de propositielogica is, richt ze zich ook vooral op geldigheid en onvervulbaarheid. Een propositie is geldig wanneer ze altijd waar is, onafhankelijk van welke waarheidswaarden aan de enkelvoudige proposities wordt toegekend. Zo is de propositie (AB) ↔ ¬(¬A ∨ ¬B) altijd waar. Een propositie is onvervulbaar wanneer ze altijd onwaar is. Ook onderzoekt de logica de geldigheid van redeneerstappen. Als A een ware propositie is en AB ook, dan is een B ook een ware propositie. Dit geldt voor alle waarheidswaarden van A en B. Uit de premissen A en AB kunnen we dus de conclusie B afleiden (deze redeneerregel wordt ook modus ponens genoemd).

Syntaxis en semantiek[bewerken]

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

Formules[bewerken]

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 p een propositievariabele is, dan is p ook een formule;
  • conjunctie: als A en B formules zijn, dan is ook (A \land B) een formule;
  • disjunctie: als A en B formules zijn, dan is ook (A \lor B) een formule;
  • negatie: als A een formule is, dan is ook \neg A een formule.

Bovendien definiëren we de volgende afkortingen:

  • implicatie: (A \to B) betekent: \neg A \lor B.
  • equivalentie: (A \leftrightarrow B) betekent: (A \to B) \land (B \to A).

We spreken af dat negatie (\neg) het sterkste bindt, daarna conjunctie (\land), daarna disjunctie (\lor, en daarna implicatie (\to) en bi-implicatie (\leftrightarrow). Bovendien spreken we af dat de implicatie rechts-associatief is. Dat betekent dat we p \to \neg q \to p \land \neg q mogen schrijven in plaats van (p \to (\neg q \to (p \land \neg q))).

Valuaties[bewerken]

Om de semantiek, dat wil zeggen 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 het begrip valuatie uit zodat ook aan formules waarheidswaarden worden toegekend, en wel als volgt:

  • v(A \land B) = \begin{cases} 1 & \mbox{als } v(A)=1 \mbox{ en } v(B)=1 \\ 0 & \mbox{anders} \end{cases}
  • v(A \lor B) = \begin{cases} 0 & \mbox{als } v(A)=0 \mbox{ en } v(B)=0 \\ 1 & \mbox{anders} \end{cases}
  • v(\neg A) = \begin{cases} 0 & \mbox{als } v(A) = 1 \\ 1 & \mbox{als } v(A) = 0 \end{cases}

Geldigheid en vervulbaarheid[bewerken]

Een formule A is vervulbaar wanneer er ten minste één valuatie v bestaat zodat v(A) = 1. Een formule is onvervulbaar wanneer ze niet vervulbaar is, dat wil zeggen, wanneer er geen valuatie v bestaat zodat v(A) = 1.

Een formule A is geldig wanneer voor alle valuaties v geldt, dat v(A) = 1. Een geldige formule wordt ook wel logische wet genoemd. Het feit dat een formule A geldig is wordt genoteerd als \models A. Voorbeelden van geldige formules zijn:

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 A_1,\ldots,A_n \models B geeft aan, dat de gevolgtrekking met hypotheses A_1,\ldots,A_n en conclusie B geldig is. In de klassieke propositielogica geldt A_1,\ldots,A_n \models B dan en slechts dan als (A_1\land\cdots\land A_n)\to B geldig is.

Twee formules A en B zijn logisch equivalent als A en B waar zijn in precies dezelfde valuaties. Dat betekent dat voor alle valuaties v moet gelden, dat als v(A)=1, dan ook v(B)=1, en dat als v(B)=1, dan ook v(A)=1. In de klassieke propositielogica zijn A en B dan en slechts dan logisch equivalent, als A\leftrightarrow B een geldige formule is.

Waarheidstabellen[bewerken]

Nuvola single chevron right.svg 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 uit te zoeken, of een gevolgtrekking geldig is en of twee formules logisch equivalent zijn. In een waarheidstabel worden alle mogelijkheden om aan de propositievariabelen waarheidswaarden toe te kennen 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:

A B \neg A A \land B A \lor B A \to B A \leftrightarrow B
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 \neg A, A \land B, A \lor B, A \to B en A \leftrightarrow B alle vervulbaar maar niet geldig zijn.

Een nadeel van een waarheidstabel bij het onderzoeken van een complexe logische stelling zoals A → (B ∧ ¬C) is dat het aantal mogelijke combinaties van de verschillende variabelen (hier A, B en C) exponentieel toeneemt met het aantal variabelen in de stelling. De waarheidstabel van een stelling met n variabelen telt 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 practische toepassingen ontstaan formules die honderden of zelfs duizenden propositievariabelen bezitten. In zulke gevallen is het zelfs met de computer practisch niet meer mogelijk de volledige waarheidstafel uit te rekenen, en moeten andere methoden worden gevonden om te beslissen of een formule geldig of vervulbaar is.

Bewijssystemen[bewerken]

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 vervuld is en geconcludeerd wordt 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 Hilbert[bewerken]

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, zo dat 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 A en A\to B volgt B (hierbij staan A en B voor willekeurige propositielogische formules);
  • uniforme substitutie: uit A volgt A[p/B], de formule die ontstaat door in A alle voorkomens van de propositie p te vervangen door B.

Bovendien bevat het de volgende axioma's:

  • P1: p \to p
  • P2: p \to (q \to p)
  • P3: (p \to (q \to r)) \to ((p \to q) \to (p \to r))
  • P4: (\neg p \to \neg q) \to (q \to p)

De bovenstaande axioma's zijn voldoende voor formules die alleen de logische connectieven \to en \neg bevatten. Voor formules die conjucties (\land) en disjuncties (\lor) bevatten, kunnen we de volgende axioma's toevoegen:

  • p \to q \to (p \land q)
  • (p \land q) \to p
  • (p \land q) \to q
  • p \to (p \lor q)
  • q \to (p \lor q)
  • (p \to r) \to (q \to r) \to (p \lor q) \to r

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

1. (p \to (q \to r)) \to ((p \to q) \to (p \to r)) (P3)
2. (p \to (q \to p)) \to ((p \to q) \to (p \to p)) Universele subst. uit 2, [r/p]
3. p \to (q \to p) (P2)
4. (p \to q) \to (p \to p) Modus ponents uit 2, 3
5. (p \to (q \to p)) \to (p \to p) Universele subst. uit 4, [q/(q \to p)]
6. p \to p Modus ponens uit 3, 5

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

Semantische tableaus[bewerken]

Nuvola single chevron right.svg 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 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 moeten A en B allebei waar zijn, of A is niet waar en de waarde van B maakt niet uit. 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 deductie[bewerken]

Nuvola single chevron right.svg 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 logische 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).

Resolutie[bewerken]

Nuvola single chevron right.svg 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

(A \lor B_1 \lor\cdots\lor B_n) \land (\neg A \lor C_1 \lor\cdots\lor C_m) \models B_1 \lor\cdots\lor B_n \lor C_1 \lor\cdots\lor C_m

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.

Complexiteitstheorie[bewerken]

Het probleem om van een gegeven propositielogische formule uit te vinden 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 zeer goede resultaten boeken.