Switch to: References

Add citations

You must login to add citations.
  1. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Types in logic and mathematics before 1940.Fairouz Kamareddine, Twan Laan & Rob Nederpelt - 2002 - Bulletin of Symbolic Logic 8 (2):185-245.
    In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • ALONZO: Deduktionsagenten höherer Ordnung für Mathematische Assistenzsysteme.Benzmüller Christoph - 2003
    Download  
     
    Export citation  
     
    Bookmark