De disjunctie-eigenschap in constructieve wiskunde

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.