University of Birmingham > Talks@bham > Lab Lunch > A Brouwerian Intuitionistic Type Theory (Part 2)

A Brouwerian Intuitionistic Type Theory (Part 2)

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

If you have a question about this talk, please contact Todd Waugh Ambridge.

First talk of the term. Please contact Todd if you wish to give a talk this term!

This is the second part of a talk given on 25/07/19.

In this talk I will present recent additions we made to CTT —-the logic implemented by the Nuprl proof assistant—-in order to turn it into a Brouwerian Intuitionistic Type Theory.

Namely, we added Brouwer’s continuity principle for numbers as well as his bar induction principle—-from which we get W types. Using our implementation or CTT in Coq, we made sure that these principles are consistent with Nuprl by proving that they are valid w.r.t. Nuprl’s semantics. In order to validate these principles we added named exceptions as well choice sequences to Nuprl’s computation system. We initially only added choice sequences to CTT ’s metatheory as an instrumental tool to derive Bar Induction, and not to the theory itself. However, Brouwer originally introduced choice sequences as first class citizens in his logic. Therefore, in our pursuit of a Brouwerian Intuitionistic Type Theory, we have recently added choice sequences to Nuprl’s theory, and have proved that the resulting theory satisfies several of the standard choice sequence axioms.

I will conclude with a discussion of positive and negative results we derived from these constructs/principles: among other things regarding the law of excluded middle, the axiom of choice, Markov’s principle, and Kripke’s schema.

This is joint work with Liron Cohen (Ben-Gurion University, Israel), and Mark Bickford & Bob Constable (Cornell University, USA ).

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.