Afleidingen in propositie- en predicatenlogica

Achtergrond

Om zorgvuldig te redeneren over programma's en systemen leggen we de toegestane redeneerstappen vast met behulp van logische afleidingsregels. Het formeel vastleggen van de redeneerregels heeft als extra voordeel dat we ook wat kunnen bewijzen over de verzameling afleidbare formules. Verder kunnen we de afleidingsregels ook operationaliseren door een computerprogramma te schrijven dat ons helpt bij het checken van redeneringen (bewijschecker) of dat helpt bij het geven van correcte bewijzen (bewijsassistent).

De regels voor propositie- en predicatenlogica zijn aan de orde gekomen in de cursus Beweren en Bewijzen. We gaan ons hiermee nader vertrouwd maken.

Leerdoel

Na het voltooien van deze taak kunt u

• afleidingen maken in de predicatenlogica met behulp van de natuurlijke-deductieregels;
• onderscheid maken tussen constructieve en niet-constructieve afleidingen;
• de noodzaak van randvoorwaarden bij de regels voor de kwantoren uitleggen;
• het begrip 'afleidbare regel' uitleggen; in een eenvoudige situatie laten zien dat een gegeven regel afleidbaar is.

Instructie

1. Lees secties 4.2 en 10.1 uit Logica voor Informatici: bestudeer de logische afleidingsregels en de gegeven voorbeelden. De afleidingsregels van de natuurlijke deductie kunt u terugvinden in de samenvatting.
2. Maak afleidingen van de volgende formules volgens de gegeven afleidingsregels.
   NB. de existentiele en universele kwantor worden genoteerd als E en A; ze binden sterker dan de propositionele connectieven.
   1. B \/ (C/\D) |- (B \/ C) /\ (B \/ D)
      (Distributiviteit van \/ over /\.)
   2. (B -> C) -> B |- B \/ ¬C
      (Hint: neem eens C aan.)
   3. Ax.(P(x) -> Ey.Q(y)) |- Ex.P(x) -> Ey.Q(y)
   4. ¬Ax.P(x) |- Ex.¬P(x)
3. Ga na welke afleidingen gebruik maken van de ¬E* regel ('bewijs uit het ongerijmde'). Dit noemen we ook wel niet-constructieve afleidingen.
4. Neem de randvoorwaarden in de E-eliminatieregel (sectie 10.1) nog eens onder de loep. Geef een formule f en een 'afleiding' voor f waarin deze randvoorwaarden overtreden worden. Leg uit dat deze afleiding ontoelaatbaar is, d.w.z. dat de conclusie "f is afleidbaar" een tegenspraak oplevert.
5. Lees de uitleg over afleidbare regels.
6. De \/-eliminatieregel vindt men soms moeilijk in het gebruik. Er is een alternatief: de \/-E* regel die in de bijlage vermeld is. Bewijs dat de \/-E* regel een afleidbare regel is in het systeem van natuurlijke deductie. Is de afleiding die dit aantoont constructief? (De \/-E regel is ook afleidbaar uit de \/-E* regel, maar dat is een stuk lastiger en doen we niet.)
7. Maak (voor 22 november) tenminste 20 opgaven in Proofweb van niveau >Medium: 10 van "propositielogica" en 10 van "predicatenlogica.

Product

• Afleidingen van de gegeven formules.
• Aanduiding van de niet-constructieve stappen.
• Een 'illegale' afleiding en uitleg waarom de door u 'afgeleide' formule niet afleidbaar is.
• Afleiding van de \/-E* regel. Analyse van het constructieve gehalte.
• 15 opgaven in Proofweb

Reflectie

• Gebruikt u de afleidingsstappen uit de bijlage? Is het bij elke stap duidelijk welke regel gebruikt is? Wordt aan de randvoorwaarden bij de regels voldaan?
• De afleidingsstijl van Van Benthem (en ook in de bijlage) is wat minder verbose dan de stijl die in de cursus Beweren en Bewijzen gepropageerd wordt. Zou u de gegeven bewijzen gemakkelijk kunnen omzetten in B&B-stijl?
• Is uw redenering over het niet-afleidbaar zijn van de formule f kernachtig en maakt u gebruik van bekende resulaten? Heeft u een concreet tegenmodel geconstrueerd?
• Zijn de opgaven in Proofweb door de computer geverifieerd. Begrijp je het bewijs zelf ook?