RUS  ENG
Full version
JOURNALS // Zapiski Nauchnykh Seminarov POMI // Archive

Zap. Nauchn. Sem. POMI, 2004 Volume 316, Pages 129–146 (Mi znsl729)

This article is cited in 8 papers

Intuitionistic frege systems are polynomially equivalent

G. Mintsa, A. A. Kojevnikovb

a Department of Philosophy, Stanford University
b St. Petersburg Department of V. A. Steklov Institute of Mathematics, Russian Academy of Sciences

Abstract: 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.

UDC: 510.531+510.642

Received: 05.12.2004

Language: English


 English version:
Journal of Mathematical Sciences (New York), 2006, 134:5, 2392–2402

Bibliographic databases:


© Steklov Math. Inst. of RAS, 2025