Propositielogica: Formele Grondslagen en Toepassingen in de Informatica

# Inleiding

Propositielogica, ook wel uitspraaklogica genoemd, vormt de funderende basis van formele logica in de wiskunde en informatica. Als een tak van de symbolische logica biedt propositielogica een wiskundige taal en formeel framework om uitspraken te representeren en hun logische verbanden te analyseren. In essentie stelt propositielogica ons in staat om complexe statements op te bouwen uit basisuitspraken (proposities) door middel van logische operatoren, en vervolgens de geldigheid van logische argumenten en redeneringen te verifiëren.

Voor informatici is propositielogica van fundamenteel belang omdat het de theoretische basis vormt van veel computationele processen en systemen. De binaire aard van elektronische circuits en digitale systemen correspondeert direct met de tweewaardige semantiek van de klassieke propositielogica (waar/onwaar). Dit is geen toevallige overlap; de architectuur en operationele semantiek van digitale computers zijn grotendeels gebaseerd op Boolean algebra, die nauw verwant is aan de propositielogica.

De relevantie van propositielogica in de informatica strekt zich uit over talrijke domeinen:

1. Programmeertalen: Conditionele statements, Boolean expressies en controlestructuren in programmeertalen zijn directe toepassingen van propositielogische principes. De evaluatie van logische expressies in een programma volgt de semantische regels van de propositielogica.

2. Hardware-ontwerp: Digitale schakelingen zijn fysieke implementaties van logische functies. De systematische omzetting van Boolean expressies naar elektronische componenten zoals AND-, OR- en NOT-poorten vormt de basis van hardwareontwerp en digitale elektronica.

3. Formele Verificatie: Het bewijzen van de correctheid van algoritmen, protocollen en systemen vereist formele logica. Propositielogica biedt fundamentele bewijstechnieken voor het verifiëren van eigenschappen in eindige systemen.

4. Theoretische Informatica: De complexiteitstheorie maakt gebruik van propositielogische formules om fundamentele problemen zoals het SAT-probleem (satisfiability problem) te definiëren, wat cruciaal is voor het begrijpen van computationele complexiteit.

5. Kunstmatige Intelligentie: Kennisrepresentatie, automatisch redeneren en expertsystemen bouwen voort op logische formalismen. Propositielogica dient als basis voor complexere logische systemen zoals predicatenlogica en modale logica die in AI-systemen worden toegepast.

6. Databases: Query-optimalisatie in databasesystemen maakt gebruik van logische equivalenties en transformatieregels die zijn afgeleid van propositielogica.

Dit artikel beoogt een diepgaande, formele behandeling van propositielogica te bieden, beginnend bij de axiomatische grondslagen en voortbouwend naar praktische toepassingen in de informatica. We zullen de syntaxis en semantiek van propositielogica nauwkeurig definiëren, de sleutelconcepten van tautologie en logische equivalentie onderzoeken, bewijstechnieken bestuderen en analyseren hoe deze abstracte concepten worden toegepast in concrete informaticaproblemen. Door dit artikel heen zullen formele definities worden afgewisseld met verhelderende voorbeelden en uiteindelijk worden aangevuld met oefeningen om het begrip te versterken.

Door de studie van propositielogica verwerft men niet alleen technische vaardigheden voor het oplossen van specifieke problemen, maar ook een fundamentele denkwijze die van onschatbare waarde is voor de ontwikkeling van robuuste, correcte software en computersystemen.

# Formele Grondslagen

# Proposities en Atomaire Zinnen

In de propositielogica is een propositie een declaratieve zin waaraan ondubbelzinnig een waarheidswaarde kan worden toegekend: waar (true, T) of onwaar (false, F). Deze definitie sluit vragen, bevelen, uitroepen en ambigue of subjectieve uitspraken uit.

Definitie 1.1: Een propositie is een uitspraak die waar of onwaar is, maar niet beide tegelijk.

Voorbeelden van geldige proposities:

• "Amsterdam is de hoofdstad van Nederland." (waar)
• "7 is een priemgetal." (waar)
• "2 + 3 = 6" (onwaar)

Voorbeelden van niet-proposities:

• "Hoe laat is het?" (vraag)
• "Sluit de deur." (bevel)
• "Deze zin is onwaar." (paradoxaal, kan niet consistent waar of onwaar zijn)

Atomaire proposities (of atomaire zinnen) zijn de elementaire bouwstenen van de propositielogica. Dit zijn enkelvoudige proposities die niet verder opgedeeld kunnen worden in eenvoudigere proposities.

Definitie 1.2: Een atomaire propositie is een propositie die niet is samengesteld uit andere proposities door middel van logische connectieven.

In de formele notatie worden atomaire proposities vaak aangeduid met hoofdletters zoals P, Q, R, etc. Complexere proposities kunnen worden opgebouwd door atomaire proposities te combineren met logische operatoren.

# Syntax

De syntax van propositielogica definieert de formele regels voor het construeren van welgevormde formules (WFFs - Well-Formed Formulas) uit atomaire proposities en logische operatoren.

Definitie 1.3: De taal van propositielogica L wordt inductief gedefinieerd als volgt:

1. Basisstap: Als P een atomaire propositie is, dan is P ∈ L.
2. Inductieve stap:
   • Als φ ∈ L, dan is ¬φ ∈ L.
   • Als φ ∈ L en ψ ∈ L, dan zijn (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), en (φ ↔ ψ) allemaal ∈ L.
3. Afsluitingsregel: Een formule behoort tot L alleen als deze kan worden geconstrueerd door eindige toepassing van de regels 1 en 2.

Hierbij zijn φ en ψ metavariabelen die staan voor willekeurige formules in L, en ¬, ∧, ∨, →, en ↔ zijn de logische operatoren (respectievelijk negatie, conjunctie, disjunctie, implicatie en equivalentie).

Conventie: Om het overmatig gebruik van haakjes te vermijden, hanteren we de volgende precedentieregels (van hoogste naar laagste prioriteit):

1. ¬ (negatie)
2. ∧ (conjunctie) en ∨ (disjunctie)
3. → (implicatie)
4. ↔ (equivalentie)

Operatoren van dezelfde precedentie worden van links naar rechts geëvalueerd, tenzij anders aangeduid met haakjes.

Voorbeelden van welgevormde formules:

• P
• ¬P
• (P ∧ Q)
• P → (Q ∨ R)
• ((P → Q) ∧ P) → Q

Voorbeeld van een formule die niet welgevormd is:

• P ∧ → Q (ontbrekende linkeroperand voor →)

# Semantiek

De semantiek van propositielogica definieert hoe waarheidswaarden worden toegekend aan proposities en hoe deze waarden door logische operatoren worden gecombineerd.

Definitie 1.4: Een waarheidswaardetoekenning of interpretatie I is een functie die elke atomaire propositie P afbeeldt op een element uit de verzameling {T, F}, ofwel I: P → {T, F}.

Een interpretatie kent een waarheidswaarde toe aan elke atomaire propositie. Deze toekenning breidt zich uit naar complexe formules volgens de semantische regels voor de logische operatoren.

Definitie 1.5: Voor een willekeurige formule φ in de taal van propositielogica, definiëren we de semantische evaluatie onder interpretatie I, genoteerd als I(φ), inductief als volgt:

1. Als φ een atomaire propositie P is, dan is I(φ) = I(P).
2. Als φ van de vorm ¬ψ is, dan is I(φ) = T als I(ψ) = F, en I(φ) = F als I(ψ) = T.
3. Als φ van de vorm (ψ ∧ χ) is, dan is I(φ) = T als I(ψ) = T en I(χ) = T, anders is I(φ) = F.
4. Als φ van de vorm (ψ ∨ χ) is, dan is I(φ) = T als I(ψ) = T of I(χ) = T (of beide), anders is I(φ) = F.
5. Als φ van de vorm (ψ → χ) is, dan is I(φ) = F als I(ψ) = T en I(χ) = F, anders is I(φ) = T.
6. Als φ van de vorm (ψ ↔ χ) is, dan is I(φ) = T als I(ψ) = I(χ), anders is I(φ) = F.

Definitie 1.6: Een formule φ is waar onder interpretatie I als I(φ) = T, en onwaar onder interpretatie I als I(φ) = F.

Definitie 1.7: Een interpretatie I voldoet aan (of modelleert) een formule φ, geschreven als I ⊨ φ, als I(φ) = T.

# Logische Operatoren

Laten we de semantiek van elke logische operator in detail bestuderen:

1. Negatie (¬)

De negatie van een propositie P, genoteerd als ¬P, is waar dan en slechts dan als P onwaar is.

2. Conjunctie (∧)

De conjunctie van twee proposities P en Q, genoteerd als P ∧ Q, is waar dan en slechts dan als zowel P als Q waar zijn.

3. Disjunctie (∨)

De disjunctie van twee proposities P en Q, genoteerd als P ∨ Q, is waar dan en slechts dan als ten minste één van P of Q waar is.

De logische disjunctie correspondeert met de inclusieve of (of... of..., of beide), in tegenstelling tot de exclusieve of (of... of..., maar niet beide).

4. Implicatie (→)

De implicatie van P naar Q, genoteerd als P → Q, is onwaar dan en slechts dan als P waar is en Q onwaar is. In alle andere gevallen is de implicatie waar.

De implicatie P → Q kan worden gelezen als "als P, dan Q" of "P impliceert Q". Hierbij wordt P de antecedent genoemd en Q de consequent. Intuïtief gezien drukt de implicatie een voorwaardelijke relatie uit: als de antecedent waar is, dan moet de consequent ook waar zijn om de gehele implicatie waar te laten zijn.

Een belangrijk punt om op te merken is dat de implicatie P → Q waar is wanneer P onwaar is, ongeacht de waarheidswaarde van Q. Dit wordt soms de ex falso quodlibet (uit het onware volgt al het denkbare) genoemd. Hoewel dit contra-intuïtief kan lijken, is het een noodzakelijke consequentie van de formele definitie van de implicatie.

5. Equivalentie (↔)

De bi-implicatie of equivalentie van P en Q, genoteerd als P ↔ Q, is waar dan en slechts dan als P en Q dezelfde waarheidswaarde hebben.

De equivalentie P ↔ Q kan worden gezien als een verkorte notatie voor (P → Q) ∧ (Q → P), wat uitdrukt dat P en Q elkaar impliceren.

# Waarheidstabellen en Semantische Evaluatie

# Constructie van Waarheidstabellen

Waarheidstabellen zijn een fundamenteel instrument in de propositielogica om de semantiek van complexe formules systematisch te analyseren. Een waarheidstabel toont alle mogelijke combinaties van waarheidswaarden voor de atomaire proposities in een formule, en de resulterende waarheidswaarde van de formule voor elke combinatie.

Procedure voor het construeren van een waarheidstabel:

1. Identificeer alle atomaire proposities in de formule.
2. Creëer kolommen voor elke atomaire propositie en bepaal alle mogelijke combinaties van waarheidswaarden (2^n combinaties voor n proposities).
3. Voeg kolommen toe voor elke deelformule, waarbij je van de eenvoudigste naar de meest complexe werkt.
4. Bereken de waarheidswaarde van elke deelformule voor elke rij, gebaseerd op de semantische regels van de logische operatoren.

Voorbeeld: Construeer een waarheidstabel voor de formule (P → Q) ∧ ¬R.

In deze tabel hebben we eerst de waarheidswaarden voor de atomaire proposities P, Q en R opgelijst (kolommen 1-3). Vervolgens hebben we de waarheidswaarden voor de deelformules ¬R en P → Q berekend (kolommen 4-5). Ten slotte hebben we de waarheidswaarden voor de volledige formule (P → Q) ∧ ¬R bepaald (kolom 6).

# Tautologie, Contradictie en Contingentie

Op basis van de semantische evaluatie kunnen we proposities classificeren volgens hun logische status:

Definitie 2.1: Een formule φ is een tautologie als en slechts als I(φ) = T voor elke interpretatie I. Notatie: ⊨ φ.

Definitie 2.2: Een formule φ is een contradictie (of antilogie) als en slechts als I(φ) = F voor elke interpretatie I.

Definitie 2.3: Een formule φ is contingent (of logisch onbepaald) als en slechts als φ noch een tautologie noch een contradictie is, d.w.z., er is minstens één interpretatie waarvoor φ waar is en minstens één interpretatie waarvoor φ onwaar is.

Voorbeelden:

1. Tautologie: P ∨ ¬P (wet van de uitgesloten derde)

   P	¬P	P ∨ ¬P
   T	F	T
   F	T	T

2. Contradictie: P ∧ ¬P (wet van non-contradictie)

   P	¬P	P ∧ ¬P
   T	F	F
   F	T	F

3. Contingentie: P → Q

   P	Q	P → Q
   T	T	T
   T	F	F
   F	T	T
   F	F	T

# Semantische Gevolgtrekking

Een centraal concept in de propositielogica is het idee van logisch volgen of semantische gevolgtrekking.

Definitie 2.4: Een formule ψ is een semantisch gevolg van een verzameling formules Γ, genoteerd als Γ ⊨ ψ, als en slechts als voor elke interpretatie I waarvoor I ⊨ φ voor alle φ ∈ Γ, geldt ook dat I ⊨ ψ.

Met andere woorden, ψ volgt logisch uit Γ als elke interpretatie die alle formules in Γ waar maakt, ook ψ waar maakt.

Voorbeeld: Is Q een semantisch gevolg van {P, P → Q}?

Om dit te bepalen, moeten we controleren of elke interpretatie die zowel P als P → Q waar maakt, ook Q waar maakt:

De enige interpretatie die zowel P als P → Q waar maakt is de eerste rij, waar Q ook waar is. Dus {P, P → Q} ⊨ Q. Dit staat bekend als de regel van modus ponens.

# Logische Equivalentie en Wetmatigheden

# Definitie van Logische Equivalentie

Definitie 3.1: Twee formules φ en ψ zijn logisch equivalent, genoteerd als φ ≡ ψ, als en slechts als voor elke interpretatie I geldt: I(φ) = I(ψ).

Met andere woorden, twee formules zijn logisch equivalent als ze onder alle mogelijke interpretaties dezelfde waarheidswaarde hebben. Logische equivalentie impliceert dat de twee formules onderling vervangbaar zijn in elke context zonder de waarheidswaarde van de omsluitende formule te wijzigen.

Methoden om logische equivalentie aan te tonen:

1. Waarheidstabellen: Vergelijk de kolommen voor de twee formules in een waarheidstabel.
2. Algebraïsche manipulatie: Gebruik bekende equivalentiewetten om een formule te transformeren naar een andere.

Voorbeeld: Toon aan dat ¬(P → Q) ≡ P ∧ ¬Q.

Methode 1: Waarheidstabel

Aangezien de kolommen voor ¬(P → Q) en P ∧ ¬Q identiek zijn, zijn de formules logisch equivalent.

Methode 2: Algebraïsche manipulatie

¬(P → Q)
≡ ¬(¬P ∨ Q)       [Implicatie herschrijven: P → Q ≡ ¬P ∨ Q]
≡ ¬(¬P) ∧ ¬Q      [De Morgan's wet]
≡ P ∧ ¬Q          [Dubbele negatie]

# De Morgan's Wetten

De Morgan's wetten zijn fundamentele equivalentiewetten die een brug slaan tussen conjunctie, disjunctie en negatie.

Stelling 3.2 (De Morgan's wetten):

1. ¬(P ∧ Q) ≡ ¬P ∨ ¬Q
2. ¬(P ∨ Q) ≡ ¬P ∧ ¬Q

Bewijs (van eerste wet): We gebruiken een waarheidstabel om aan te tonen dat ¬(P ∧ Q) en ¬P ∨ ¬Q onder alle interpretaties dezelfde waarheidswaarden hebben.

Aangezien de kolommen voor ¬(P ∧ Q) en ¬P ∨ ¬Q identiek zijn, is de eerste De Morgan's wet bewezen. De tweede wet kan op dezelfde manier worden bewezen.

Intuïtieve interpretatie: De Morgan's wetten stellen dat de negatie van een conjunctie equivalent is aan de disjunctie van de negaties, en omgekeerd, dat de negatie van een disjunctie equivalent is aan de conjunctie van de negaties. Dit kan worden gezien als een formalisatie van het idee dat "niet beide" equivalent is aan "minstens één niet", en "niet minstens één" equivalent is aan "beide niet".

# Distributieve Wetten

De distributieve wetten beschrijven hoe conjunctie en disjunctie met elkaar in verband staan en bieden manieren om complexe formules te herschrijven.

Stelling 3.3 (Distributieve wetten):

1. P ∧ (Q ∨ R) ≡ (P ∧ Q) ∨ (P ∧ R)
2. P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R)

Bewijs (van eerste wet):

We construeren een waarheidstabel om aan te tonen dat P ∧ (Q ∨ R) en (P ∧ Q) ∨ (P ∧ R) onder alle interpretaties dezelfde waarheidswaarden hebben:

Aangezien de kolommen voor P ∧ (Q ∨ R) en (P ∧ Q) ∨ (P ∧ R) identiek zijn, is de eerste distributieve wet bewezen. De tweede wet kan op dezelfde manier worden bewezen.

# Associativiteit en Commutativiteit

Zowel conjunctie als disjunctie zijn associatief en commutatief, wat flexibiliteit biedt bij het herschrijven van formules.

Stelling 3.4 (Associativiteit):

1. (P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R)
2. (P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R)

Stelling 3.5 (Commutativiteit):

1. P ∧ Q ≡ Q ∧ P
2. P ∨ Q ≡ Q ∨ P

Het bewijs voor deze stellingen kan worden geleverd door het construeren van waarheidstabellen of door directe toepassing van de semantische definities van conjunctie en disjunctie.

Dankzij associativiteit en commutativiteit kunnen we haakjes weglaten bij ketens van conjuncties of disjuncties (zolang alle operatoren hetzelfde zijn) en kunnen we operanden in willekeurige volgorde schrijven. Bijvoorbeeld: P ∧ Q ∧ R is ondubbelzinnig en P ∧ Q ∧ R ≡ R ∧ P ∧ Q.

# Identiteitswetten, Dubbele Negatie en Idempotentie

Stelling 3.6 (Identiteitswetten):

1. P ∧ T ≡ P (T is het identiteitselement voor ∧)
2. P ∨ F ≡ P (F is het identiteitselement voor ∨)
3. P ∧ F ≡ F (F is het annihilerende element voor ∧)
4. P ∨ T ≡ T (T is het annihilerende element voor ∨)

Stelling 3.7 (Dubbele negatie): ¬¬P ≡ P

Stelling 3.8 (Idempotentie):

1. P ∧ P ≡ P
2. P ∨ P ≡ P

Deze wetten kunnen eenvoudig worden bewezen met waarheidstabellen.

Bewijs (Dubbele negatie):

Aangezien de kolommen voor P en ¬¬P identiek zijn, is bewezen dat ¬¬P ≡ P.

# Contraposities, Inverse en Converse

Voor implicaties zijn er verschillende verwante formules die belangrijk zijn om te onderscheiden:

Definitie 3.9: Voor een implicatie P → Q definiëren we:

1. De contrapositie: ¬Q → ¬P
2. De inverse: ¬P → ¬Q
3. De converse: Q → P

Een belangrijk resultaat in de propositielogica is dat een implicatie logisch equivalent is aan haar contrapositie:

Stelling 3.10: P → Q ≡ ¬Q → ¬P

Bewijs:

De kolommen voor P → Q en ¬Q → ¬P zijn identiek, wat bewijst dat de formules logisch equivalent zijn.

De inverse en converse van een implicatie zijn echter over het algemeen niet equivalent aan de oorspronkelijke implicatie. Ze zijn wel equivalent aan elkaar:

Stelling 3.11: (Q → P) ≡ (¬P → ¬Q)

Dit kan op dezelfde manier worden bewezen met een waarheidstabel.

Voorbeeld: Voor de implicatie "Als het regent, dan is de straat nat", hebben we:

• Contrapositie: "Als de straat niet nat is, dan regent het niet" (equivalent aan de oorspronkelijke implicatie)
• Inverse: "Als het niet regent, dan is de straat niet nat" (niet noodzakelijk waar)
• Converse: "Als de straat nat is, dan regent het" (niet noodzakelijk waar; de straat kan nat zijn door andere oorzaken)

# Bewijstechnieken

# Semantisch Bewijs met Waarheidstabellen

Een van de eenvoudigste manieren om beweringen in propositielogica te bewijzen is door middel van waarheidstabellen. Deze methode is gebaseerd op de semantische definitie van logische geldigheid en is altijd sluitend voor de propositielogica (omdat er een eindig aantal mogelijke interpretaties zijn).

Procedure voor semantisch bewijs:

1. Identificeer de premissen (P₁, P₂, ..., Pₙ) en de conclusie (Q).
2. Construeer een waarheidstabel voor alle mogelijke interpretaties van de atomaire proposities.
3. Controleer of bij elke interpretatie waar alle premissen waar zijn (P₁ ∧ P₂ ∧ ... ∧ Pₙ = T), ook de conclusie waar is (Q = T).

Definitie 4.1: Een argument is semantisch geldig als en slechts als de conclusie een semantisch gevolg is van de premissen.

Voorbeeld: Bewijs de geldigheid van het volgende argument:

1. P → Q
2. P
3. Daarom, Q

We kijken alleen naar rijen waar beide premissen waar zijn, wat alleen in de eerste rij het geval is. In die rij is de conclusie Q ook waar, dus het argument is geldig. Dit bevestigt de regel van modus ponens.

Een variant van deze methode kan worden gebruikt om te bewijzen dat een enkele formule een tautologie is door te verifiëren dat de formule waar is onder alle interpretaties.

# Formele Afleiding in Natuurlijke Deductie

Naast de semantische benadering kunnen we ook syntactische bewijsmethoden gebruiken, die vaak krachtiger zijn bij het werken met complexere logische systemen. Natuurlijke deductie is zo'n syntactisch bewijssysteem dat formele afleidingen mogelijk maakt zonder afhankelijk te zijn van waarheidstabellen.

In een natuurlijk deductiesysteem voor propositielogica hebben we afleidingsregels die ons in staat stellen om vanuit premissen naar conclusies te redeneren.

Definitie 4.2: Een afleidingsregel is een syntactisch patroon dat ons toestaat om vanuit bepaalde formules (de premissen van de regel) een nieuwe formule (de conclusie van de regel) af te leiden.

Enkele fundamentele afleidingsregels in natuurlijke deductie zijn:

1. Modus Ponens (MP):

   P → Q
   P
   ------
   Q

2. Modus Tollens (MT):

   P → Q
   ¬Q
   ------
   ¬P

3. Conjunctie-introductie (∧I):

   P
   Q
   ------
   P ∧ Q

4. Conjunctie-eliminatie (∧E):

   P ∧ Q
   ------
   P

   en

   P ∧ Q
   ------
   Q

5. Disjunctie-introductie (∨I):

   P
   ------
   P ∨ Q

   en

   Q
   ------
   P ∨ Q

6. Disjunctie-eliminatie (∨E) (ook bekend als bewijs per casus):

   P ∨ Q
   P → R
   Q → R
   ------
   R

7. Dubbele negatie (DN):

   P
   ------
   ¬¬P

   en

   ¬¬P
   ------
   P

8. Reductio ad Absurdum (RAA) (bewijs door contradictie):

   [¬P]
   ...
   Q ∧ ¬Q
   ------
   P

   Hier betekent [¬P] dat we ¬P als een tijdelijke aanname nemen.

Voorbeeld van een formele afleiding: Bewijs: (P → Q) ∧ (Q → R) ⊢ (P → R)

1. (P → Q) ∧ (Q → R)    [Premisse]
2. P → Q                [∧E, 1]
3. Q → R                [∧E, 1]
4. [P]                  [Aanname]
5.  Q                   [MP, 2, 4]
6.  R                   [MP, 3, 5]
7. P → R                [→I, 4-6]

In deze afleiding beginnen we met de premisse (P → Q) ∧ (Q → R). Op regels 2 en 3 passen we conjunctie-eliminatie toe om de individuele implicaties te verkrijgen. Vervolgens nemen we P aan (regel 4) om een implicatie te bewijzen. Met herhaalde toepassing van modus ponens leiden we R af (regels 5-6). Ten slotte, aangezien we R hebben afgeleid onder de aanname P, kunnen we de implicatie P → R concluderen (regel 7).

# Reductio ad Absurdum

Reductio ad absurdum (RAA), ook bekend als bewijs door contradictie, is een krachtige bewijstechniek in de propositielogica. Deze techniek is gebaseerd op het principe dat als de ontkenning van een propositie leidt tot een contradictie, de propositie zelf waar moet zijn.

Procedure voor bewijs door contradictie:

1. Neem aan dat de te bewijzen propositie P onwaar is, dus ¬P is waar.
2. Leid uit deze aanname, eventueel samen met andere premissen, een contradictie af (een stelling van de vorm Q ∧ ¬Q).
3. Concludeer dat de aanname ¬P onwaar moet zijn, en dus P waar is.

Voorbeeld: Bewijs dat P → (Q → P) een tautologie is.

1. [¬(P → (Q → P))]       [Aanname voor contradictie]
2. P ∧ ¬(Q → P)           [¬(A → B) ≡ A ∧ ¬B, 1]
3. P                      [∧E, 2]
4. ¬(Q → P)               [∧E, 2]
5. Q ∧ ¬P                 [¬(A → B) ≡ A ∧ ¬B, 4]
6. ¬P                     [∧E, 5]
7. P ∧ ¬P                 [∧I, 3, 6]
8. P → (Q → P)            [RAA, 1-7]

In deze afleiding nemen we aan dat P → (Q → P) niet waar is. Door logische equivalenties en eliminatieregels toe te passen, leiden we een contradictie af (P ∧ ¬P). Dit bewijst dat onze aanname onwaar is, en dus dat P → (Q → P) waar is onder alle interpretaties, ofwel een tautologie is.

# Toepassingen in de Informatica

# Conditionele Expressies en Boolean Algebra

Propositielogica vormt de theoretische basis voor Boolean algebra, wat direct wordt toegepast in de evaluatie van conditionele expressies in programmeertalen en het ontwerp van digitale schakelingen.

Conditionele expressies in programmeertalen zijn directe implementaties van propositielogische formules:

// Java voorbeeld
boolean isEligible = (age >= 18) && (isRegistered || hasExemption);

In dit voorbeeld worden de logische operatoren && (conjunctie), || (disjunctie) en impliciete vergelijkingsoperatoren gebruikt om een complexe Boolean expressie te construeren die wordt geëvalueerd volgens dezelfde semantiek als de propositielogica.

Short-circuit evaluatie in veel programmeertalen is gebaseerd op logische equivalenties:

• Voor P ∧ Q: Als P onwaar is, is de gehele conjunctie onwaar, ongeacht Q.
• Voor P ∨ Q: Als P waar is, is de gehele disjunctie waar, ongeacht Q.

Dit leidt tot efficiëntere evaluatie en stelt programmeurs in staat om veilige conditionele constructies te schrijven:

// Veilige toegang tot potentieel null-referentie
if (object != null && object.method() > 0) {
    // Verwerking
}

Hardware-implementatie: De logische poorten in digitale circuits implementeren Boolean functies:

• AND-poort implementeert conjunctie
• OR-poort implementeert disjunctie
• NOT-poort implementeert negatie
• XOR-poort implementeert exclusieve disjunctie

Booleaanse expressies kunnen worden geoptimaliseerd met behulp van logische equivalenties, wat leidt tot efficiëntere schakelingen:

(A ∧ B) ∨ (A ∧ ¬B) ≡ A ∧ (B ∨ ¬B) ≡ A ∧ T ≡ A

Deze vereenvoudiging, gebaseerd op distributiviteit en complementwet, reduceert een complexe schakeling tot een enkele doorlaat voor signaal A.

# SAT-solvers

Het satisfiability probleem (SAT) vraagt of er een toekenning van waarheidswaarden bestaat voor de variabelen in een propositielogische formule zodanig dat de formule waar wordt.

Definitie 5.1: Een formule φ is satisfiable als er ten minste één interpretatie I bestaat zodanig dat I(φ) = T.

SAT is het eerste probleem dat werd bewezen NP-volledig te zijn (Cook-Levin theorema). Dit betekent dat veel belangrijke computationele problemen kunnen worden omgezet naar een SAT-probleem.

Modern SAT-solvers gebruiken geavanceerde algoritmen zoals:

• DPLL (Davis-Putnam-Logemann-Loveland) algoritme
• CDCL (Conflict-Driven Clause Learning)
• Lokale zoekalgoritmen zoals WalkSAT

Toepassingen van SAT-solvers:

1. Hardware-verificatie: Controleren of een circuit aan bepaalde specificaties voldoet.
2. Software-verificatie: Controleren op bugs en garanderen van programma-eigenschappen.
3. AI-planning: Omzetten van planningsproblemen naar SAT-formules en deze oplossen.
4. Bioinformatica: Problemen zoals vouwing van eiwitten en genetische analyse.
5. Cryptanalyse: Het breken van cryptografische algoritmen door SAT-encoding.

Voorbeeld: Een eenvoudig SAT-probleem

Beschouw de formule: (P ∨ Q) ∧ (¬P ∨ R) ∧ (¬Q ∨ ¬R)

Is deze formule vervulbaar? We kunnen dit controleren met een waarheidstabel:

We zien dat de formule vervulbaar is met ten minste twee verschillende waardetoekenningen: (P=T, Q=F, R=T) en (P=F, Q=T, R=F).

# Compilerbouw en Typechecking

Propositielogica speelt een belangrijke rol in verschillende fasen van compilerbouw:

1. Parseren: Expressies in programmeertalen worden geparseerd volgens formele grammatica's, waarbij logische operatoren specifieke precedentie en associativiteit hebben, vergelijkbaar met de syntactische regels van propositielogica.

2. Type-checking: Moderne typesystemen gebruiken propositionele en predicatenlogica om type-constraints uit te drukken en op te lossen:

   // TypeScript voorbeeld met union types
   type Result<T, E> = Success<T> | Error<E>;
   
   function isSuccess<T, E>(result: Result<T, E>): result is Success<T> {
    return 'value' in result;
   }

   Hier wordt de typevariable result verfijnd op basis van een logische propositie ('value' in result).

3. Controlestroom-analyse: Compilers gebruiken propositielogica om bereikbaarheidsanalyse uit te voeren:

   if (x > 0 && dead_code()) { ... }

   Een slimme compiler kan concluderen dat als x <= 0, de tweede conditie nooit wordt geëvalueerd.

4. Constante propagatie: Logische regels worden gebruikt om expressies te evalueren:

   if (constant == true || variable) { ... }

   Dit kan worden vereenvoudigd tot if (true) { ... } door toepassing van de regel P ∨ Q ≡ T als P ≡ T.

# Formele Verificatie en Model Checking

Formele verificatie is het proces van het rigoreus controleren of een systeem voldoet aan een formele specificatie. Propositielogica dient als basis voor complexere logische systemen die worden gebruikt in formele verificatie, zoals temporele logica en Hoare-logica.

Model checking is een specifieke formele verificatietechniek waarbij:

1. Het systeem wordt gemodelleerd als een eindige-toestandsautomaat.
2. De specificaties worden uitgedrukt in een logische taal (vaak temporele logica).
3. Een algoritme bepaalt of het model voldoet aan de specificatie.

Voorbeeld: Verifiëren van een eenvoudig protocol

Beschouw een eenvoudig mutex-protocol voor twee processen P₁ en P₂:

• Propositie enter₁: P₁ betreedt de kritieke sectie
• Propositie enter₂: P₂ betreedt de kritieke sectie
• Propositie in₁: P₁ is in de kritieke sectie
• Propositie in₂: P₂ is in de kritieke sectie

We willen verifiëren dat het systeem voldoet aan wederzijdse uitsluiting: ¬(in₁ ∧ in₂).

Door alle mogelijke toestanden van het model te controleren en de overgangen te evalueren op basis van de protocolspecificatie, kan model checking automatisch bepalen of deze eigenschap altijd geldt.

# Toegangscontrole en Beveiliging

Propositielogica wordt gebruikt in toegangscontrolesystemen om machtigingsregels en beveiligingsbeleid te modelleren:

Access Control Lists (ACLs) kunnen worden geïnterpreteerd als disjuncties van conjuncties:

access(resource) ≡ (user=admin) ∨ (user=owner ∧ resource=private) ∨ (authenticated=true ∧ resource=public)

Role-Based Access Control (RBAC) gebruikt logische expressies om te bepalen of een gebruiker toegang heeft:

canAccess(u, resource) ≡ ∃r(hasRole(u, r) ∧ permitsAccess(r, resource))

Security Policies worden vaak uitgedrukt als een reeks regels, waarbij elke regel is geformuleerd als een propositielogische formule. Bijvoorbeeld, om een firewall te configureren:

allowTraffic ≡ (srcIP=local ∧ dstPort!=22) ∨ (protocol=HTTPS ∧ authenticated=true)

Formele analyse van beveiliging stelt ons in staat om te bewijzen dat een beveiligingsbeleid bepaalde eigenschappen heeft, zoals:

• Volledigheid: Elk verzoek wordt expliciet toegestaan of geweigerd.
• Consistentie: Er zijn geen tegenstrijdige regels.
• Minimaliteit: Er zijn geen redundante regels.

# Geavanceerde Concepten

# Normaalvormen

In de propositielogica kunnen formules worden gerepresenteerd in verschillende standaardvormen, wat nuttig is voor algoritmische manipulatie en analyse:

Definitie 6.1: Een formule is in Conjunctieve Normaalvorm (CNF) als het een conjunctie is van disjuncties van literalen (een atomaire propositie of de negatie daarvan).

Algemene vorm: (l₁₁ ∨ l₁₂ ∨ ... ∨ l₁ₘ) ∧ (l₂₁ ∨ l₂₂ ∨ ... ∨ l₂ₙ) ∧ ... ∧ (lₖ₁ ∨ lₖ₂ ∨ ... ∨ lₖₚ)

Voorbeeld: (P ∨ Q) ∧ (¬P ∨ R) is in CNF.

Definitie 6.2: Een formule is in Disjunctieve Normaalvorm (DNF) als het een disjunctie is van conjuncties van literalen.

Algemene vorm: (l₁₁ ∧ l₁₂ ∧ ... ∧ l₁ₘ) ∨ (l₂₁ ∧ l₂₂ ∧ ... ∧ l₂ₙ) ∨ ... ∨ (lₖ₁ ∧ lₖ₂ ∧ ... ∧ lₖₚ)

Voorbeeld: (P ∧ ¬Q) ∨ (¬P ∧ R) is in DNF.

Stelling 6.3: Elke propositielogische formule kan worden omgezet naar CNF en naar DNF.

Procedure voor conversie naar CNF:

1. Elimineer implicaties en equivalenties:
   • P → Q wordt vervangen door ¬P ∨ Q
   • P ↔ Q wordt vervangen door (P → Q) ∧ (Q → P), wat verder wordt omgezet in (¬P ∨ Q) ∧ (¬Q ∨ P)
2. Verplaats negaties naar binnen met De Morgan's wetten:
   • ¬(P ∧ Q) wordt vervangen door ¬P ∨ ¬Q
   • ¬(P ∨ Q) wordt vervangen door ¬P ∧ ¬Q
   • ¬¬P wordt vervangen door P
3. Pas distributieve wetten toe om een conjunctie van disjuncties te verkrijgen:
   • P ∨ (Q ∧ R) wordt vervangen door (P ∨ Q) ∧ (P ∨ R)

Voorbeeld: Converteer P → (Q ∨ R) naar CNF.

P → (Q ∨ R)
≡ ¬P ∨ (Q ∨ R)         [Eliminatie van implicatie]
≡ ¬P ∨ Q ∨ R           [Associativiteit van disjunctie]

De formule is nu in CNF, aangezien het een enkele disjunctie van literalen is.

Voordelen van normaalvormen:

• Algoritmische bewerking: Veel algoritmen, zoals SAT-solvers, werken efficiënter met formules in normaalvorm.
• Standaardisatie: Normaalvormen bieden een uniforme representatie, wat vergelijking van formules vereenvoudigt.
• Theoretische inzichten: Bepaalde eigenschappen van formules zijn gemakkelijker te analyseren in normaalvorm.

# Beslissingsprocedures

Een beslissingsprocedure is een algoritme dat bepaalt of een logische formule geldig, vervulbaar, of onvervulbaar is. Voor propositielogica zijn er verschillende beslissingsprocedures:

1. Waarheidstabellen: De eenvoudigste beslissingsprocedure is het construeren van een volledige waarheidstabel, wat werkt voor formules met een klein aantal atomaire proposities. Complexiteit: O(2ⁿ), waar n het aantal verschillende atomaire proposities is.

2. Davis-Putnam-Logemann-Loveland (DPLL) algoritme: Een efficiënter algoritme voor het SAT-probleem, gebaseerd op:

• Unit propagation: Als een clausule uit één literal bestaat, ken de juiste waarde toe aan die variabele.
• Pure literal elimination: Als een variabele alleen in positieve of alleen in negatieve vorm voorkomt, ken de waarde toe die de respectievelijke literalen waar maakt.
• Branching: Kies een variabele en probeer beide mogelijke waardetoekenningen.

3. Conflict-Driven Clause Learning (CDCL): Een verbetering van DPLL die "leert" van conflicten om toekomstige zoekpaden te snoeien, wat tot significante prestatieverbetering leidt bij veel praktische SAT-instanties.

4. Binary Decision Diagrams (BDDs): Een datastructuur die propositielogische formules representeert als een gerichte acyclische graaf, waarmee efficiënte operaties op Booleaanse functies kunnen worden uitgevoerd.

Hoewel het SAT-probleem NP-compleet is (en dus in het algemeen exponentiële tijd vereist in de slechtste gevallen), kunnen moderne SAT-solvers opmerkelijk efficiënt zijn voor veel praktische probleeminstanties, wat hun wijdverbreide toepassing in industrie en onderzoek verklaart.

# Koppeling met Predicatenlogica

Propositielogica, hoewel krachtig voor veel toepassingen, heeft beperkingen. Het kan interne structuur binnen proposities niet vertegenwoordigen en kan niet kwantificeren over objecten. Predicatenlogica (ook bekend als eerste-orde logica) breidt propositielogica uit om deze beperkingen te overwinnen:

Uitbreidingen in predicatenlogica:

1. Termen en Predicaten: In plaats van atomaire proposities gebruikt predicatenlogica predicaten met termen als argumenten.

   Propositielogica: P (Jan is lang)
   Predicatenlogica: Lang(jan) (Jan is lang)

2. Kwantoren:

   • Universele kwantor (∀): "voor alle"
   • Existentiële kwantor (∃): "er bestaat"

     ∀x(Student(x) → Studeert(x))  // Alle studenten studeren
     ∃x(Student(x) ∧ Speelt(x, gitaar))  // Er bestaat een student die gitaar speelt

3. Functies:

   Vader(jan)  // Verwijst naar de vader van Jan
   Plus(x, y)  // Verwijst naar de som van x en y

Relatie tussen propositielogica en predicatenlogica:

1. Propositielogica als subset: Elke propositielogische formule is ook een formule in predicatenlogica (zonder kwantoren en met 0-aire predicaten).

2. Proposititionalisatie: In sommige gevallen kan een probleem in predicatenlogica worden omgezet naar propositielogica door alle mogelijke instantiaties van kwantoren te genereren. Dit werkt alleen voor eindig domein.

3. Herbrand-semantiek: Een benadering om redeneertechnieken uit propositielogica toe te passen op predicatenlogica.

Voorbeeld: Herbrand-expansie van ∀x(P(x) → Q(x)) over domein {a, b}:

(P(a) → Q(a)) ∧ (P(b) → Q(b))

Computationele aspecten:

• Het vervulbaarheidsprobleem in propositielogica is NP-compleet (beslisbaar, maar vermoedelijk niet in polynomiale tijd).
• Het vervulbaarheidsprobleem in predicatenlogica is onbeslisbaar (er bestaat geen algoritme dat voor elke predicatenlogische formule in eindige tijd bepaalt of deze vervulbaar is).

# Oefeningen

# Oefening 1: Waarheidstabellen en Tautologieën

Construct waarheidstabellen voor de volgende formules en bepaal of ze tautologieën, contradicties of contingent zijn:

a) P → (Q → P) b) (P → Q) → P c) (P → Q) ∨ (Q → P) d) (P → Q) ∧ (Q → P) ↔ (P ↔ Q) e) [P → (Q → R)] ↔ [(P ∧ Q) → R]

# Oefening 2: Logische Equivalentie

Bewijs of weerleg de volgende logische equivalenties, zowel met waarheidstabellen als met algebraïsche manipulatie:

a) (P → Q) ≡ (¬P ∨ Q) b) ¬(P → Q) ≡ (P ∧ ¬Q) c) (P → Q) ∧ (P → R) ≡ P → (Q ∧ R) d) (P → Q) ∨ (P → R) ≡ P → (Q ∨ R) e) (P → R) ∧ (Q → R) ≡ (P ∨ Q) → R

# Oefening 3: Normaalvormen

Converteer de volgende formules naar zowel CNF als DNF:

a) P → (Q ∧ R) b) (P ∨ Q) → R c) (P → Q) → R d) P ↔ (Q ∨ R) e) ¬(P ∧ Q) → (P ∨ R)

# Oefening 4: Formele Afleiding

Gebruik natuurlijke deductie om de volgende stellingen te bewijzen:

a) (P → Q), (Q → R) ⊢ (P → R) b) P → Q ⊢ ¬Q → ¬P (contrapositiviteit) c) (P ∧ Q) → R ⊢ P → (Q → R) d) ⊢ ((P → Q) → P) → P (Wet van Peirce) e) (P ∨ Q), ¬P ⊢ Q (disjunctief syllogisme)

# Oefening 5: Toepassingen in de Informatica

1. Boolean Expressies in Programmeertalen
   Schrijf een programma in een programmeertaal naar keuze (bijvoorbeeld Python, Java of C++) dat een complexe Boolean expressie evalueert, zoals (A ∧ ¬B) ∨ (C ∧ (A → B)). Geef een uitleg hoe de evaluatie overeenkomt met de semantiek van propositielogica.

2. SAT-probleem
   Gegeven de formule (P ∨ ¬Q) ∧ (Q ∨ R) ∧ (¬P ∨ ¬R):
   a. Bepaal handmatig of de formule satisfiable is door een waarheidstabel te construeren.
   b. Geef een toekenning van waarheidswaarden die de formule waar maakt, indien mogelijk.
   c. Beschrijf hoe een SAT-solver zoals DPLL dit probleem zou aanpakken.

3. Typechecking
   In een programmeertaal met statische typering (zoals TypeScript of Haskell), definieer een type dat een waarde kan zijn die alleen waar is als de waarde een string of een getal is. Schrijf een functie die controleert of een waarde aan deze voorwaarde voldoet en leg uit hoe propositielogica wordt gebruikt in de typechecking-logica.

4. Formele Verificatie
   Modelleer een eenvoudig verkeerslichtsysteem met twee toestanden (rood, groen) en een specificatie dat beide lichten nooit tegelijk groen mogen zijn. Gebruik propositielogica om deze eigenschap te formaliseren en beschrijf hoe een model checker deze eigenschap zou verifiëren.

5. Toegangscontrole
   Ontwerp een toegangscontrolesysteem voor een bestandssysteem waarbij een gebruiker toegang heeft als:

   • Ze een admin zijn, of
   • Ze de eigenaar van het bestand zijn en het bestand niet gemarkeerd is als alleen-lezen.
     Formuleer dit beleid in propositielogica en toon aan dat het beleid volledig en consistent is door middel van een waarheidstabel.

# Verder Lezen

Voor wie zich verder wil verdiepen in propositielogica en de toepassingen ervan in de informatica, zijn de volgende bronnen waardevol:

1. Boeken:

   • Logic in Computer Science: Modelling and Reasoning about Systems door Michael Huth en Mark Ryan. Een uitgebreide inleiding tot logica met een focus op toepassingen in informatica.
   • Mathematical Logic for Computer Science door Mordechai Ben-Ari. Dit boek behandelt propositielogica, predicatenlogica en hun computationele aspecten.
   • Introduction to Automata Theory, Languages, and Computation door John E. Hopcroft, Rajeev Motwani en Jeffrey D. Ullman. Bevat relevante secties over logica in de context van theoretische informatica.
   • Computer Architecture: A Quantitative Approach door John L. Hennessy en David A. Patterson. Behandelt Boolean algebra en digitale circuits in detail.

2. Online Bronnen:

   • Stanford Encyclopedia of Philosophy: De artikelen over Propositional Logic en Logic and Artificial Intelligence bieden een filosofische en technische inleiding.
   • MIT OpenCourseWare: Cursussen zoals Mathematics for Computer Science bevatten modules over logica en bewijstechnieken.
   • Coursera/EdX: Cursussen zoals Introduction to Logic (Stanford) of Logic and Computational Thinking (Microsoft) bieden interactieve leertrajecten.

3. Software en Tools:

   • SAT-solvers: MiniSAT, Z3 (Microsoft Research), en Glucose zijn open-source tools om SAT-problemen op te lossen.
   • Model Checkers: Tools zoals SPIN en NuSMV worden gebruikt voor formele verificatie van systemen.
   • Logica Simulators: LogiSim en DigitalJS voor het visualiseren en simuleren van digitale circuits gebaseerd op propositielogica.

4. Academische Artikelen:

   • Cook, S. A. (1971). The Complexity of Theorem-Proving Procedures. Dit artikel introduceert de NP-volledigheid van SAT.
   • Davis, M., & Putnam, H. (1960). A Computing Procedure for Quantification Theory. Beschrijft een vroege versie van het DPLL-algoritme.
   • Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model Checking. Een standaardwerk over model checking technieken.

5. Gemeenschappen:

   • Stack Exchange: De Computer Science en Mathematics Stack Exchange communities hebben actieve discussies over logica en informatica.
   • Reddit: Subreddits zoals r/compsci en r/logic bieden informele discussies en vragen over propositielogica.

# Referenties

1. Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
2. Ben-Ari, M. (2012). Mathematical Logic for Computer Science. Springer.
3. Hopcroft, J. E., Motwani, R., & Ullman, J. D. (2006). Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.
4. Hennessy, J. L., & Patterson, D. A. (2011). Computer Architecture: A Quantitative Approach. Morgan Kaufmann.
5. Cook, S. A. (1971). The Complexity of Theorem-Proving Procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, 151–158.
6. Davis, M., & Putnam, H. (1960). A Computing Procedure for Quantification Theory. Journal of the ACM, 7(3), 201–215.
7. Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model Checking. MIT Press.
8. Stanford Encyclopedia of Philosophy. (2023). Propositional Logic. Beschikbaar op: https://plato.stanford.edu/entries/logic-propositional/
9. Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2009). Handbook of Satisfiability. IOS Press.