7 found
Order:
  1.  14
    Epsilon Substitution Method for Elementary Analysis.Grigori Mints, Sergei Tupailo & Wilfried Buchholz - 1996 - Archive for Mathematical Logic 35 (2):103-130.
    We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   20 citations  
  2. Realization of Analysis Into Explicit Mathematics.Sergei Tupailo - 2001 - Journal of Symbolic Logic 66 (4):1848-1864.
    We define a novel interpretation R of second order arithmetic into Explicit Mathematics. As a difference from standard D-interpretation, which was used before and was shown to interpret only subsystems proof-theoretically weaker than T 0 , our interpretation can reach the full strength of T 0 . The R-interpretation is an adaptation of Kleene's recursive realizability, and is applicable only to intuitionistic theories.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  3.  18
    Characterizing the Interpretation of Set Theory in Martin-Löf Type Theory.Michael Rathjen & Sergei Tupailo - 2006 - Annals of Pure and Applied Logic 141 (3):442-471.
    Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice.The paper builds on a self-interpretation (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  4.  15
    Realization of Constructive Set Theory Into Explicit Mathematics: A Lower Bound for Impredicative Mahlo Universe.Sergei Tupailo - 2003 - Annals of Pure and Applied Logic 120 (1-3):165-196.
    We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T 0 , thus providing relative lower bounds for the proof-theoretic strength of the latter.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  5.  20
    On the Intuitionistic Strength of Monotone Inductive Definitions.Sergei Tupailo - 2004 - Journal of Symbolic Logic 69 (3):790-798.
    We prove here that the intuitionistic theory $T_{0}\upharpoonright + UMID_{N}$ , or even $EEJ\upharpoonright + UMID_{N}$ , of Explicit Mathematics has the strength of $\prod_{2}^{1} - CA_{0}$ . In Section I we give a double-negation translation for the classical second-order $\mu-calculus$ , which was shown in [ $M\ddot{o}02$ ] to have the strength of $\prod_{2}^{1}-CA_{0}$ . In Section 2 we interpret the intuitionistic $\mu-calculus$ in the theory $EETJ\upharpoonright + UMID_{N}$ . The question about the strength of monotone inductive definitions in (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  25
    Consistency of Strictly Impredicative NF and a Little More ….Sergei Tupailo - 2010 - Journal of Symbolic Logic 75 (4):1326-1338.
    An instance of Stratified Comprehension ∀x₁ … ∀x n ∃y∀x (x ∈ y ↔ φ(x, x₁, …, x n )) is called strictly impredicative iff, under minimal stratification, the type of x is 0. Using the technology of forcing, we prove that the fragment of NF based on strictly impredicative Stratified Comprehension is consistent. A crucial part in this proof, namely showing genericity of a certain symmetric filter, is due to Robert Solovay. As a bonus, our interpretation also satisfies some (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7. Fixpoints of Models Constructions.Sergei Tupailo - 2007 - Logique Et Analyse 50:63-78.