Categorische logica
Categorische logica is de tak van de wiskunde waarin hulpmiddelen en concepten uit de categorietheorie worden toegepast op de studie van wiskundige logica. Het valt ook op door zijn verbanden met de theoretische informatica. In grote lijnen vertegenwoordigt categorische logica zowel syntaxis als semantiek door een categorie, en een interpretatie door een functor. Het categorische raamwerk biedt een rijke conceptuele achtergrond voor logische en typetheoretische constructies. In deze termen kwam het onderwerp op sinds circa 1970.
Overzicht bewerken
Er zijn drie belangrijke thema’s in de categorische benadering van logica:
- Categorische semantiek
- Categorische logica introduceert het begrip structuur gewaardeerd in een categorie C, waarbij het klassieke modeltheoretische begrip van een structuur verschijnt in het specifieke geval waarin C de categorie van verzamelingen is. Deze notie is nuttig gebleken, wanneer de verzamelingstheoretische notie van een model algemeenheid mist en/of onwennig is. R.A.G. Seely's modellering van verschillende impredicatieve theorieën, zoals System F, is een voorbeeld van het nut van categorische semantiek.
Er werd ontdekt dat de connectieven van pre-categorische logica duidelijker werden begrepen met behulp van het concept van adjunct-functor, en dat de kwantoren ook het best werden begrepen met behulp van adjunct-functors. - Interne talen
- Dit kan worden gezien als een formalisering en veralgemening van bewijs door middel van diagram chasing. Men definieert een geschikte interne taal waarin relevante bestanddelen van een categorie worden benoemd. Vervolgens past men categorische semantiek toe om beweringen in een logica over de interne taal om te zetten in overeenkomstige categorische uitspraken. Dit is het meest succesvol geweest in de topostheorie, waar de interne taal van een topos, samen met de semantiek van de intuïtionistische logica van hogere orde in een topos, men in staat stelt te redeneren over de objecten en morfismen van een topos ‘alsof het verzamelingen en functies zijn’. Dit is succesvol geweest bij het omgaan met topoi die "verzamelingen" hebben met eigenschappen die onverenigbaar zijn met de klassieke logica.
- Term-modelconstructies
- In veel gevallen biedt de categorische semantiek van een logica een basis voor het tot stand brengen van een overeenkomst tussen theorieën in de logica en instanties van een passend soort categorie.