4 found
  1.  44
    A Refinement of de Bruijn's Formal Language of Mathematics.Fairouz Kamareddine & Rob Nederpelt - 2004 - Journal of Logic, Language and Information 13 (3):287-340.
    We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.
    Direct download (9 more)  
    Export citation  
    Bookmark   2 citations  
  2.  28
    A Modern Elaboration of the Ramified Theory of Types.Twan Laan & Rob Nederpelt - 1996 - Studia Logica 57 (2-3):243 - 278.
    The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica [32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like [25], [19], [6] and [7]).As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern (...)
    Direct download (5 more)  
    Export citation  
    Bookmark   2 citations  
  3.  28
    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 (...)
    Direct download (10 more)  
    Export citation  
    Bookmark   1 citation  
  4.  12
    On Π-Conversion in the Λ-Cube and the Combination with Abbreviations.Fairouz Kamareddine, Roel Bloo & Rob Nederpelt - 1999 - Annals of Pure and Applied Logic 97 (1-3):27-45.
    Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...)
    Direct download (4 more)  
    Export citation