×

zbMATH — the first resource for mathematics

On theorems of Gödel and Kreisel: Completeness and Markov’s principle. (English) Zbl 0801.03038
Summary: In 1957, Gödel proved that completeness for intuitionistic predicate logic HPL implies forms of Markov’s Principle, MP. The result first appeared, with G. Kreisel’s refinements and elaborations, in J. Symb. Log. 27, 139-158 (1963; Zbl 0117.010). Featuring large in the Gödel-Kreisel proofs are applications of the axiom of dependent choice, DC. Also in play is a form of Herbrand’s theorem, one allowing a reduction of HPL derivations for negated prenex formulae to derivations of negations of conjunctions of suitable instances. First, we here show how to deduce Gödel’s results by alternative means, ones arguably more elementary than those of Kreisel [loc. cit.]. We avoid DC and Herbarnd’s theorem by marshalling simple facts about negative translations and Markov’s rule. Second, the theorems of Gödel and Kreisel are commonly interpreted as demonstrating the unprovability of completeness of HPL, if means of proof are confined within strictly intuitionistic metamathematics. In the closing section, we assay some doubts about such interpretations.

MSC:
03F50 Metamathematics of constructive systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Boolos, G. and R. Jeffrey, Computability and logic , Second Edition, Cambridge University Press, New York. · Zbl 0298.02003
[2] Cutland, N., Computability , Cambridge University Press, New York, 1980. · Zbl 0448.03029
[3] Dummett, M., Elements of Intuitionism , Clarendon Press, Oxford, 1977. · Zbl 0358.02032
[4] Friedman, H., “Classically and intuitionistically provably recursive functions,” pp. 21–27 in Higher Set Theory , edited by G. Müller and D.S. Scott, Springer-Verlag, New York, 1978. · Zbl 0396.03045
[5] Gödel, K., “On the completeness of the calculus of logic,” pp. 61–101 in Collected Works , Volume I, Publications 1929–1936, edited by S. Feferman et al ., Oxford University Press, New York, 1986.
[6] Gödel, K., “On the completeness of the calculus of logic,” p. 125 in Collected Works , Volume I, Publications 1929–1936, edited by S. Feferman et al ., Oxford University Press, New York, 1986.
[7] Gödel, K., “On intuitionistic arithmetic and number theory,” pp. 286–295 in Collected Works , Volume I, Publications 1929–1936, edited by S. Feferman et al ., Oxford University Press, New York, 1986.
[8] Heyting, A., “Die formalen Regeln der intuitionistischen Logik,” Sitzungsberichte der Preussischen Akademie der Wissenschaften , physikalisch-mathematische Klasse, (1930), pp. 42–56. · JFM 56.0823.01
[9] Heyting, A., “Die formalen Regeln der intuitionistischen Mathematik II,” Sitzungsberichte der Preussischen Akademie der Wissenschaften , physikalisch-mathematische Klasse, (1930), pp. 57–71. · JFM 56.0823.01
[10] Heyting, A., “Die formalen Regeln der intuitionistischen Mathematik III,” Sitzungsberichte der Preussischen Akademie der Wissenschaften , physikalisch-mathematische Klasse, (1930), pp. 158–169. · JFM 56.0823.01
[11] Kolmogorov, A.N., “On the principle of the excluded middle,” pp. 414–437 in From Frege to G ödel: A Source Book in Mathematical Logic, 1879–1931, edited by J. van Heijenoort, Harvard University Press, Cambridge, 1977.
[12] Kreisel, G., “Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae,” The Journal of Symbolic Logic , vol. 23 (1958), pp. 317–330. JSTOR: · Zbl 0086.24601
[13] Kreisel, G., “The nonderivability of \(\neg (x)A(x)\rightarrow (\exists x)\neg A(x)\), \(A\) primitive recursive, in intuitionistic formal systems (abstract),” The Journal of Symbolic Logic , vol. 23 (1958), pp. 456–457. JSTOR:
[14] Kreisel, G., “On weak completeness of intuitionistic predicate logic,” The Journal of Symbolic Logic , vol. 27 (1962), pp. 139–158. JSTOR: · Zbl 0117.01005
[15] Kreisel, G., “Hilbert’s Programme,” pp. 157–183 in Philosophy of Mathematics , Selected Readings, edited by P. Benacerraf and H. Putnam, Prentice-Hall, Englewood Cliffs, 1964. · Zbl 0090.01004
[16] Kreisel, G., “Mathematical logic,” pp. 95–195 in Lectures in Modern Mathematics III , edited by T.L. Saaty, Wiley and Sons, New York, 1965. · Zbl 0147.24703
[17] M c Carty, D.C., “Markov’s Principle, isols and Dedekind-finite sets,” The Journal of Symbolic Logic , vol. 53 (1988), pp. 1042–1069. JSTOR: · Zbl 0671.03037
[18] Smorynski, C., “Applications of Kripke models,” pp. 324–391 in Metamathematical Investigation of Intuitionistic Arithmetic and Analysis , edited by A.S. Troelstra, Springer-Verlag, New York, 1973.
[19] Troelstra, A.S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis , Springer-Verlag, New York, 1973. · Zbl 0275.02025
[20] Troelstra, A.S. and D. van Dalen, Constructivism in Mathematics , An Introduction, Volume II, North-Holland, New York, 1988. · Zbl 0661.03047
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.