Intuitionistic frege systems are polynomially equivalent

G. Mints   ; A. A. Kojevnikov

Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part IX, Tome 316 (2004), pp. 129-146

Résumé

As shown in [3], any two classical Frege systems polynomially simulate each other. The same proof does not work for the intuitionistic Frege systems, since they can have non-derivable admissible rules. (The rule $A/B$ is derivable if formula $A\to B$ is derivable. The rule $A/B$ is admissible if for all substitutions $\sigma$ if $\sigma(A)$ is derivable then $\sigma(B)$ is derivable). In this paper we polynomially simulate a single admissible rule and show that any two intuitionistic Frege systems polynomially simulate each other.

Bibliographie

[1] S. Buss, G. Mints, “The complexity of the disjunction and existential properties in intuitionistic logic”, Annals of Pure and Applied Logic, 99:1–3 (1999), 93–104 | DOI | MR | Zbl

[2] S. Buss, P. Pudlak, “On the computational content of intuitionistic propositional proofs”, Annals of Pure and Applied Logic, 109:1–2 (2001), 49–64 | DOI | MR | Zbl

[3] S. A. Cook, A. Reckhow, “The relative efficiency of propositional proof systems”, The Journal of Symbolic Logic, 44:1 (1979), 36–50 | DOI | MR | Zbl

[4] M. Ferrari, C. Fiorentini, G. Fiorino, “On the complexity of disjunction and explicit definability properties in some intermediate logics”, Proceedings of LPAR'02, Lect. Notes in Computer Science, 2514, 2002, 175–189 | MR | Zbl

[5] H. Friedman, “One Hundred and Two Problems in Mathematics Logic”, The Journal of Symbolic Logic, 40:2 (1975), 113–129 | DOI | MR | Zbl

[6] S. Ghilardi, “Unification in intuitionistic logic”, The Journal of Symbolic Logic, 64:2 (1999), 859–880 | DOI | MR | Zbl

[7] Ja. Ja. Golota, “Nets of Marks and Deducibility in the Intuitionistic Propositional Calculus”, Zap. Nauchn. Semin. LOMI, 40, 1974, 4–9 | MR | Zbl

[8] R. Harrop, “Concerning formulas of the types $A\to B\lor C$, $A\to(Ex)B(x)$ in intuitionistic formal systems”, The Journal of Symbolic Logic, 25:1 (1960), 27–32 | DOI | MR | Zbl

[9] R. Iemhoff, “On the admissible rules of intuitionistic propositional logic”, The Journal of Symbolic Logic, 66:1 (2001), 281–243 | DOI | MR

[10] G. Kreisel, “Constructivist approaches to logic”, Modern Logic – A Survey: Historical, Philosophical, and Mathematical Aspects of Modern Logic and Its Applications, 149, ed. E. Agazzi, 1981, 67–91 | MR

[11] G. Kreisel, H. Putnam, “Eine Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül”, Archiv für mathematische Logic und Grundlagenforschung, 3:3–4 (1957), 74–78 | DOI | MR | Zbl

[12] A. V. Kuznetsov, “Analogs of the 'Sheffer stroke' in constructive logic”, Dokl. Akad. Nauk SSSR, 160 (1965), 274–277 | MR | Zbl

[13] G. Mints, “Derivability of admissible rules”, Zap. Nauchn. Semin. LOMI, 32, 1972, 85–89 | MR

[14] G. Mints, A Short Introduction to Intuitionistic Logic, Kluwer Academic/Plenum Publishers, 2000 | MR | Zbl

[15] V. P. Orevkov, Complexity of Proofs and their Transformations in Axiomatic Theories, Translations of Mathematical Monographs, 128, American Mathematical Society, 1993 | MR | Zbl

[16] P. Pudlák, “On the complexity of the propositional calculus”, Sets and Proofs: Invited papers from Logic Colloquium' 97, Cambridge University Press, 1999, 197–218 | MR | Zbl

[17] R. A. Reckhow, On the lengths of proofs in the propositional calculus, PhD thesis, Department of Computer Science, University of Toronto, 1976

[18] V. V. Rybakov, Admissibility of Logical Inference Rules, Elsevier, Amsterdam, 1997 | MR | Zbl

[19] P. Schroeder-Heister, “A natural extension of natural deduction”, The Journal of Symbolic Logic, 49:4 (1984), 1284–1300 | DOI | MR | Zbl

[20] J. I. Zucker, R. S. Tragesser, “The adequacy problem for inferential logic”, Journal of Philosophical Logic, 7 (1978), 501–516 | MR | Zbl