Explicit logic is a great tradition similar to that of classical and intuitionistic
logic. Due to its very explicitness, it is the most challenging of the
three, and the one most closely connected with Computer Science. Languages
whose most natural semantics are in explicit logic include functional programming
languages, PROLOG, together with theorem provers such as Nuprl, HOL, Coq,
etc.
From the point of view of logic, every computation is a deduction from
initial premises in a suitable associated formal system. From the point
of view of Computer Science, every deduction is an execution sequence of
a computation with the premises as initial data. The "Greats" (Brouwer,
Kolmogorov, Goedel) raised in the 1930's a complex of fundamental questions
of explicit logic which we can now characterize as determining the exact
relation between deduction and computation. One such fundamental relation,
stemming from the consistency proofs of Gentzen, has already become a cornerstone
of Computer Science. This is the Curry-Howard Isomorphism between typed
lambda-terms and intuitionistic deductions.
The Curry-Howard Isomorphism does not of itself capture the self-referential
mechanisms available in deductions in sufficiently rich formal systems and in
programming languages. Our discovery of a natural system of self-referential
proof terms, which we call "proof polynomials", was essential in our solution
to the famous open problem of Goedel (1933) concerning formalization of provability
(cf.
major scientific accomplishments). Proof polynomials
considerably extend the Curry-Howard Isomorphism and lead to a joint calculus
of propositions and proofs which unifies several previously unrelated areas.
We will explain our solution, and why it changes our conception of the appropriate
syntax and semantics for typed programming languages, automated deduction and
formal verification, reasoning about knowledge, nonmonotonic reasoning.