{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T10:05:48Z","timestamp":1775037948104,"version":"3.50.1"},"reference-count":15,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":6951,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1995,3]]},"abstract":"If it is difficult to give the exact significance of consistency proofs from a classical point of view, in particular the proofs of Gentzen [2, 6], and Novikoff [14], the motivations of these proofs are quite clear intuitionistically. Their significance is then less to give a mere consistency proof than to present an intuitionistic explanation of the notion of classical truth. Gentzen for instance summarizes his proof as follows [6]: \u201cThus propositions of actualist mathematics seem to have a certain utility, but no sense<\/jats:italic>. The major part of my consistency proof, however, consists precisely in ascribing a finitist sense<\/jats:italic> to actualist propositions.\u201d From this point of view, the main part of both Gentzen's and Novikoff's arguments can be stated as establishing that modus ponens is valid w.r.t. this interpretation ascribing a \u201cfinitist sense\u201d to classical propositions.<\/jats:p>In this paper, we reformulate Gentzen's and Novikoff's \u201cfinitist sense\u201d of an arithmetic proposition as a winning strategy for a game associated to it. (To see a proof as a winning strategy has been considered by Lorenzen [10] for intuitionistic logic.) In the light of concurrency theory [7], it is tempting to consider a strategy as an interactive program (which represents thus the \u201cfinitist sense\u201d of an arithmetic proposition). We shall show that the validity of modus ponens then gets a quite natural formulation, showing that \u201cinternal chatters\u201d between two programs end eventually.<\/jats:p>We first present Novikoff's notion of regular<\/jats:italic> formulae, that can be seen as an intuitionistic truth definition for classical infinitary propositional calculus. We use this in order to motivate the second part, which presents a game-theoretic interpretation of the notion of regular formulae, and a proof of the admissibility of modus ponens which is based on this interpretation.<\/jats:p>","DOI":"10.2307\/2275524","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:54:10Z","timestamp":1146956050000},"page":"325-337","source":"Crossref","is-referenced-by-count":73,"title":["A semantics of evidence for classical arithmetic"],"prefix":"10.1017","volume":"60","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200019046_ref014","first-page":"230","article-title":"On the consistency of certain logical calculus","volume":"54","author":"Novikoff","year":"1943","journal-title":"Matematiceskij sbornik (Recueil-Math\u00e9matique, T.12)"},{"key":"S0022481200019046_ref0012","first-page":"385","volume":"56","author":"Mints","year":"1991","journal-title":"Proof theory in the USSR, 1925-1969"},{"key":"S0022481200019046_ref010","first-page":"193","volume-title":"Infinitistic methods","author":"Lorenzen","year":"1962"},{"key":"S0022481200019046_ref009","first-page":"50","volume":"17","author":"Kreisel","year":"1952","journal-title":"Interpretation of non-finitist proofs"},{"key":"S0022481200019046_ref008","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1952"},{"key":"S0022481200019046_ref013","unstructured":"Murthy C. , Extracting constructive content from classical proofs, Ph.D. thesis , Cornell University, 1990."},{"key":"S0022481200019046_ref007","volume-title":"Communicating sequential processes","author":"Hoare","year":"1985"},{"key":"S0022481200019046_ref005","volume-title":"Technical Report TR 85\u2013684","author":"Constable","year":"1985"},{"key":"S0022481200019046_ref003","doi-asserted-by":"publisher","DOI":"10.4064\/fm-77-2-151-166"},{"key":"S0022481200019046_ref002","first-page":"409","volume-title":"Intuitionism and proof theory","author":"Bernays","year":"1970"},{"key":"S0022481200019046_ref001","first-page":"3","volume-title":"Theoretical Computer Science","author":"Abramsky","year":"1993"},{"key":"S0022481200019046_ref0011","volume-title":"Notes on constructive mathematics","author":"Martin-L\u00f6f","year":"1970"},{"key":"S0022481200019046_ref004","first-page":"129","volume":"11","author":"Church","year":"1946","journal-title":"Review of Novikoff's article"},{"key":"S0022481200019046_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0079691"},{"key":"S0022481200019046_ref006","volume-title":"The collected papers of Gerhard Gentzen","author":"Gentzen","year":"1969"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200019046","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T19:31:00Z","timestamp":1557862260000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200019046\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["S0022481200019046"],"URL":"https:\/\/doi.org\/10.2307\/2275524","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}