Beweren en bewijzen/de zuilen/Taal/5. Definities/Grondwet
| literatuur
... |
Inhoud
Troonopvolging
In taak 8 werd gevraagd om artikel 25 van de Nederlandse Grondwet te formaliseren. Het artikel luidt:
|
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. |
Recursie
Achter de woorden met plaatsvervulling volgens dezelfde regel verbergt zich een recursie: als een kind van de koning eerder is overleden, treden de wettige nakomelingen daarvan in zijn plaats, waarbij het oudste kind voorrang heeft.
Volgens het commentaar op de Grondwet van Bovend'Eert (online beschikbaar: zoek op „grondwet” in de catalogus van de universiteitsbibliotheek) is het bovendien zo dat het aantal generaties van nakomelingen niet beperkt is: achter-achterkleinkinderen etc. kunnen dus ook kroonprins zijn.
Echter, volgens Engelbert kan Coq niet met recursieve definities overweg. Ik stel daarom voor het domeinmodel als volgt te wijzigen: het predicaat N k o moet niet betekenen dat k een wettig kind van o is, maar dat k een wettige nakomeling (kind, kleinkind, achterkleinkind of ...) van o is.
Uitwerking
Hieronder geef ik een poging tot formalisering van deze regel.
Domeinmodel
Ik gebruik het volgende domeinmodel – hetzelfde model als in taak 9:
- K k betekent „k is op dit moment koning.”
- L m betekent „m leeft op dit moment.”
- N k o betekent „k is wettige nakomeling (kind, kleinkind, achterkleinkind, of ...) van o.”
- O o j betekent „o is ouder dan j.”
Preciseringen
- abdicatie
- Als de koning abdiceert leeft hij nog en wordt de kroonprins nieuwe koning. Stel dat de nieuwe koning enig kind is en kinderloos. Wordt dan zijn ouder, dus de voormalige koning, kroonprins? Nee. Een voormalige koning geldt, wat de troonopvolging betreft, als overleden. Hetzelfde geldt voor personen die door huwelijk of om andere redenen van troonopvolging worden uitgesloten. Het predicaat L m moet niet alleen betekenen „m leeft”, maar exacter: „m leeft en heeft geen afstand genomen van de troon, noch is m ongeschikt verklaard.”
- troonopvolging volgens zijlijn
- Het is niet de bedoeling dat de aangetrouwde familie op de troon komt. Stel dat William Koning van Engeland wordt – dan is het niet de bedoeling dat zijn grootvader Philip Mountbatten of diens andere nakomelingen op de troon komen, noch de kinderen van Camilla Parker Bowles uit haar eerdere huwelijk. Het predicaat N k o mag daarom alleen waar zijn als de troonopvolging via die lijn verloopt, dus als k koning is geweest of een nakomeling van de een gewezen koning. (Als gevolg heeft iedereen maximaal één ouder volgens N!)
Hulppredikaten
Ik definiëer de volgende hulppredikaten:
Algemene hulppredicaten
Definition Ki (kind:M) (ouder:M) :=
N kind ouder
/\
~(exists tussen:M, N kind tussen /\ N tussen ouder)
.
Ki kind ouder betekent: kind is wettig kind van ouder, d.i. kind is nakomeling van ouder en er bestaat geen tussenpersoon in een generatie tussen kind en ouder.
Definition Nrefl (nakomeling:M) (voorouder:M) :=
nakomeling = voorouder \/ N nakomeling voorouder
.
Nrefl is de reflexieve afsluiting van N, d.i. nakomeling is een echte nakomeling van voorouder of de twee zijn gelijk.
Kroonprins in rechte lijn
Definition KiL (kind:M) (ouder:M) :=
Ki kind ouder
/\
(exists nakomeling:M, L nakomeling /\ Nrefl nakomeling kind)
.
KiL kind ouder betekent: kind is wettig kind van ouder en leeft of heeft levende nakomelingen.
Definition OKiL (kind:M) (ouder:M) :=
KiL kind ouder
/\
(
forall ander_kind:M,
KiL ander_kind ouder
->
~O ander_kind kind
)
.
OKiL kind ouder betekent: kind is het oudste wettige kind van ouder dat leeft of levende nakomelingen heeft.
Definition KpR (prins:M) (koning:M) :=
(
forall tussen_kind:M,
forall tussen_ouder:M,
Nrefl prins tussen_kind
/\
Ki tussen_kind tussen_ouder
/\
Nrefl tussen_ouder koning
->
(prins = tussen_kind \/ ~L tussen_kind)
/\
OKiL tussen_kind tussen_ouder
)
/\
N prins koning
.
KpR prins koning beschrijft de Kroonprins in rechte lijn, d.i. prins is kroonprins als hij leeft en koning koning is, of exacter: prins is een nakomeling van koning zodat geen enkele tussengeneratie leeft, maar wel in elke generatie de verwantschapsrelatie via OKiL verloopt.
Hier gebruiken we ook dat de N-relatie alleen die ouder aangeeft via welke de troonopvolging verloopt; anders zou bij een neef–nicht-huwelijk tussen nakomelingen van de koning eventueel geen kroonprins aangewezen worden.
Kroonprins in de 1e (ouderlijke) zijlijn
Voor de troonopvolging in de zijlijn kunnen we ongeveer dezelfde predicaten gebruiken; we moeten echter dan rekening houden met het feit dat de koning of zijn ouder geen kroonprins mag zijn. Bovendien hebben we te maken met een generatie-beperking. Vanwege die generatie-beperking gebruik ik hier geen recursieve predicaten als N, maar alleen Ki.
Definition KiL1 (kind:M) (ouder:M) :=
Ki kind ouder
/\
(
L kind
\/
(exists kleinkind:M, Ki kleinkind kind /\ L kleinkind)
)
.
KiL1 kind ouder betekent: kind is wettig kind van ouder en leeft of heeft levende kinderen.
Definition OKiL1_Z (kind:M) (ouder:M) (koning:M) :=
(
forall ander_kind:M,
KiL1 ander_kind ouder /\ ander_kind <> koning
->
~O ander_kind kind
)
/\
KiL1 kind ouder /\ kind <> koning
.
OKiL1_Z kind ouder koning betekent: kind is het oudste wettige kind van ouder dat leeft of levende kinderen heeft en in de zijlijn van de koning staat.
Definition KpZ1 (prins:M) (koning:M) :=
forall koningouder:M,
Ki koning koningouder
/\
(
exists koningbroer:M,
OKiL1_Z koningbroer koningouder koning
/\
(
prins = koningbroer
\/
~L koningbroer /\ OKiL prins koningbroer
)
)
.
KpZ1 prins koning betekent: prins is kroonprins in de 1e zijlijn, als hij leeft, er geen kroonprins in de rechte lijn bestaat en koning koning is.
Kroonprins in 2e (grootouderlijke) zijlijn
We gebruiken bijna dezelfde predicaten als bij de 1e zijlijn, alleen is het aantal generaties nog verder beperkt.
Definition KiL0 (kind:M) (ouder:M) :=
Ki kind ouder /\ L kind
.
KiL0 kind ouder betekent: kind is levend wettig kind van ouder.
Definition OKiL0_Z (kind:M) (ouder:M) (koningouder:M) :=
(
forall ander_kind:M,
KiL0 ander_kind ouder /\ ander_kind <> koningouder
->
~O ander_kind kind
)
/\
KiL0 kind ouder /\ kind <> koningouder
.
OKiL0_Z kind ouder koningouder betekent: kind is het oudste levende wettige kind van ouder dat in de zijlijn van koningouder staat.
Definition KpZ2 (prins:M) (koning:M) :=
forall koningouder:M,
forall koninggrootouder:M,
Ki koning koningouder
/\
Ki koningouder koninggrootouder
/\
OKiL0_Z prins koninggrootouder koningouder
.
KpZ2 prins koning betekent: prins is kroonprins in de 2e zijlijn, als hij leeft, er geen kroonprins in de rechte lijn of de 1e zijlijn bestaat en koning koning is.
Algemene definitie van kroonprins
Definition Kp (prins:M) :=
L prins
/\
(
exists koning:M,
K koning
/\
(
KpR prins koning
\/
~(exists pr:M, KpR pr koning)
/\
(
KpZ1 prins koning
\/
~(exists pr:M, KpZ1 pr koning)
/\
KpZ2 prins koning
)
)
)
.
Kp prins betekent: prins is kroonprins, d.i. een gevalsonderscheiding: prins is een kroonprins in rechte lijn, of als die niet bestaat, in de 1e zijlijn, of als die ook niet bestaat, in de 2e zijlijn.
| Tentative below this line. Je kunt beter nu niet verder lezen, want het gaat nog veranderen. |
Kroonprins in zijlijn (schets van een recursieve definitie)
In het geval dat er geen generatiebeperking is, wordt ook bij troonopvolging in de zijlijn gebruik gemaakt van het recursieve predicaat N.
Definition KiLZ (kind:M) (ouder:M) (koningslijn:M) :=
KiL kind ouder
/\
kind != koningslijn
.
Definition OKiLZ (kind:M) (ouder:M) (koningslijn:M) :=
KiL kind ouder
/\
kind != koningslijn
/\
(
forall ander_kind:M,
KiLZ ander_kind ouder koningslijn
->
~O ander_kind kind
)
.
Definition OuZ (koning:M) (ouder:M) :=
exists koningslijn:M,
Nrefl koning koningslijn
/\
Ki koningslijn ouder
/\
(exists zijlijn:M, KiLZ zijlijn ouder koning)
.
een ouder die een zijlijn heeft
Definition JOuZ (koning:M) (ouder:M) :=
OuZ koning ouder
/\
(forall voorouder:M, OuZ koning voorouder -> Nrefl ouder voorouder)
.
de jongste ouder die een zijlijn heeft
Definition KpZ (prins:M) (koning:M) :=
exists ouder:M,
exists zijlijn:M,
JOuZ koning ouder
/\
(
exists koningslijn:M,
Ki koningslijn ouder
/\
Nrefl koning koningslijn
/\
OKiLZ zijlijn ouder koningslijn
)
/\
(
prins = zijlijn
\/
~L zijlijn /\ KpR prins zijlijn
)
.
de persoon die kroonprins is, indien zij leeft en er geen kroonprins in rechte lijn is. Deze definitie moet ongeveer op de plaats van KpZ1 in de algemene definitie van Kroonprins ingevoegd worden.
