Tel-Aviv University - Computer Science Colloquium

Sunday,  December 26, 14:15-15:15
at 14:00

Room 309
Schreiber Building

How to circumvent the Goedel incompleteness theorem in applications.

Sergei Artemov

Moscow State University and  Cornell University

The fundamental Goedel incompleteness theorem says that no correct and
sufficiently rich formal system can establish its own consistency. This
theorem has had a profound restricting effect in the foundations of
mathematics. Some theoretical areas of Computer Science such as
constructive semantics, knowledge representation, formal verification,
etc. , suffered similar limitations. In particular, even the most basic
constructive and epistemic logical systems had not have an exact intended semantics.
A formal verification system generally speaking cannot be extended by new
verified facts and rules without making extra unverifiable assumptions
about the system. Isomorphism of formal proofs and programs of special sort did
not reflect an ability of a system to reason about its own proofs. Recent
solution of the Goedel's problem of 1933 and the explicit provability
technique developed for this solution removed the Goedel curse from the
areas above.
 

For colloquium schedule, see http://www.math.tau.ac.il/~zwick/colloq.html