Stability of intuitionistic systems
by Sergei Artemov
1999-2000
Comment
A formal system is stable if it
does not change after extension by internally
verified rules. A stability of a classical system
requires rather strong semantical assumptions about
the system (some form of soundness with respect to
special kind of semantics) which usually cannot be
constructively verified.
In this talk we will give a concise account of
metamathematics of verification for both classical
and intuitionistic systems and correct some mistakes
in the original Davis-Schwartz theory. In particular,
we show that an intuitionistic system with the usual
constructive properties (disjunctive property,
explicit definability, etc.) is stable. Therefore
constructive systems are the systems of choice for
verification purposes.