Axiomatische logica: Hilbert's systeem

Propositielogica: Hilbert's deductief systeem

Axiomatische logica: Hilbert's systeem

Hilbert's deductief systeem, of kortweg Hilbert's systeem, is een voorbeeld van de axiomatisch bewijssysteem waarin een aantal axioma's als uitgangspunt gekozen wordt en uit die axioma's m.b.v afleidingsregels nieuwe formules worden afgeleid. Hilbert's deductief schema is een relatief eenvoudig systeem: er zijn hierin maar drie axioma's en één afleidingsregel (Modus Ponens).

Hilbert's systeem Logische formules van de volgende vormen zijn de axioma's van Hilbert's systeem: \[\begin{array}{ll} \varphi\rightarrow(\psi\rightarrow \chi) & \text{Axioma a} \\[0.2cm] \bigl(\varphi\rightarrow(\psi\rightarrow \chi)\bigr)\rightarrow \bigl(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow \chi)\bigr) & \text{Axioma b} \\[0.2cm] (\neg\,\varphi\rightarrow \neg\,\psi)\rightarrow (\psi\rightarrow \varphi)& \text{Axioma c}\end{array}\] Niets anders is een axioma.

Hilbert's systeem kent slechts één afleidingsregel, namelijk Modus Ponens (\(\mathrm{MP}\)):

Als \(\varphi\) is afgeleid en \(\varphi\rightarrow \psi\) is afgeleid, dan is ook \(\psi\) afgeleid.

Voorbeelden van axioma's Er zijn oneindig veel axioma's, bijvoorbeeld zijn voor propositievariabelen \(p\), \(q\) en \(r\) de volgende formules nieuwe axioma's: \[\begin{aligned} p\rightarrow(p\rightarrow p) & \quad\text{Axioma a met }\varphi=\psi=\chi=p\\ (p\rightarrow q) \rightarrow (p\rightarrow (q\rightarrow p) & \quad\text{Axioma b met }\varphi=\chi=p, \psi=q\\ \bigl (\neg\neg\,p\rightarrow \neg(q\rightarrow r)\bigr)\rightarrow \bigl((q\rightarrow r)\rightarrow \neg\,p\bigr)&\quad \text{Axioma c met }\varphi=\neg\,p, \psi=q\rightarrow r\end{aligned}\]

Afleiding in een deductief systeem Een afleiding uit een formuleverzameling \(\Sigma\) is een eindig genummerd rijtje formules, waarbij geldt: elke formule in het rijtje is een axioma, of een formule uit \(\Sigma\), of een formule die met behulp van een afleidingsregel is verkregen uit voorafgaande formules in het rijtje. Een afleiding binnen een deductief systeem waarbij geen extra premissen worden gebruikt noemen we een stelling.

We noteren afleidingen op een vergelijkbare manier als bij natuurlijke deductie, alleen hebben we nu axioma's en maar één afleidingsregel ter beschikking. Verder laten we alleen de connectieven \(\neg\) en \(\rightarrow\) toe want hiermee kunnen we conjunctie (\(\land\)) en disjunctie (\(\lor\)) respectievelijk introduceren als afkortingen via de definities \(\varphi\land\psi = \neg(\varphi\rightarrow \neg\,\psi\)) en \(\varphi\lor\psi = \neg\,\varphi\rightarrow \neg\, \psi\). De negatie \(\neg\,\varphi\) is ook te introduceren als \(\varphi\vdash\bot\). Een paar voorbeelden illustreren hoe afleidingen in Hilbert's systeem gaan.

Voorbeeld 1 Toon aan \(p\rightarrow q, q\rightarrow r, q\vdash r\).

Uitwerking: \[\begin{array}{l|ll} 1 & p\rightarrow q & (\mathrm{P)}\\ 2 & q\rightarrow r & (\mathrm{P}) \\ 3 & p & (\mathrm{P}) \\ 4 & q & \mathrm{MP}, 1, 3\\ 5 & r & \mathrm{MP}, 2, 4\end{array}\]

Voorbeeld 2 Toon aan \(\neg\, p\rightarrow \neg\,q, q\vdash p\).

Uitwerking: \[\begin{array}{l|ll} 1 & \neg\, p\rightarrow \neg\,q & (\mathrm{P)}\\ 2 & q & (\mathrm{P})\\ 3 & (\neg\,p\rightarrow \neg\, q)\rightarrow (q\rightarrow p) & \mathrm{Ax\;c} \\ 4 & q\rightarrow p & \mathrm{MP}, 1, 3 \\ 5 & p & \mathrm{MP}, 2, 4\end{array}\]

Voorbeeld 3 Toon aan dat voor elke formule \(\varphi\) het volgende geldt: \(\vdash \varphi\rightarrow \varphi\) .

Uitwerking: \[\begin{array}{l|ll} 1 & \varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr) & \mathrm{Ax\;a}\text{ met }(\varphi\rightarrow \varphi)\text{ voor }\psi\\ 2 & \Bigl(\varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr)\Bigr)\rightarrow \Bigl(\bigl(\varphi\rightarrow(\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow\varphi)\Bigr) & \mathrm{Ax\;b}\text{ met }(\varphi\rightarrow \varphi)\text{ voor }\psi\\ 3 & \bigl(\varphi\rightarrow (\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow \varphi) & \mathrm{MP}, 1, 2\\ 4 & \varphi\rightarrow (\varphi\rightarrow\varphi) & \mathrm{Ax\;a}\text{ met }\varphi\text{ voor }\psi\\ 5 & \varphi\rightarrow \varphi & \mathrm{MP}, 3, 4\end{array}\] Hoewel het bewijs van voor naar achter is opgeschreven, construeer je het in de omgekeerde richting. De formule \(\varphi\rightarrow \varphi\) is geen axioma, maar \(\varphi\rightarrow (\varphi\rightarrow\varphi)\) wel. Je bent dus klaar als je \(\bigl(\varphi\rightarrow (\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow \varphi)\) kunt aantonen. Maar dat volgt weer uit het axioma \(\Bigl(\varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr)\Bigr)\rightarrow \Bigl(\bigl(\varphi\rightarrow(\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow\varphi)\Bigr) \) plus het axioma \(\varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr) \) en klaar!

Hilbert's systeem gebruikt een minimum aan axioma's en redeneerregels. Het geven van een zo zuinig systeem heeft als voordeel dat redeneren over het systeem gemakkelijk is. Het nadeel is dat het leveren van afleidingen binnen het systeem in eerste instantie wat lastiger is dan bij een systeem zoals dat van natuurlijke deductie met meerdere afleidingsregels. Je moet nu eerst extra redeneer-hulpmiddelen gaan fabriceren: iedere stelling die je hebt bewezen mag vanaf dat moment worden gebruikt als ware het een axioma. Voorbeeld 3 is zo'n stelling die in verdere afleidingen gebruikt mag worden.

Handig bij afleidingen is ook onderstaande stelling.

Deductiestelling In Hilbert's system geldt voor een verzameling \(\Sigma\) van welgevormde formules (premissen, axioma's en afgeleide formules) en voor de formules \(\varphi\) en \(\psi\) het volgende: als \(\Sigma,\varphi\vdash \psi\) dan en slechts dan als \(\Sigma\vdash \varphi\rightarrow \psi\).

We bewijzen eerst dat \(\Sigma,\varphi\vdash \psi\) volgt uit \(\Sigma\vdash \varphi\rightarrow \psi\). Als \(\Sigma\vdash \varphi\rightarrow \psi\), dan ook \(\Sigma, \varphi \vdash \varphi\rightarrow \psi\). Omdat tevens \(\Sigma, \varphi\vdash \varphi\) krijgen we via Modus Ponens ook \(\Sigma,\varphi\vdash \psi\).

Het bewijs dat \(\Sigma\vdash \varphi\rightarrow \psi\) volgt uit \(\Sigma,\varphi\vdash \psi\) gaat met inductie naar de lengte van de afleiding van \(\psi\) uit \(\Sigma,\varphi\). We onderscheiden 3 gevallen:

\(\psi\in\Sigma\cup\{\varphi\}\). Dit splitst op in twee deelgevallen: als \(\psi\in\Sigma\), dan \(\Sigma \vdash \psi\), en als \(\psi=\varphi\), dan ook (volgens voorbeeld 3) \(\Sigma, \varphi\vdash \varphi\) en dus \(\Sigma, \varphi\vdash \psi\).
\(\psi\) is een axioma. Dan: \(\Sigma\vdash \psi\). Ook hebben we nog \(\psi\rightarrow (\varphi\rightarrow \psi)\) als instantie van Axioma a. Met Modus Ponens krijgen we dan \(\Sigma\vdash \varphi\rightarrow \psi\).
\(\Sigma,\varphi\vdash \psi\) komt via Modus Ponens uit een eerdere formule \(\chi\) via \(\Sigma,\varphi\vdash \chi\) en \(\Sigma,\varphi\vdash \chi\rightarrow \psi\). Hierop is de inductiehypothese van toepassing. We hebben dus: \(\Sigma\vdash \varphi\rightarrow \chi\) en \(\Sigma\vdash \varphi\rightarrow (\chi\rightarrow \psi)\). De afleiding voor \(\Sigma\vdash \varphi\rightarrow \psi\) gaat nu als volgt: \[\begin{array}{r|ll} \vdots & \vdots & \\ \vdots & \Sigma & \\ \vdots & \vdots & \\ k & \varphi\rightarrow \chi & \\ \vdots & \vdots & \\ l &\varphi\rightarrow (\chi\rightarrow \psi) & \\ l+1 & \bigl( \varphi\rightarrow (\chi\rightarrow \psi)\bigr)\rightarrow \bigl((\varphi\rightarrow \chi)\rightarrow (\varphi\rightarrow\psi)\bigr) & \mathrm{Ax\;b}\text{ met }\varphi\text{ en }\psi\text{ verwisseld}\\ l+2 & (\varphi\rightarrow \chi)\rightarrow (\varphi\rightarrow\psi) & \mathrm{MP}, l, l+1\\ l+2 & \varphi\rightarrow \psi & \mathrm{MP}, k, l+1\end{array}\]

De motivatie om op Hilbert's systeem in de verhandeling over propositielogica kort in te gaan vindt zijn oorsprong in de volgende stelling.

De afleiding \(\Sigma\vdash \varphi\) is in Hilbert' systeem dan en slechts dan mogelijk als de afleiding via natuurlijke deductie mogelijk is.

Bewijsschets Stel dat \(\Sigma\vdash \varphi\) aangetoond kan worden in Hilbert's systeem. Met inductie naar de lengte van een afleiding kan dan bewezen worden dat de afleiding ook via natuurlijke deductie gedaan kan worden omdat alle axioma's via natuurlijke deductie afgeleid kunnen worden en de implicatie eliminatieregel gebruikt kan worden om de Modus Ponens regel toe te passen.

Omgekeerd, als \(\Sigma\vdash \varphi\) aangetoond kan worden, dan kan via inductie naar de lengte van een afleiding bewezen worden dat de uitspraak ook aangetoond kan worden in Hilbert's systeem. Hierbij gebruik je de Deductiestelling en het feit dat de axioma's anders dan Axioma a en Axioma b in wezen hetzelfde zijn als redeneerregels bij natuurlijke deductie.