Skip to main content
SpringerLink
Log in

Negative Translations Not Intuitionistically Equivalent to the Usual Ones

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

We refute the conjecture that all negative translations are intuitionistically equivalent by giving two counterexamples. Then we characterise the negative translations intuitionistically equivalent to the usual ones.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Avigad, J., A variant of the Double-Negation Translation, Carnegie Mellon University Research Showcase, number CMU-PHIL-179, 2006.

  2. Berger U., Buchholz W., Schwichtenberg H.: Refined program extraction from classical proofs. Annals of Pure and Applied Logic 114(1–3), 3–25 (2002)

    Article  Google Scholar 

  3. Coquand, T., Computational content of classical logic, in A. M. Pitts and P. Dybjer (eds.), Semantics and Logics of Computation, Cambridge University Press, Cambridge, United Kingdom, 1997, pp. 33–78.

  4. Dragalin A.G.: New forms of realizability and Markov’s rule. Soviet Mathematics Doklady 21(2), 461–464 (1980)

    Google Scholar 

  5. Dragalin, A. G., New forms of realizability and Markov’s rule (Russian), Doklady Akademii Nauk SSSR 251:534–537, 1980. English translation: New forms of realizability and Markov’s rule [4].

  6. Ferreira, G., and P. Oliva, On various negative translations, in S. van Bakel, S. Berardi and U. Berger (eds.), Electronic Proceedings in Theoretical Computer Science, number 47, 2001, pp. 21–33. Proceedings of the Third International Workshop on Classical Logic and Computation, Brno, Czech Republic, 21–22 August 2010.

  7. Flagg R.C., Friedman H.: Epistemic and intuitionistic formal systems. Annals of Pure and Applied Logic 32, 53–60 (1986)

    Article  Google Scholar 

  8. Friedman, H., Classically and intuitionistically provably recursive functions, in G. H. Müller and D. S. Scott (eds.), Higher Set Theory, Lecture Notes in Mathematics, number 669, Springer-Verlag, Berlin, Germany, and Heidelberg, Germany, 1978, pp. 21–27. Proceedings of Higher Set Theory, Oberwolfach, Germany, 13–23 April 1977.

  9. Gentzen, G., Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik, 1933. Galley proof from Mathematische Annalen. Appeared in Archiv für mathematische Logik und Grundlagenforschung [11]. English translation: On the relation between intuitionistic and classical arithmetic [10, pp. 53–67].

  10. Gentzen, G., The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Company, Amsterdam, Netherlands, and London, United Kingdom, 1969.

  11. Gentzen G.: Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik. Archiv für mathematische Logik und Grundlagenforschung 16, 119–132 (1974)

    Article  Google Scholar 

  12. Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines mathematischen Kolloquiums 4:34–38, 1933. English translation: On intuitionistic arithmetic and number theory [13, pp. 286–295].

  13. Gödel, K., Collected Works, volume 1, Oxford University Press, New York, United States of America, 1986.

  14. Ishihara H.: A note on the Gödel-Gentzen translation. Mathematical Logic Quarterly 46(1), 135–137 (2000)

    Article  Google Scholar 

  15. Kolmogorov, A. N., On the principle of tertium non datur (Russian), Matematicheskii Sbornik 32(4):646–667, 1925. English translation: On the principle of excluded middle [22, pp. 414–437].

    Google Scholar 

  16. Krivine J.-L.: Opérateurs de mise en mémoire et traduction de Gödel. Archive for Mathematical Logic 30(4), 241–267 (1990)

    Article  Google Scholar 

  17. Kuroda S.: Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal 2, 35–47 (1951)

    Google Scholar 

  18. Streicher T., Kohlenbach U.: Shoenfield is Gödel after Krivine. Mathematical Logic Quarterly 53(2), 176–179 (2007)

    Article  Google Scholar 

  19. Streicher T., Reus B.: Classical logic, continuation semantics and abstract machines. Journal of Functional Programming 8(6), 543–572 (1998)

    Article  Google Scholar 

  20. Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, number 344, Springer-Verlag, Berlin, Germany, and Heidelberg, Germany, 1973.

  21. van Dalen, D., Logic and Structure, Springer-Verlag, 1980. Fourth edition, 2004.

  22. van Heijenoort, J., (ed.), From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Harvard University Press, Cambridge, Massachusetts, United States of America, 1967.

Download references

Author information

Authors and Affiliations

  1. Arbeitsgruppe Logik, Fachbereich Mathematik, Technische Universität Darmstadt, Schlossgartenstrasse 7, 64289, Darmstadt, Germany

    Jaime Gaspar

Authors
  1. Jaime Gaspar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jaime Gaspar.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Gaspar, J. Negative Translations Not Intuitionistically Equivalent to the Usual Ones. Stud Logica 101, 45–63 (2013). https://doi.org/10.1007/s11225-011-9367-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11225-011-9367-6

Keywords

Mathematics Subject Classification (2010)

Search

Navigation