Hostname: page-component-7b7567c8c-kwt9d Total loading time: 0 Render date: 2026-11-14T21:08:24.495Z Has data issue: false hasContentIssue false

Flagg realizability in arithmetic

Published online by Cambridge University Press:  12 March 2014

Nicolas D. Goodman*
Affiliation:
Department of Mathematics, State University of New York at Buffalo, Buffalo, New York 14214

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 .

Information

Type
Research Article
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.)

Article purchase

Temporarily unavailable