Switch to: References

Add citations

You must login to add citations.
  1. Reverse Mathematics and Uniformity in Proofs without Excluded Middle.Jeffry L. Hirst & Carl Mummert - 2011 - Notre Dame Journal of Formal Logic 52 (2):149-162.
    We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a $\Pi^1_2$ sentence of a certain form is provable using E-HA ${}^\omega$ along with the axiom of choice and an independence of premise principle, the sequential form of the statement is provable in the classical system RCA. We obtain this and similar results using applications of modified realizability and the Dialectica interpretation. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • On Goodman Realizability.Emanuele Frittaion - 2019 - Notre Dame Journal of Formal Logic 60 (3):523-550.
    Goodman’s theorem states that HAω+AC+RDC is conservative over HA. The same result applies to the extensional case, that is, E-HAω+AC+RDC is also conservative over HA. This is due to Beeson. In this article, we modified the Goodman realizability and provide a new proof of the extensional case.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation