16 found
Order:
See also
Stefano Berardi
Università degli Studi di Torino
  1.  31
    Games with 1-Backtracking.Stefano Berardi, Thierry Coquand & Susumu Hayashi - 2010 - Annals of Pure and Applied Logic 161 (10):1254-1269.
    We associate with any game G another game, which is a variant of it, and which we call . Winning strategies for have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over , and vice versa. Through we can express in algorithmic form, as a recursive winning strategy, many common proofs of non-constructive Mathematics, namely exactly the theorems of the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  2.  66
    On the Computational Content of the Axiom of Choice.Stefano Berardi, Marc Bezem & Thierry Coquand - 1998 - Journal of Symbolic Logic 63 (2):600-622.
    We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  3.  12
    An Intuitionistic Version of Ramsey's Theorem and its Use in Program Termination.Stefano Berardi & Silvia Steila - 2015 - Annals of Pure and Applied Logic 166 (12):1382-1406.
  4.  30
    A Generalization of Conservativity Theorem for Classical Versus Intuitionistic Arithmetic.Stefano Berardi - 2004 - Mathematical Logic Quarterly 50 (1):41.
    A basic result in intuitionism is Π02-conservativity. Take any proof p in classical arithmetic of some Π02-statement , with P decidable). Then we may effectively turn p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof p of an arithmetical statement ∀x.∃y.P, with P of degree k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree k formulas. When k = 0, (...)
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  5
    Ramsey’s Theorem for Pairs and K Colors as a Sub-Classical Principle of Arithmetic.Stefano Berardi & Silvia Steila - 2017 - Journal of Symbolic Logic 82 (2):737-753.
    The purpose is to study the strength of Ramsey’s Theorem for pairs restricted to recursive assignments ofk-many colors, with respect to Intuitionistic Heyting Arithmetic. We prove that for every natural number$k \ge 2$, Ramsey’s Theorem for pairs and recursive assignments ofkcolors is equivalent to the Limited Lesser Principle of Omniscience for${\rm{\Sigma }}_3^0$formulas over Heyting Arithmetic. Alternatively, the same theorem over intuitionistic arithmetic is equivalent to: for every recursively enumerable infinitek-ary tree there is some$i < k$and some branch with infinitely many (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  4
    A Sequent Calculus for Limit Computable Mathematics.Stefano Berardi & Yoriyuki Yamagata - 2008 - Annals of Pure and Applied Logic 153 (1-3):111-126.
    We introduce an implication-free fragment image of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in image. Our main result is that cut-free proofs of image are isomorphic with recursive winning strategies of a set of games called “1-backtracking games” in [S. Berardi, Th. Coquand, S. Hayashi, Games with 1-backtracking, Games for Logic and Programming Languages, Edinburgh, April 2005].We also show that image is a sound and complete formal system for the implication-free (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  7
    Krivine's Intuitionistic Proof of Classical Completeness.Stefano Berardi & Silvio Valentini - 2004 - Annals of Pure and Applied Logic 129 (1-3):93-106.
    In 1996, Krivine applied Friedman's A-translation in order to get an intuitionistic version of Gödel completeness result for first-order classical logic and countable languages and models. Such a result is known to be intuitionistically underivable 559), but Krivine was able to derive intuitionistically a weak form of it, namely, he proved that every consistent classical theory has a model. In this paper, we want to analyze the ideas Krivine's remarkable result relies on, ideas which where somehow hidden by the heavy (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  8.  2
    Some Intuitionistic Equivalents of Classical Principles for Degree 2 Formulas.Stefano Berardi - 2006 - Annals of Pure and Applied Logic 139 (1):185-200.
    We consider the restriction of classical principles like Excluded Middle, Markov’s Principle, König’s Lemma to arithmetical formulas of degree 2. For any such principle, we find simple mathematical statements which are intuitionistically equivalent to it, provided we restrict universal quantifications over maps to computable maps.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  9.  17
    A Parallel Game Semantics for Linear Logic.Stefano Baratella & Stefano Berardi - 1997 - Archive for Mathematical Logic 36 (3):189-217.
    We describe the constructive content of proofs in a fragment of propositional Infinitary Linear Logic in terms of strategies for a suitable class of games. Such strategies interpret linear proofs as parallel algorithms as long as the asymmetry of the connectives ? and ! allows it.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  10.  25
    A Constructive Valuation Semantics for Classical Logic.Franco Barbanera & Stefano Berardi - 1996 - Notre Dame Journal of Formal Logic 37 (3):462-482.
    This paper presents a constructive interpretation for the proofs in classical logic of $\Sigma^0_1$ -sentences and for a witness extraction procedure based on Prawitz's reduction rules.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  11.  16
    Equalization of Finite Flowers.Stefano Berardi - 1988 - Journal of Symbolic Logic 53 (1):105-123.
  12.  8
    Preface.Steffen van Bakel, Stefano Berardi & Ulrich Berger - 2010 - Annals of Pure and Applied Logic 161 (11):1313-1314.
  13.  36
    Intuitionistic Completeness for First Order Classical Logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
    In the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic. All results included here, but a part of the proposition (a) below, are new. This work is, ideally, (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  4
    Preface.Steffen van Bakel, Stefano Berardi & Ulrich Berger - 2013 - Annals of Pure and Applied Logic 164 (6):589-590.
  15.  8
    A Strong Normalization Result for Classical Logic.Franco Barbanera & Stefano Berardi - 1995 - Annals of Pure and Applied Logic 76 (2):99-116.
    In this paper we give a strong normalization proof for a set of reduction rules for classical logic. These reductions, more general than the ones usually considered in literature, are inspired to the reductions of Felleisen's lambda calculus with continuations.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16.  1
    Preface.Steffen van Bakel & Stefano Berardi - 2008 - Annals of Pure and Applied Logic 153 (1-3):1-2.