Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-22T05:35:34.387Z Has data issue: false hasContentIssue false
  • English
  • Français

Constructive validity is nonarithmetic

Published online by Cambridge University Press:  12 March 2014

Charles McCarty
Charles McCarty*
Affiliation:
Center for Cognitive Science, Department of Computer Science, University of Edinburgh, Edinburgh, Scotland Department of Philosophy, Florida State University, Tallahassee, Florida 32306
Get access Rights & Permissions [Opens in a new window]

Extract

It follows constructively from weak versions of Markov's principle (MP) and of Church's thesis (WCT) that logical validity for single sentences is not arithmetically definable. This is a direct consequence of the constructive model-theoretic fact that, using MP and WCT, one can prove the categoricity of first-order Heyting arithmetic. By a straightforward refinement of this proof, we then obtain generalizations of the incompleteness theorem of Kreisel [K 2] as presented by van Dalen [Da] and improved by Leivant [L 1]. An analogous result for classical validity in r.e. models appears in [V].

Our methods of proof are new in that they rely not upon variants of the ideas of [K2] but upon a constructive proof idea inspired by the classical result of Tennenbaum ([Te], [E&K], [S]) on recursive models of arithmetic. This line of reasoning was suggested by the applications of readability to recursive mathematics described in [McC1], [McC2] and [McC3].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 53 , Issue 4 , December 1988 , pp. 1036 - 1041
Copyright
Copyright © Association for Symbolic Logic 1988

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCE

[Da] van Dalen, D., Lectures on intuitionism, Cambridge summer school in mathematical logic (Mathias, A. R. D. and Rogers, H., editors), Lecture Notes in Mathematics, vol. 337, Springer-Verlag, Berlin, 1973, pp. 1–94.CrossRefGoogle Scholar
[Du] Dummett, M. A. E., Elements of intuitionism, Clarendon Press, Oxford, 1977.Google Scholar
[E&K] Ehrenfeucht, A. and Kreisel, G., Strong models for arithmetic, Bulletin de l'Académie Polonaise des Sciences, Série des Sciences Mathématiques, Astronomiques et Physiques, vol. 14 (1966), pp. 107–110.Google Scholar
[K 1] Kreisel, G., Weak completeness of intuitionistic predicate logic, this Journal, vol. 27 (1962), pp. 139–158.Google Scholar
[K 2] Kreisel, G., Church's thesis: A kind of reducibility axiom for constructive mathematics, Intuitionism and proof theory (Kino, A. et al., editors), North-Holland, Amsterdam, 1970, pp. 12–150.Google Scholar
[L1] Leivant, D., Failure of completeness properties of intuitionistic predicate logic for constructive models, Report ZW 48/75, Mathematisch Centrum, Amsterdam, 1975; also Annales Scientifiques de l'Université de Clermont, Série Mathématique , no. 13 (1976), pp. 93–107.Google Scholar
[L2] Leivant, D., The maximality of intuitionistic predicate logic, manuscript, Ohio State University, Columbus, Ohio, 1978.Google Scholar
[McC1] McCarty, C., Realizability and recursive mathematics, D.Phil, thesis, Oxford University, Oxford, 1984; also Technical Report CMU-CS-84-131, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, Pennsylvania, 1984; also Report CST-35-85, Department of Computer Science, Edinburgh University, Edinburgh, 1985.Google Scholar
[McC2] McCarty, C., Realizability and recursive set theory, Annals of Pure and Applied Logic, vol. 32 (1986), pp. 153–183.CrossRefGoogle Scholar
[McC3] McCarty, C., Computation and construction, Oxford University Press, Oxford (to appear).Google Scholar
[McC&T] McCarty, C. and Tennant, N., Skolem's paradox and constructivism, Journal of Philosophical Logic, vol. 16 (1987), pp. 165–202.CrossRefGoogle Scholar
[My] Myhill, J., Constructive set theory, this Journal, vol. 40 (1975), pp. 347–382.Google Scholar
[S] Smoryński, C., Lectures on nonstandard models of arithmetic, Logic Colloquim '82 (Lolli, G. et al., editors), North-Holland, Amsterdam, 1984, pp. 1–70.Google Scholar
[Te] Tennenbaum, S., Non-archimedean models of arithmetic, Notices of the American Mathematical Society, vol. 6 (1959), p. 270.Google Scholar
[Tr 1] Troelstra, A. S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar
[Tr2] Troelstra, A. S. (editor), Completeness and validity for intuitionistic predicate logic, Collogue International de Logique (Clermont-Ferrand, 1975), Colloques Internationaux du CNRS, vol. 249, Éditions du Centre National de la Recherche Scientifique, Paris, 1977, pp. 39–58.Google Scholar
[V] Vaught, R., Sentences true in all constructive models, this Journal, vol. 25 (1960), pp. 39–53.Google Scholar