Logical Aspects of Virtual Double Categories

TL;DR

This thesis explores virtual double categories as a unified framework for semantics and syntax in predicate logic, proposing a double-categorical approach and developing a corresponding type theory.

Contribution

It introduces a double-categorical method for categorical logic and presents FVDblTT, a type theory serving as an internal language for virtual double categories.

Findings

Virtual double categories effectively model predicate logic semantics.

The framework subsumes existing categorical logic models.

FVDblTT provides a syntactic language for virtual double categories.

Abstract

This thesis deals with two main topics: virtual double categories as semantics environments for predicate logic, and a syntactic presentation of virtual double categories as a type theory. One significant principle of categorical logic is bringing together the semantics and the syntax of logical systems in a common categorical framework. This thesis is intended to propose a double-categorical method for categorical logic in line with this principle. On the semantic side, we investigate virtual double categories as a model of predicate logic and illustrate that this framework subsumes the existing frameworks properly. On the syntactic side, we develop a type theory called FVDblTT that is designed as an internal language for virtual double categories.