This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Buss [1986]. Bounded Arithmetic, Bibliopolis, Naples.
S. A. Cook and A. Urquhart [1994]. Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic (to appear).
S. Feferman [1977]. Theories of finite type related to mathematical practice, in Handbook of Mathematical Logic (J. Barwise, ed.), North-Holland, Amsterdam, 913–971.
S. Feferman [1984]. Kurt Gödel: conviction and caution, Philosophia Naturalis 21, 546–562.
S. Feferman [1987]. Proof theory: a personal report, appendix to second edition of Proof Theory by G. Takeuti, North-Holland, Amsterdam, 447–485.
S. Feferman [1988]. Hilbert's program relativized: proof-theoretical and foundational reductions, J. Symbolic Logic 53, 364–384.
S. Feferman [1990]. Milking the Dialectica interpretation, unpublished notes for a lecture at the Conference on Proof Theory, Arithmetic and Complexity, U. C. San Diego, June 25–27, 1990.
S. Feferman [1993]. What rests on what? The proof-theoretic analysis of mathematics, to appear in Proc. 15th International Wittgenstein Symposium, Kirchberg, Austria.
S. Feferman and G. Jäger [1983]. Choice principles, the bar rule and automomously iterated comprehension schemes in analysis, J. Symbolic Logic 48, 63–70.
S. Feferman and W. Sieg [1981]. Proof-theoretic equivalences between classical and constructive theories for analysis, Lecture Notes in Mathematics 879, 78–142.
F. Ferreira [1988]. Polynomial Time Computable Arithmetic and Conservative Extensions, Ph. D. Thesis, Pennsylvania State University, University Park, PA.
G. Gentzen [1936]. Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematischen Annalen 112, 493–565.
K. Gödel [1933]. Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums 4, 34–38 (reproduced, with English translation, in [Gödel 1986], 286–295).
K. Gödel [1958]. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12, 280–287 (reproduced with English translation, in [Gödel 1990], 240–251.
K. Gödel [1972]. On an extension of finitary mathematics which has not yet been used, in[Gödel 1990], 271–280.
K. Gödel [1986]. Collected Works, Vol. I: Publications 1929–1936 (S. Feferman et al., eds.), Oxford University Press, New York.
K. Gödel [1990]. Collected Works, Vol. II: Publications 1937–1974 (S. Feferman et al., eds.), Oxford University Press, New York.
N. D. Goodman [1970]. The faithfulness of the interpretation of arithmetic in the theory of constructions, J. Symbolic Logic 38, 453–459.
D. Hilbert [1926]. Über das Unendliche, Mathematische Annalen 95, 161–190.
W. Howard [1968]. Functional interpretation of bar induction by bar recursion, Compositio Mathematica 20, 107–124.
W. Howard [1973], Hereditarily majorizable functionals of finite type, Appendix to [Troelstra 1973], 454–461.
S. C. Kleene [1952]. Introduction to Metamathematics, North-Holland, Amsterdam.
S. C. Kleene [1959]. Countable functionals, in Constructivity in Mathematics (A. Heyting, ed.), North-Holland, Amsterdam, 81–100.
G. Kreisel [1951]. On the interpretation of non-finitist proofs — Part I. J. Symbolic Logic 16, 241–267.
G. Kreisel [1952]. On the interpretation of non-finitist proofs — Part II. Interpretation of number theory. Applications. J. Symbolic Logic 17, 43–58.
G. Kreisel [1957]. Gödel's interpretation of Heyting's arithmetic, Summaries of talks, Summer Institute for Symbolic Logic, Cornell University 1957 (2nd edn. 1960), Inst. for Defense Analyses, Princeton.
G. Kreisel [1959]. Interpretation of analysis by means of constructive functionals of finite types, in Constructivity in Mathematics (A. Heyting, ed.), North-Holland, Amsterdam, 101–128.
G. Kreisel [1962]. Foundations of intuitionistic logic, in Logic, Methodology and Philosophy of Science (E. Nagel et al., eds.) Stanford University Press, Stanford.
G. Kreisel (ed.) [1963]. Reports of Seminar on the Foundations of Analysis, Stanford, Summer 1963. Stanford University, Stanford.
G. Kreisel [1987]. Gödel's excursions into intuitionistic logic, in Gödel Remembered (P. Weingartner and L. Schmetterer, eds.), Bibliopolis, Naples, 65–186.
J. R. Shoenfield [1967]. Mathematical Logic, Addison-Wesley, Reading MA.
W. Sieg [1985]. Fragments of arithmetic, Annals of Pure and Applied Logic 28, 33–72.
W. Sieg [1991]. Herbrand analyses, Archive for Mathematical Logic 30, 409–441.
C. Spector [1962]. Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, in Recursive Function Theory (J. C. E. Dekker, ed.), Proc. Symposia in Pure Mathematics 5, American Math. Society, Providence, 1–27.
A. S. Troelstra (ed.) [1973]. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics 344, Springer-Verlag, Berlin.
A. S. Troelstra [1990]. Introductory note to 1958 and 1972, in[Gödel 1990], 217–241.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Feferman, S. (1993). Gödel's Dialectica interpretation and its two-way stretch. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1993. Lecture Notes in Computer Science, vol 713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022549
Download citation
DOI: https://doi.org/10.1007/BFb0022549
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57184-1
Online ISBN: 978-3-540-47943-7
eBook Packages: Springer Book Archive