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 inleiding 
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 semantiek 
Als men over propositielogica spreekt, heeft men het meestal over de klassieke propositielogica. Hieronder wordt de syntaxis en semantiek van deze logica gegeven.

Formules 
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 .

Valuaties 
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 vervulbaarheid 
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.

Identiteitswet 
Zijn  en  proposities met  en , dan is:
 
 
Deze equivalenties vormen de identiteitswet van de propositielogica.

Waarheidstabellen 

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:

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.

Bewijssystemen 
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 Hilbert 
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:

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

Semantische tableaus 

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 deductie 

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).

Resolutie 

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.

Complexiteitstheorie 
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.

Logica
Theoretische informatica
Booleaanse algebra