A workshop to be held on 3 July 2019 at the University of Kent, Cornwallis East Seminar Room 1. Registration not necessary. For details, email d.corfield@kent.ac.uk.
10.00-10.20 Coffee
10.20-10.30 Welcome
10.30-11.30 Stuart Presnell (Bristol), 12 Reasons to be Interested in Topos Theory, (abstract)
11.30-12.30 Zhaohui Luo (Royal Holloway), Proof Irrelevance in Type-Theoretical Semantics, (abstract)
12.30-13.45 Lunch
13.45-14.45 Dominic Orchard (Kent), Graded Modal Logics: Past, present, and a possible future, (abstract), (slides)
14.45-15.45 Gavin Thomson (Kent), Logical Expressivism and Type Theory, (abstract)
15.45-16.00 Coffee
16.00-17.00 David Corfield (Kent), Temporal Types and Events, (abstract), (slides)
Mathematicians have plenty of reasons to be interested in topos theory, since toposes have proved to be an exciting and fruitful domain of study at the intersection of geometry (in particular: homotopy theory) and logic (in particular: constructive logic). But topos theory has received considerably less attention outside the mathematics department — not least because many introductory texts on the subject demand a lot of background knowledge in category theory and/or algebraic geometry.
In this talk I’ll give a basic introduction to topos theory without assuming a lot of background knowledge. I’ll then outline 12 ways in which topos theory may be of interest to a wider audience, including philosophers, physicists, and computer scientists.
Type theories have been used as foundational languages for formal semantics of natural language. Under the propositions-as-types principle, most modern type systems have explicit proof objects which, however, cause problems in obtaining correct identity criteria in semantics. Therefore, it has been proposed that some principle of proof irrelevance should be enforced in order for a type theory to be an adequate semantic language. This talk studies how proof irrelevance can be enforced, particularly in predicative type systems.
In an impredicative type theory such as UTT, proof irrelevance can be imposed directly since the type Prop in such a type theory represents the totality of logical propositions and helps to distinguish propositions from other types. In a predicative type theory, however, such a simple approach would not work; for example, in Martin-Löf’s type theory (MLTT), propositions and types are identified and, hence, proof irrelevance would have implied the collapse of all types. We propose that Martin-Löf’s type theory should be extended with h-logic, as proposed by Veovodsky and studied in the HoTT project, where proof irrelevance is built-in in the notion of logical proposition. This amounts to , a predicative type system that can be adequately employed for formal semantics.
In the 1970s, the notion of “grading” appeared in modal logic as a way of making reasoning more fine-grained, capturing degrees of necessity or possibility. Somewhat independently, “grading” has become a topic of increasing interest in type theory and programming language semantics, with graded structures again providing a means of more fine-grained reasoning. In this talk, I propose some general definitions for the notion of ‘graded modality’ which encompass both past work in logic and recent work in types and semantics. I will demonstrate some recent work in using graded modalities for program reasoning, via their application in a practical language, and discuss some ideas for taking this forwards.
Philosopher Robert Brandom has entered the literature on proof-theoretic semantics. Brandom coined the term “inferentialism” for any claim that linguistic meaning (“conceptual content”) should be explained in terms of inference; to be meaningful is to be governed by a set of inferential rules. He endorses Gentzen’s remarks that the meanings of the logical connectives are determined by their introduction rules (“logical inferentialism”), and proposes that this idea can be extended to natural language via normative rules of application.
But Brandom also offers us a pragmatist or meaning-as-use account of logical vocabulary – what it does and how it might be demarcated. This is his position of logical expressivism. In this talk I consider how the propositions-as-types paradigm might be accommodated by logical expressivism. In particular I discuss: the proposition-judgment distinction; type-theoretic treatments of identity; and how the expressivist may diverge from traditional philosophical accounts of constructive or intuitionistic mathematics.
It seems reasonable to follow Donald Davidson in drawing an ontological distinction between objects and events. But what should we say of the structures implicit in our descriptions of events? In this talk I discuss how linguists have taken up and improved Zeno Vendler’s classification of kinds of event, and what this might have to do with a temporal type theory.
Last revised on July 8, 2019 at 14:46:26. See the history of this page for a list of all contributions to it.