The implicational fragment of Dummett's LC
Robert A. Bull · Journal of Symbolic Logic · 1962
It has been shown in Dummett [1] that the system LC given by Heyting's Calculus plus the additional axiom ACpqCqp is complete with respect to the model having as truth values the integers 0, 1,2, … and ω, 0 being the designated value, with In this system CCCpqrCCCqprr is equivalent to ACpqCqp, and the purpose of this paper is to show that the implicational fragment of Heyting's Calculus plus the additional axiom CCCpqrCCCqprr yields the implicational fragment of LC.