Order:
Disambiguations
Jesper Carlström [4]J. Carlstrom [1]
  1.  13
    EM + Ext− + ACint is Equivalent to ACext.Jesper Carlström - 2004 - Mathematical Logic Quarterly 50 (3):236-240.
    It is well known that the extensional axiom of choice implies the law of excluded middle . We here prove that the converse holds as well if we have the intensional axiom of choice ACint, which is provable in Martin-Löf's type theory, and a weak extensionality principle , which is provable in Martin-Löf's extensional type theory. In particular, EM is equivalent to ACext in extensional type theory.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  2.  2
    EM + Ext_ + AC~I~N~T is Equivalent to AC~E~X~T.J. Carlstrom - 2004 - Mathematical Logic Quarterly 50 (3):236.
    It is well known that the extensional axiom of choice implies the law of excluded middle. We here prove that the converse holds as well if we have the intensional axiom of choice ACint, which is provable in Martin-Löf's type theory, and a weak extensionality principle, which is provable in Martin-Löf's extensional type theory. In particular, EM is equivalent to ACext in extensional type theory.
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  3.  11
    Interpreting Descriptions in Intensional Type Theory.Jesper Carlström - 2005 - Journal of Symbolic Logic 70 (2):488 - 514.
    Natural deduction systems with indefinite and definite descriptions (ε-terms and ι-terms) are presented, and interpreted in Martin-Löf's intensional type theory. The interpretations are formalizations of ideas which are implicit in the literature of constructive mathematics: if we have proved that an element with a certain property exists, we speak of 'the element such that the property holds' and refer by that phrase to the element constructed in the existence proof. In particular, we deviate from the practice of interpreting descriptions by (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  4.  2
    A Constructive Version of Birkhoff's Theorem.Jesper Carlström - 2008 - Mathematical Logic Quarterly 54 (1):27-34.
    A version of Birkhoff's theorem is proved by constructive, predicative, methods. The version we prove has two conditions more than the classical one. First, the class considered is assumed to contain a generic family, which is defined to be a set-indexed family of algebras such that if an identity is valid in every algebra of this family, it is valid in every algebra of the class. Secondly, the class is assumed to be closed under inductive limits.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography