Beweren en bewijzen/supplement/planning (voor docenten)/het werk/taak/07
| Beweren en bewijzen: "redeneren op het hoogste niveau over gemaakte dingen". Gemaakte dingen kunnen ook regels en wetten zijn. En constitutionele kwesties. Bijvoorbeeld de regeling, wie de volgende koning (m/v) van Nederland wordt. We vertalen een stuk grondwet naar predikaatlogica. | 
|
Achtergrond
De Nederlandse grondwet bevat een fraai stukje specificatie in de geest van Beweren en bewijzen. Sommige dingen moeten absoluut zeker en ondubbelzinnig geregeld zijn, en met een domeinmodel dat geen ruimte laat voor interpretatie.
Het kan gebeuren dat op een onverwacht moment een bericht binnenkomt in het torentje bij het Binnenhof: de koning (m/v) is overleden. Het ergste wat men nu kan hebben is ruzie over de opvolging of populistische acties. En om dingen en mensen goed voor te kunnen bereiden, wil men liefst al ruim voor het overlijden van een koning zo goed mogelijk weten wie zijn opvolger wordt. Daarom heeft de wetgever het uiterste gedaan, de opvolging helder te regelen. Op elk moment moet vaststaan wie de troonopvolger is. Deze regeling is zo belangrijk dat ze in de grondwet staat.
Artikelen 25 t/m 26 specificeren voor elk willekeurig moment wie de opvolger van de koning zou worden als deze op dat moment zou overlijden. Laten we deze vermoedelijke troonopvolger kroonprins (m/v) noemen. Zolang een koning leeft is niet noodzakelijk steeds dezelfde persoon kroonprins. Als een koning overlijdt wordt de kroonprins koning en iemand anders kroonprins. Maar de tekst van de grondwet blijft altijd dezelfde! Door een altijd vastliggende tekst, die niet afhangt van een specifieke situatie wordt iets geregeld dat in de loop van de tijd op een grillige manier verandert.
Deze opdracht beperkt zich tot artikel 25:
|
Het koningschap gaat bij overlijden van de Koning krachtens erfopvolging over op zijn wettige nakomelingen, waarbij het oudste kind voorrang heeft, met plaatsvervulling volgens dezelfde regel. Bij gebreke van eigen nakomelingen gaat het koningschap op gelijke wijze over op de wettige nakomelingen eerst van zijn ouder, dan van zijn grootouder, in de lijn van erfopvolging, voor zover de overleden Koning niet verder bestaand dan in de derde graad van bloedverwantschap. |
Deze regeling uit de grondwet heeft een interessante eigenschap, die het vertalen naar predikaatlogica eenvoudiger maakt: er worden geen verschillende tijdspunten aan elkaar gepraat. Alle beweringen betreffen het "nu". Als nu die en die persoon koning is en nu die en die mensen zo en zo met elkaar verwant zijn, dan is nu die persoon kroonprins (m/v), d.w.z. degene waarop het koningschap zou overgaan als de koning nu zou overlijden. Dat betekent dat alle predikaten uit het domeinmodel nu gelden. Als ze een tijdsparameter hadden, zou deze overal dezelfde zijn. Daarom kun je tijdsparameter beter weglaten.
Doel
literatuur
|
- Je kunt een predikaatlogisch domeinmodel maken voor familierelaties en opvolgingskwesties.
- Je kunt abstraheren van de tijd waar dat mogelijk is.
- Je kunt een wetstekst vertalen naar predikaatlogica.
- Je kunt een complexe specificatie stap voor stap opbouwen met hulpdefinities.
Instructie
- Bekijk het hierboven geciteerde artikel 25 van de Nederlandse grondwet. De grondwet kent geen koningin, alleen een koning (m/v).
- Denk na over het juiste perspectief. Waarvan kun je abstraheren?
- Bekijk de oefenpagina predicaatlogica. Wat ervan kun je gebruiken?
- Maak een domeinmodel, d.w.z. definieer een lijstje van predikaten die voldoende zijn om alles te zeggen wat conform artikel 25 gezegd moet worden. Voorbeelden zijn 'x is koning', 'x is wettig kind van y'.
- Streef ernaar dat je domeinmodel minimaal is, d.w.z. dat het geen predikaten bevat die men kan uitdrukken door samenstelling van andere predikaten uit je model. Als je 'is kind van' en 'is vrouwelijk' al hebt, is 'is moeder van' niet meer nodig want dit is te formuleren als samenstelling.
- Denk na over hulpdefinities die het verhaal eenvoudiger kunnen maken. Je kunt je laten inspireren door de definities van de oefenpagina.
- Bestudeer nu nog eens artikel 25. Het is een goed idee om te beginnen met iets eenvoudigs en dat stapsgewijs uit te breiden, bijvoorbeeld:
- Neem even aan dat de koning altijd twee kinderen en geen kleinkinderen heeft. Schrijf op wie in zo'n geval kroonprins is.
- Houd er nu rekening mee dat mensen dood kunnen zijn. Breid je specificatie uit.
- Breid je specificatie uit op de situatie waarin de koning kleinkinderen heeft, enz.
- Geef ten slotte een definitie van het predikaat "is kroonprins" die overeenkomt met artikel 25. kroonprins(x) moet waar zijn voor de persoon x waarop het koningschap zou overgaan als de huidige koning nu zou overlijden. Probeer daartoe niet al die merkwaardige zinnen uit de wet na te bootsen maar een predikaat te definiëren dat dezelfde betekenis heeft. Misschien kan het eleganter dan in de grondwet staat.
Definition isKroonprins (p:M) := ...
Product
- Een tabel met je domeinmodel.
- Een lijst van definities van samengestelde predikaten. Geef de definitie van kroonprins en hulpdefinities die ertoe bijdragen dat het geheel beter leesbaar en begrijpelijk wordt. Het e.e.a. in door Coq goedgekeurde syntax.
- Een korte verantwoording: geeft dit de betekenis van het wetsartikel precies weer? Welke twijfels heb je nog?
Reflectie
- Kloppen de bereiken van je kwantoren? Staan er voldoende haakjes?
- Sta je zelf 100% achter wat je hebt opgeschreven? Welke twijfels heb je?
- Ben je zeker dat, onafhankelijk van de huidige familiesituatie van de Oranjes, je predikaat kroonprins(x) waar is dan en alleen dan als voor x de door de grondwet aangewezen vermoedelijke opvolger ingevuld is?
Inleveren
- Je uitwerking maak je hier.
- Zet op de eerste regel van je uitwerking precies dit:
{{individuele opdracht}} - Uiterste inleverdatum: {{{deadline}}} en geen minuut later -
- Wil je deelnemen aan het responsiecollege moet je uitwerking op tijd af zijn en (indien MediaWiki correct functioneert) in het goede lijstje hieronder verschijnen.
