Promotie F. Liang: algebraic proof theory

03 juli 2018 17:30 - Locatie: Aula, TU Delft - Door: webredactie

Multi-type Algebraic Proof Theory. Promotor 1: Dr. A. Palmigiano (TBM); Promotor 2: Prof.dr. M. Ma (Sun Yat-sen U., China); Promotor 3: Prof.dr.ir. I.R. van de Poel (TBM).

Dit proefschrift heeft betrekking op algebraïsche bewijstheorie, een onderzoeksgebied dat gericht is op het oplossen van problemen in structurele bewijstheorie met behulp van resultaten en inzichten uit de algebraïsche logica, universele algebra, dualiteit en representatietheorie voor klassen van algebra’s. De belangrijkste bijdragen van dit proefschrift betreffen, aan de bewijs-theoretische kant, de zeer recente theorie van multi-type calculi en, aan de algebraïsche kant, de gevestigde theorie van heterogene algebra’s.

Gegeven een sequentiële calculus met snede-eliminatiestelling voor een basislogica (b.v. de Lambek-calculus), heeft een kernvraag in de structurele bewijstheorie betrekking op de identificatie van axioma’s die kunnen worden toegevoegd aan de gegeven basis- logica zodat de resulterende axiomatische uitbreidingen kunnen worden vastgelegd door calculi waarvan de snede opnieuw geëlimineerd kan worden. Deze vraag is moeilijk, omdat de snede-eliminatiestelling bekend staat als een zeer fragiel resultaat. De algebraïsche bewijstheorie heeft echter voor substructurele logica een bevredigend antwoord gegeven op deze vraag, door een hiërarchie (Nn,Pn) van axioma’s in de taal van de Lambek-calculus te identificeren (die de substructurele hiërarchie genoemd wordt), die garanderen dat, tot op het niveau N2, deze axioma’s effectief kunnen worden omgezet in speciale (analytische) structurele regels die veilig kunnen worden toegevoegd aan een calculus met snede-eliminatiestelling zonder de snede-eliminatiestelling te vernietigen.

Het onderzoeksprogramma van algebraïsche bewijstheorie kan worden geëxporteerd naar willekeurige talen van normale tralieuitbreidingen, naar de studie van de systematis- che verbindingen tussen algebraïsche logica en displaycalculi, en voorbij aan displaycalculi, naar de studie van de systematische verbindingen tussen de theorie van heterogene algebra’s en multi-type calculi In de voorliggende dissertatie breiden we de semantische cut-eliminatie en de eindige-modeleigenschap uit van de taal van geresidueerde tralies (residuated lattices) naar willekeurige talen van normale tralieuitbreidingen en bouwen of verfijnen de multi-type algebraïsche bewijstheorie van drie logica’s.

Het bepalende kenmerk van de aanpak van de multi-type calculi is dat het entiteiten van verschillende types in staat stelt om gelijkwaardig naast elkaar te bestaan en op elkaar in te werken: elk type heeft zijn eigen interne logica (d.w.z. taal- en afleidingsre- latie) en de interactie tussen logica’s van verschillende typen wordt gefaciliteerd door speciale heterogene connectieven, primitief voor de taal, en gelijkwaardig met alle andere behandeld. Het fundamentele inzicht dat een dergelijke stap rechtvaardigt, is de zeer natuurlijke overweging, voortkomend uit het algebraïsche standpunt over (verenigde) correspondentie, dat de fundamentele eigenschappen die aan deze theorie ten grondslag liggen, zuiver ordetheoretisch zijn. Zolang afbeeldingen of logische verbanden deze fundamentele eigenschappen hebben is er weinig verschil of deze afbeeldingen een en hetzelfde domein en co-domein hebben, danwel verschillende domeinen en co-domeinen overbruggen.

Deze verrijkte omgeving is specifiek ontworpen om het probleem aan te pakken van het uitdrukken van de interacties tussen entiteiten van verschillende typen door middel van analytische structuurregels.

In dit proefschrift bouwen of verfijnen we de multi-type algebraïsche bewijstheorie van drie logica’s, elk waarvan ontstaat in nauwe samenhang met één bekende klasse van algebra’s (semi De Morgan algebra’s, bi-tralies en Kleene algebra’s) en problematisch is voor gebruikelijke bewijstheoretische methoden.

Meer informatie?

Voor inzage in proefschriften van de promovendi kunt u kijken in de TU Delft Repository, de digitale vindplaats van openbare publicaties van de TU Delft. Proefschriften zullen binnen een paar weken na de desbetreffende promotie in de Repository te vinden zijn.