BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning

Add to your list(s) Download to your calendar using vCal

• Vincent Rahli (University of Birmingham)
• Thursday 16 June 2022, 14:00-15:00
• 245, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

Time-progressing expressions, i.e., expressions that compute to different values over time such as Brouwerian choice sequences or reference cells, are a common feature in many frameworks. For type theories to support such elements, they usually employ sheaf models.

We have recently developed a number of theories featuring such time-progressing expressions, which we have now generalized into a general framework in the form of an extensional type theory incorporating various time-progressing elements along with a general possible-worlds forcing interpretation parameterized by modalities.

The modalities can, in turn, be instantiated with topological spaces of bars, leading to a general sheaf model. This parameterized construction allows capturing a distinction between theories that are ``agnostic’’, i.e., compatible with classical reasoning in the sense that classical axioms can be validated, and those that are ``intuitionistic’’, i.e., incompatible with classical reasoning in the sense that classical axioms can be proven false.

This distinction is made via properties of the modalities selected to model the theory and consequently via the space of bars instantiating the modalities. We further identified a class of time-progressing elements that allows deriving ``intuitionistic’’ theories that include not only choice sequences but also simpler operators, namely reference cells.

In this talk, we will first present the BITT and OpenTT that led to this general framework, before presenting the framework, along with examples of theories it captures.

=== Zoom details ===

https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09

Passcode: 217 Meeting ID: 818 7333 5084

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• 245, SoCS and Zoom (see abstract for link)
• Lab Lunch

Note that ex-directory lists are not shown.