De disjunctie-eigenschap in constructieve wiskunde

dc.rights.license	CC-BY-NC-ND
dc.contributor.advisor	Iemhoff, Rosalie
dc.contributor.author	Pit, Q.J.
dc.date.accessioned	2020-08-06T18:00:38Z
dc.date.available	2020-08-06T18:00:38Z
dc.date.issued	2020
dc.identifier.uri	https://studenttheses.uu.nl/handle/20.500.12932/36819
dc.description.abstract	De gevolgtrekkingen in de constructieve wiskunde laten zich goed beschrijven door de intuïtionistische logica I. Deze logica heeft de zogeheten disjunctie-eigenschap: ⊢A∨B impliceert ⊢A of ⊢B. Buss en Pudlák vonden een algoritme dat bewerkstelligt dat deze eigenschap ook voor de constructieve wiskunde geldt. Dat maakt gebruik van het bewijssysteem G1ip voor het propositionele deel van I, Ip. Voor de klasse Harrop-formules geldt zelfs een generalisatie van dit resultaat. Ik voltooi de bewijzen van deze resultaten en vertaal ze naar een ander Ip-bewijssysteem: G3ip.
dc.description.sponsorship	Utrecht University
dc.format.extent	490583
dc.format.mimetype	application/pdf
dc.language.iso	nl
dc.title	De disjunctie-eigenschap in constructieve wiskunde
dc.type.content	Bachelor Thesis
dc.rights.accessrights	Open Access
dc.subject.courseuu	Filosofie