-
779Strong normalization of a symmetric lambda calculus for second-order classical logicArchive for Mathematical Logic 41 (1): 91-99. 2002.We extend Barbanera and Berardi's symmetric lambda calculus [2] to second-order classical propositional logic and prove its strong normalization.
-
601Consistency proof of a fragment of pv with substitution in bounded arithmeticJournal of Symbolic Logic 83 (3): 1063-1090. 2018.This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved and either its left- o…Read more
-
520This paper considers Rumfitt’s bilateral classical logic (BCL), which is proposed to counter Dummett’s challenge to classical logic. First, agreeing with several authors, we argue that Rumfitt’s notion of harmony, used to justify logical rules by a purely proof theoretical manner, is not sufficient to justify coordination rules in BCL purely proof-theoretically. For the central part of this paper, we propose a notion of proof-theoretical validity similar to Prawitz for BCL and proves that BCL is…Read more
-
45A sequent calculus for Limit Computable MathematicsAnnals of Pure and Applied Logic 153 (1-3): 111-126. 2008.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 comp…Read more
-
6On Proving Consistency of Equational Theories in Bounded ArithmeticJournal of Symbolic Logic 90 (1): 135-165. 2025.We consider equational theories based on axioms for recursively defining functions, with rules for equality and substitution, but no form of induction—we denote such equational theories as PETS for pure equational theories with substitution. An example is Cook’s system PV without its rule for induction. We show that the Bounded Arithmetic theory $\mathrm {S}^{1}_2$ proves the consistency of PETS. Our approach employs model-theoretic constructions for PETS based on approximate values resembling n…Read more
Areas of Specialization
Logic and Philosophy of Logic |
Computer Science |
Mathematical Logic |
Areas of Interest
Logic and Philosophy of Logic |
Computer Science |
Mathematical Logic |