Hostname: page-component-745bb68f8f-hvd4g Total loading time: 0 Render date: 2025-02-11T10:27:19.575Z Has data issue: false hasContentIssue false

MARKOV’S PRINCIPLE AND SUBSYSTEMS OF INTUITIONISTIC ANALYSIS

Published online by Cambridge University Press:  26 February 2019

JOAN RAND MOSCHOVAKIS*
Affiliation:
PROF. EMERITA OF MATHEMATICS, OCCIDENTAL COLLEGE 721 24TH STREET SANTA MONICA, CA90402, USA E-mail: joan.rand@gmail.comURL: https://www.math.ucla.edu/∼joan/
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Using a technique developed by Coquand and Hofmann [3] we verify that adding the analytical form MP1: $\forall \alpha (\neg \neg \exists {\rm{x}}\alpha ({\rm{x}}) = 0 \to \exists {\rm{x}}\alpha ({\rm{x}}) = 0)$ of Markov’s Principle does not increase the class of ${\rm{\Pi }}_2^0$ formulas provable in Kleene and Vesley’s formal system for intuitionistic analysis, or in subsystems obtained by omitting or restricting various axiom schemas in specified ways.

Type
Articles
Copyright
Copyright © The Association for Symbolic Logic 2019 

References

REFERENCES

Avigad, J., Interpreting classical theories in constructive ones, this Journal, vol. 65 (2000), pp. 17851812.Google Scholar
Bridges, D. and Richman, F., Varieties of Constructive Mathematics, London Mathematical Society Lecture Note Series, vol. 97, Cambridge University Press, Cambridge, 1987.Google Scholar
Coquand, T. and Hofmann, M., A new method for establishing conservativity of classical systems over their intuitionistic version. Mathematical Structures in Computer Science, vol. 9 (1999), pp. 323333.Google Scholar
Kleene, S. C., Introduction to Metamathematics, van Nostrand, Princeton, NJ, 1952.Google Scholar
Kleene, S. C., Formalized Recursive Functionals and Formalized Realizability, Memoirs, vol. 89, American Mathematical Society, Providence, RI, 1969.Google Scholar
Kleene, S. C. and Vesley, R. E., The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, North Holland, Amsterdam, 1965.Google Scholar
Vafeiadou, G., Formalizing constructive analysis: A comparison of minimal systems and a study of uniqueness principles, Ph.D. thesis, National and Kapodistrian University of Athens, 2012.Google Scholar
Vafeiadou, G., A comparison of minimal systems for constructive analysis, arXiv:1808.000383.Google Scholar