Skip to main content
PRL Project

Stability of intuitionistic systems

by Sergei Artemov


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.