Hostname: page-component-78c5997874-8bhkd Total loading time: 0 Render date: 2024-11-04T19:07:21.806Z Has data issue: false hasContentIssue false
  • English
  • Français

Flagg realizability in arithmetic

Published online by Cambridge University Press:  12 March 2014

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

Extract

Epistemic arithmetic—that is, first-order arithmetic with S4 as the underlying logic—was introduced by Shapiro in [7] and independently by Reinhardt in [6]. Shapiro showed that intuitionistic first-order arithmetic HA can be embedded in epistemic arithmetic EA . Moreover he showed that some of the basic proof-theoretic facts about HA , such as the existence and disjunction properties, can be extended to EA . In [3] we showed that the interpretation of HA in EA is faithful. (G.E. Mine has independently also proved this theorem.) Finally, in [2], Flagg showed that a suitable form of Church's thesis is consistent with EA . (Carlson [1] has announced another proof of this result.) Flagg's argument involves an ingenious realizability notion for EA which, as it stands, is not very perspicuous. The purpose of the present paper is to give a more transparent treatment of Flagg realizability. We obtain a new version of Flagg's proof of the consistency of Church's thesis with EA . Our main new result is that, in a sense to be made precise below, Flagg realizability coincides on HA embedded in EA with Kleene's 1945 realizability (e.g. see [5, pp. 501–516]). Thus it turns out once more that methods and results proved for EA can be viewed as extensions or generalizations of well-known methods and results for HA .

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 51 , Issue 2 , June 1986 , pp. 387 - 392
Copyright
Copyright © Association for Symbolic Logic 1986

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.)

Footnotes

1

Preparation of this paper was supported in part by NSF Grant No. SES8411917.

References

REFERENCES

[1] Carlson, T., Epistemic arithmetic and a conjecture of Reinhardt (abstract).Google Scholar
[2] Flagg, R. C., Church's thesis is consistent with epistemic arithmetic, Intensional mathematics (Shapiro, S., editor), North-Holland, Amsterdam, 1985, pp. 121–172.CrossRefGoogle Scholar
[3] Goodman, N. D., Epistemic arithmetic is a conservative extension of intuitionistic arithmetic, this Journal, vol. 49 (1984), pp. 192–203.Google Scholar
[4] Kleene, S. C., Disjunction and existence under implication in elementary intuitionistic formalisms, this Journal, vol. 27 (1962), pp. 11–18.Google Scholar
[5] Kleene, S. C., Introduction to metamathematics, Van Nostrand, New York, 1952.Google Scholar
[6] Reinhardt, W. N., The consistency of a variant of Church's thesis with an axiomatic theory of an epistemic notion (preprint).Google Scholar
[7] Shapiro, S., Epistemic and intuitionistic arithmetic, Intensional mathematics (Shapiro, S., editor), North-Holland, Amsterdam, 1985, pp. 11–46.CrossRefGoogle Scholar