10 found
Order:
  1. Reverse mathematics and π21 comprehension.Carl Mummert & Stephen G. Simpson - 2005 - Bulletin of Symbolic Logic 11 (4):526-533.
    We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π2 1 comprehension. An MF space is defined to be a topological space of the form MF(P) with the topology generated by $\lbrace N_p \mid p \in P \rbrace$ . Here P is a poset, MF(P) is the set of maximal filters on P, and $N_p = \lbrace F \in MF(P) \mid p \in F \rbrace$ . If the poset P is countable, (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  2.  17
    Reverse Mathematics and Π 1 2 Comprehension.Carl Mummert & Stephen G. Simpson - 2005 - Bulletin of Symbolic Logic 11 (3):526-533.
    We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π12 comprehension. An MF space is defined to be a topological space of the form MF with the topology generated by {Np ∣ p ϵ P}. Here P is a poset, MF is the set of maximal filters on P, and Np = {F ϵ MF ∣ p ϵ F }. If the poset P is countable, the space MF is said to (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  3.  24
    Reverse mathematics of mf spaces.Carl Mummert - 2006 - Journal of Mathematical Logic 6 (2):203-232.
    This paper gives a formalization of general topology in second-order arithmetic using countably based MF spaces. This formalization is used to study the reverse mathematics of general topology. For each poset P we let MF denote the set of maximal filters on P endowed with the topology generated by {Np | p ∈ P}, where Np = {F ∈ MF | p ∈ F}. We define a countably based MF space to be a space of the form MF for some (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  4.  40
    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  
  5.  22
    Using Ramsey’s theorem once.Jeffry L. Hirst & Carl Mummert - 2019 - Archive for Mathematical Logic 58 (7-8):857-866.
    We show that \\) cannot be proved with one typical application of \\) in an intuitionistic extension of \ to higher types, but that this does not remain true when the law of the excluded middle is added. The argument uses Kohlenbach’s axiomatization of higher order reverse mathematics, results related to modified reducibility, and a formalization of Weihrauch reducibility.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  39
    Filters on Computable Posets.Steffen Lempp & Carl Mummert - 2006 - Notre Dame Journal of Formal Logic 47 (4):479-485.
    We explore the problem of constructing maximal and unbounded filters on computable posets. We obtain both computability results and reverse mathematics results. A maximal filter is one that does not extend to a larger filter. We show that every computable poset has a \Delta^0_2 maximal filter, and there is a computable poset with no \Pi^0_1 or \Sigma^0_1 maximal filter. There is a computable poset on which every maximal filter is Turing complete. We obtain the reverse mathematics result that the principle (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  7.  96
    An incompleteness theorem for β n -models.Carl Mummert & Stephen G. Simpson - 2004 - Journal of Symbolic Logic 69 (2):612-616.
    Let n be a positive integer. By a $\beta_{n}-model$ we mean an $\omega-model$ which is elementary with respect to $\sigma_{n}^{1}$ formulas. We prove the following $\beta_{n}-model$ version of $G\ddot{o}del's$ Second Incompleteness Theorem. For any recursively axiomatized theory S in the language of second order arithmetic, if there exists a $\beta_{n}-model$ of S, then there exists a $\beta_{n}-model$ of S + "there is no countable $\beta_{n}-model$ of S". We also prove a $\beta_{n}-model$ version of $L\ddot{o}b's$ Theorem. As a corollary, we obtain (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  8.  25
    Reverse mathematics and properties of finite character.Damir D. Dzhafarov & Carl Mummert - 2012 - Annals of Pure and Applied Logic 163 (9):1243-1251.
  9.  54
    Subsystems of second-order arithmetic between RCA0 and WKL0.Carl Mummert - 2008 - Archive for Mathematical Logic 47 (3):205-210.
    We study the Lindenbaum algebra ${\fancyscript{A}}$ (WKL o, RCA o) of sentences in the language of second-order arithmetic that imply RCA o and are provable from WKL o. We explore the relationship between ${\Sigma^1_1}$ sentences in ${\fancyscript{A}}$ (WKL o, RCA o) and ${\Pi^0_1}$ classes of subsets of ω. By applying a result of Binns and Simpson (Arch. Math. Logic 43(3), 399–414, 2004) about ${\Pi^0_1}$ classes, we give a specific embedding of the free distributive lattice with countably many generators into ${\fancyscript{A}}$ (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  32
    The modal logic of Reverse Mathematics.Carl Mummert, Alaeddine Saadaoui & Sean Sovine - 2015 - Archive for Mathematical Logic 54 (3-4):425-437.
    The implication relationship between subsystems in Reverse Mathematics has an underlying logic, which can be used to deduce certain new Reverse Mathematics results from existing ones in a routine way. We use techniques of modal logic to formalize the logic of Reverse Mathematics into a system that we name s-logic. We argue that s-logic captures precisely the “logical” content of the implication and nonimplication relations between subsystems in Reverse Mathematics. We present a sound, complete, decidable, and compact tableau-style deductive system (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark