15 found
Order:
  1.  44
    A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
    We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  2.  13
    A Very Absolute Pi-1-2 Real Singleton.René David - 1982 - Annals of Mathematical Logic 23 (2-3):101-120.
    I give a class forcing that adds a real which is Pi-1-2 and for which no forcing extension (by a set of conditions) can destroy this definability.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  3.  17
    Kenneth McAloon. On the Sequence of Models HODn. Fundamenta Mathematicae, Vol. 82 , Pp. 85–93. - Thomas J. Jech. Forcing with Trees and Ordinal Definability. Annals of Mathematical Logic, Vol. 7 No. 4 , Pp. 387–409. - Włodzimierz Zadrożny. Iterating Ordinal Definability. Annals of Pure and Applied Logic, Vol. 24 , Pp. 263–310. [REVIEW]René David - 1987 - Journal of Symbolic Logic 52 (2):570-571.
  4.  8
    Δ31 Reals.René David - 1982 - Annals of Mathematical Logic 23 (2-3):121-125.
  5.  8
    Normalization Without Reducibility.René David - 2000 - Annals of Pure and Applied Logic 107 (1-3):121-130.
    In [gallier], general results (due to Coppo, Dezani and Veneri) relating properties of pure lambda terms and their typability in some systems with conjunctive types are proved in a uniform way by using the reducibility method.This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  63
    Storage Operators and Directed Lambda-Calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
    Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability of the set (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark  
  7.  3
    A Very Absolute Π21 Real Singleton.René David - 1982 - Annals of Mathematical Logic 23 (2-3):101-120.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8.  33
    Λμ-Calculus and Böhm's Theorem.René David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
    The λμ-calculus is an extension of the λ-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Bohm's theorem fails in this calculus.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  48
    $Lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
    The $\lambda\mu$-calculus is an extension of the $\lambda$-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Bohm's theorem fails in this calculus.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  10.  46
    Counting Proofs in Propositional Logic.René David & Marek Zaionc - 2009 - Archive for Mathematical Logic 48 (2):185-199.
    We give a procedure for counting the number of different proofs of a formula in various sorts of propositional logic. This number is either an integer (that may be 0 if the formula is not provable) or infinite.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark  
  11.  15
    Review: Kenneth McAloon, On the Sequence of Models $Operatorname{HOD}_n$; Thomas J. Jech, Forcing with Trees and Ordinal Definability; Wlodzimierz Zadrozny, Iterating Ordinal Definability. [REVIEW]Rene David - 1987 - Journal of Symbolic Logic 52 (2):570-571.
  12.  18
    A Result of Relative Consistency About the Predicate WO(Δ, Κ).René David - 1980 - Journal of Symbolic Logic 45 (3):483-492.
  13.  6
    Strong Normalization Results by Translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.
    We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark  
  14.  6
    Domains and Lambda-Calculi.René David - 2004 - Bulletin of Symbolic Logic 10 (2):211-213.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  15. REVIEWS-Domains and Lambda-Calculi.R. Amadio, P. L. Curien & Rene David - 2004 - Bulletin of Symbolic Logic 10 (2):211-212.
     
    Export citation  
     
    Bookmark