Context, Judgement, Deduction

TL;DR

This paper introduces judgemental theories as a versatile framework for studying deductive systems, applying it to dependent type theory and natural deduction to offer new insights and unify various logical structures.

Contribution

It presents judgemental theories and their calculi as a general approach, providing abstract definitions and deep analyses of type constructors, natural deduction rules, and internal logics of toposes.

Findings

Judgemental theories unify various deductive systems.

New abstract definitions for type constructors.

Deeper understanding of structural rules in natural deduction.

Abstract

We introduce judgemental theories and their calculi as a general framework to present and study deductive systems. As an exemplification of their expressivity, we approach dependent type theory and natural deduction as special kinds of judgemental theories. Our analysis sheds light on both the topics, providing a new point of view. In the case of type theory, we provide an abstract definition of type constructor featuring the usual formation, introduction, elimination and computation rules. For natural deduction we offer a deep analysis of structural rules, demystifying some of their properties, and putting them into context. We finish the paper discussing the internal logic of a topos, a predicative topos, an elementary 2-topos et similia, and show how these can be organized in judgemental theories.