| Summary: | Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for
every two statements the first implies the second or the second implies the
first. We present a natural deduction and a Curry-Howard correspondence for
first-order and second-order Dummett's logic. We add to the lambda calculus an
operator which represents, from the viewpoint of programming, a mechanism for
representing parallel computations and communication between them, and from the
viewpoint of logic, Dummett's axiom. We prove that our typed calculus is
normalizing and show that proof terms for existentially quantified formulas
reduce to a list of individual terms forming an Herbrand disjunction.
|
|---|