Analysis and construction of logical systems: a category-theoretic approach

Celem niniejszej rozprawy jest zbudowanie teoriokategoryjnych fundamentów umożliwiających studiowanie rachunków lambda i ich logik opisanych za pomocą systemów logicznych. Pokazujemy w jaki sposób 2-kategorie z notacją dyskretności pozawalają mówić o modelach dla polimorficznych rachunków lambda. Uogólniamy i internalizujemy w 2-kategoriach klasyczne twierdzenia Petera Freyda o nieistnieniu dostatecznie (ko)zupełnych niezdegenerowanych kategorii. Jako prosty wniosek otrzymujemy wariant twierdzenia Freyda dla kategorii wewnętrznych względem dowolnej kategorii z tensorami. Wprowadzamy pojęcie kategorii stowarzyszonej i bazując na nim dowodzimy twierdzenie o reprezentacji wiążące wprowadzone w rozprawie wewnętrzne modele z dobrze znanymi modelami rozwłóknieniowymi dla polimorfizmu. Definiujemy pojęcie trójkąta Yonedy jako relatywizację wewnętrznych sprzężeń i używamy go do charakteryzacji uniwersów posiadających notację splotu. Pokazujemy, że takie uniwersa indukują semantykę dla rachunków lambda. Dowodzimy, że konstrukcja analogiczna do splotu Day'a dla kategorii wzbogacanych strukturą monoidalną zachodzi także dla kategorii wewnętrznych względem dowolnej lokalnie kartezjańsko domkniętej kategorii ze skończonymi kogranicami.

The aim of this dissertation is to develop categorical foundations for studying lambda calculi and their logics formed into logical systems. We show how internal models for polymorphic lambda calculi arise in any 2-category with a notion of discreteness. We generalise to a 2-categorical setting the famous theorem of Peter Freyd saying that there are no sufficiently (co)complete non-degenerate categories. As a simple corollary, we obtain a variant of Freyd theorem for categories internal to any tensored category. We introduce the concept of an associated category, and relying on it, provide a representation theorem relating our internal models with well-studied fibrational models for polymorphism. Finally, we define Yoneda triangles as relativisations of internal adjunctions, and use them to characterise universes that admit a notion of convolution. We show that such universes induce semantics for lambda calculi. We prove that a construction analogical to enriched Day convolution works for categories internal to a locally cartesian closed category with finite colimits.