On the Power of Substitution in the Calculus of Structures
Novak Novaković, Lutz Straßburger · ACM Transactions on Computational Logic · 2015
There are two contributions in this article. First, we give a direct proof of the known fact that Frege systems with substitution can be p-simulated by the calculus of structures (CoS) extended with the substitution rule. This is done without referring to the p-equivalence of extended Frege systems and Frege systems with substitution. Second, we then show that the cut-free CoS with substitution is p-equivalent to the cut-free CoS with extension.