Leertaak 10

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

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

Product

Reflectie