Abstract of Monday's talk
cas at cs.brandeis.edu
Thu Mar 4 18:37:12 EST 1999
A Type Theory for Classical Arithmetic
Monday, March 8, Volen 101, 3-5 p.m.
In this talk I shall present a calculus that arises as a natural
extension of the arithmetic fragment of Martin-L\"of's intensional
type theory with constructors for classical logic.
The work builds upon earlier attempts to model classical proofs of
mathematical theorems in type theories based upon the $\lambda\mu$
calculus by Parigot and on the $\lambda_\Delta$ calculus by Rehof and
Whilst these approaches successfully provide accounts of classical
predicate calculus, they do not appear to be extensible to
satisfactory accounts of induction in classical arithmetic. I shall
show how, by appealing to the blurring between the concepts of proof
and construction induced by the Curry-Howard correspondence, the
difficulties arising with classical induction are due to structural
features of classical induction proofs related to those examples in
functional languages with control whose value depends upon the choice
of reduction strategy. Once uncovered, the difficulties can be
remedied by appeal to an idea from functional programming folklore
about recursing over data structures.
I shall assume some familiarity with proof normalisation in natural
deduction and type dependency. I shall introduce Parigot's
$\lambda\mu$ calculus, and explain how Martin-L\"of's intensional
equality allows us to properly model contructive proofs in type
theory, and how semantic ideas of Dag Prawitz and Michael Dummett
allow us to justify the claim that our type theory constructively
models classical proofs.
This work is from my DPhil thesis 'On the formulae-as-types
correspondence for classical logic' which was supervised by Luke Ong
More information about the Church-announce