Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#10 Classical Logic vs Intuitionistic Logic

Thorsten Altenkirch and Anupam Das

Apr 11th 2024   |  77 min
0:00
0:00

In this episode we host a discussion between Anupam Das and Thorsten Altenkirch on the role of constructivism in mathematics, logic and computer science.

Anupam is a lecturer in the University of Birmingham in the UK, and Thorsten Altenkirch is a CS Professor at the University of Nottingham.

We discuss why constructive content in proofs matters, the law of excluded middle, the axiom of choice, category theory, and much more!

Links