Hostname: page-component-848d4c4894-pftt2 Total loading time: 0 Render date: 2024-05-28T15:43:29.231Z Has data issue: false hasContentIssue false
  • English
  • Français

The faithfulness of the interpretation of arithmetic in the theory of constructions

Published online by Cambridge University Press:  12 March 2014

Nicolas D. Goodman
Nicolas D. Goodman*
Affiliation:
State University of New York at Buffalo, Amherst, New York 14226
Get access Rights & Permissions [Opens in a new window]

Extract

In my paper [1], with which I assume the reader is familiar, I defined an arithmetic theory of constructions ATC and gave an interpretation of intuitionistic arithmetic HA in ATC. I proved that, in a suitable sense, every formula provable in HA is also provable in ATC. I proved the converse of this result only for positive sentences. In the present paper I will prove in full generality that any formula of HA which is provable in ATC is already provable in HA. In a later paper I shall use this result to obtain new information about certain extensions of HA by addition of higher types.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 38 , Issue 3 , September 1973 , pp. 453 - 459
Copyright
Copyright © Association for Symbolic Logic 1973

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

REFERENCES

[1]Goodman, N. D., The arithmetic theory of constructions, Proceedings of the Cambridge Conference on Mathematical Logic (Mathias, A. R. D., Editor), Springer (to appear).Google Scholar
[2]Kleene, S. C. and Vesley, R. E., The foundations of intuitionistic mathematics, North-Holland, Amsterdam, 1965.Google Scholar
[3]Troelstra, A. S., The theory of choice sequences, Logic, Methodology, and Philosophy of Science. III, (van Rootselaar, B. and Staal, J. F., Editors), North-Holland, Amsterdam, 1968, pp. 201–223.Google Scholar