A realizability interpretation for classical analysis. Towsner, H. Arch. Math. Logic, 43(7):891–900, 2004. Journal Pdf doi abstract bibtex We present a realizability interpretation for classical analysis—an association of a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of Π2 sentences ∀ x ∃ y A(x,y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x,y).
@article {MR2096140,
AUTHOR = {Towsner, Henry},
TITLE = {A realizability interpretation for classical analysis},
JOURNAL = {Arch. Math. Logic},
FJOURNAL = {Archive for Mathematical Logic},
VOLUME = {43},
YEAR = {2004},
NUMBER = {7},
PAGES = {891--900},
ISSN = {0933-5846},
CODEN = {AMLOEH},
MRCLASS = {03F35 (03F05)},
MRNUMBER = {2096140 (2005i:03070)},
MRREVIEWER = {Thomas Strahm},
DOI = {10.1007/s00153-004-0233-3},
URLJOURNAL= {http://dx.doi.org/10.1007/s00153-004-0233-3},
urlpdf={http://www.sas.upenn.edu/~htowsner/realize.pdf},
abstract={We present a realizability interpretation for classical analysis—an association
of a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of Π<sub>2</sub> sentences ∀ x ∃ y A(x,y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x,y).},
}
Downloads: 0
{"_id":{"_str":"51f58c5128e84a503b000004"},"__v":145,"authorIDs":["3GEPwq9joMrcxxoCw","4KQet7uefuvLzwtpx","545832462abc8e9f37000b09","5c8vhjzWNNjGW4qbh","5decfea43d02efdf010000be","5def8c8545114dde01000167","5df216ace4cb4ede0100016b","5e04f7d6fff612df01000139","5e07fc92cdee3adf0100003b","5e0b8c33ca6111df010000a2","5e0fd5b12cfae9df010000b2","5e10e8e545c12cde01000086","5e15529bedfb1ede01000156","5e1ae0065f3d2cdf01000075","5e25e33da6f19fde010000f0","5e2ecddbc2015cde01000106","5e2f2e7378a7cedf01000043","5e2f7d669ca24fdf010001e9","5e31874200e4e5de010000f3","5e349b4753b794de01000107","5e3871a21f8af9e0010000f6","5e3d9a82f33211df01000085","5e3daa13f33211df01000192","5e405ccaaeea22df0100009b","5e442d87e5a34dde010000ac","5e4a4b925675c1de01000107","5e51554afe5af9df01000104","5e52ae476a3abede0100003e","5e599979ad6c7fde0100004a","5e5c8dfa9933dade01000017","5e5d5d37ad47bcde010000c0","5e5e8a77c0a53dde01000054","5e5e9e03c0a53dde0100025f","5e64727de1ac00de010000d6","8eyEAbrHsTiQjrh7m","9xwKHbohnMHpGd326","AKhMye69vFo9ZBkJn","B8ktHCTYohgyN3zHd","BeL58hABvbynGFvkM","E6dySSeKcY8eAMMJB","EHJuZpHSt5bw4erqn","EjhY4z5ziCGtFZAAp","Fr8xk6h7QLy2uc6qT","HGCndpBQapLkeXcCv","JXPiBhJhKZpboe3cv","KYQ2gtq5nH4r2yEXs","M5pdPBbKqC9YYHd6n","PKNH7m7rTTAWiLt3x","Pz5HyZqksZg56dyuD","QJDeWCekzoGrAH7hG","QWy8CzoFcY4jkh9XS","RWoRfxCmeqb6fsA7N","RiWhh5sCAejRxYRtr","TdZKmjjXfpX5riMhc","W8K2TwaE7YMfqQquc","W9X6jnrT5WndXxz4f","WJ4bEb9E3XqnkvyCX","XMaQnCeR8pCaxKwS6","ZB6i2RZxTFGTnNJcr","ZfXCGDcjZMeE4QSqP","b9AcCuxsqzpiCMFsG","cNR3H4e3QEnD3WkbJ","cnQY9tt7BQH92KkyP","fDCSEz7FfSCxERX9L","fkakjW7HDbgrSiTnc","g2bZv9uHbxMAPTro2","mgLyDAsFS9g7HNyuT","n6SFWyWp7WHG5YnrG","nDtKTAspawBCun8X8","nJTiiRRLbohMDGYgA","nvTYkDHXvRYJbiLqm","o6p92SSgdiePc5yu8","oNpdLEjNerjoioXTr","qTYgvoePYaSXGnmPe","t9d9TPHkaTGkNr5RP","tYHK4CxbC8KJ8CgMF","vymEvveSkq34uS28E","wm9ugGRCbkcFjNxF5","xJZc77uii7zQDbato","xvWPite86SqosFSo5"],"author_short":["Towsner, H."],"bibbaseid":"towsner-arealizabilityinterpretationforclassicalanalysis-2004","bibdata":{"bibtype":"article","type":"article","author":[{"propositions":[],"lastnames":["Towsner"],"firstnames":["Henry"],"suffixes":[]}],"title":"A realizability interpretation for classical analysis","journal":"Arch. Math. Logic","fjournal":"Archive for Mathematical Logic","volume":"43","year":"2004","number":"7","pages":"891–900","issn":"0933-5846","coden":"AMLOEH","mrclass":"03F35 (03F05)","mrnumber":"2096140 (2005i:03070)","mrreviewer":"Thomas Strahm","doi":"10.1007/s00153-004-0233-3","urljournal":"http://dx.doi.org/10.1007/s00153-004-0233-3","urlpdf":"http://www.sas.upenn.edu/~htowsner/realize.pdf","abstract":"We present a realizability interpretation for classical analysis—an association of a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of Π<sub>2</sub> sentences ∀ x ∃ y A(x,y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x,y).","bibtex":"@article {MR2096140,\n AUTHOR = {Towsner, Henry},\n TITLE = {A realizability interpretation for classical analysis},\n JOURNAL = {Arch. Math. Logic},\n FJOURNAL = {Archive for Mathematical Logic},\n VOLUME = {43},\n YEAR = {2004},\n NUMBER = {7},\n PAGES = {891--900},\n ISSN = {0933-5846},\n CODEN = {AMLOEH},\n MRCLASS = {03F35 (03F05)},\n MRNUMBER = {2096140 (2005i:03070)},\nMRREVIEWER = {Thomas Strahm},\n DOI = {10.1007/s00153-004-0233-3},\n URLJOURNAL= {http://dx.doi.org/10.1007/s00153-004-0233-3},\nurlpdf={http://www.sas.upenn.edu/~htowsner/realize.pdf},\nabstract={We present a realizability interpretation for classical analysis—an association\nof a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of Π<sub>2</sub> sentences ∀ x ∃ y A(x,y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x,y).},\n}\n","author_short":["Towsner, H."],"key":"MR2096140","id":"MR2096140","bibbaseid":"towsner-arealizabilityinterpretationforclassicalanalysis-2004","role":"author","urls":{"Journal":"http://dx.doi.org/10.1007/s00153-004-0233-3","Pdf":"http://www.sas.upenn.edu/~htowsner/realize.pdf"},"metadata":{"authorlinks":{"towsner, h":"https://www.sas.upenn.edu/~htowsner/index.html"}}},"bibtype":"article","biburl":"www.sas.upenn.edu/~htowsner/papers.bib","downloads":57,"keywords":[],"search_terms":["realizability","interpretation","classical","analysis","towsner"],"title":"A realizability interpretation for classical analysis","title_words":["realizability","interpretation","classical","analysis"],"year":2004,"dataSources":["6NR8bS3FWz4thtH6K","HbyKaYarx2Kg7vovB"]}