53 found
Sort by:
  1. Toshiyasu Arai (2013). Proof Theory of Weak Compactness. Journal of Mathematical Logic 13 (1):1350003.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Toshiyasu Arai (2011). Exact Bounds on Epsilon Processes. Archive for Mathematical Logic 50 (3):445-458.
    In this paper we show that the lengths of the approximating processes in epsilon substitution method are calculable by ordinal recursions in an optimal way.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. Toshiyasu Arai (2011). Nested PLS. Archive for Mathematical Logic 50 (3-4):395-409.
    In this note we will introduce a class of search problems, called nested Polynomial Local Search (nPLS) problems, and show that definable NP search problems, i.e., ${\Sigma^{b}_{1}}$ -definable functions in ${T^{2}_{2}}$ are characterized in terms of the nested PLS.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Toshiyasu Arai (2011). Quick Cut-Elimination for Strictly Positive Cuts. Annals of Pure and Applied Logic 162 (10):807-815.
    In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Toshiyasu Arai (2010). Wellfoundedness Proofs by Means of Non-Monotonic Inductive Definitions II: First Order Operators. Annals of Pure and Applied Logic 162 (2):107-143.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Toshiyasu Arai (2008). Non‐Elementary Speed‐Ups in Logic Calculi. Mathematical Logic Quarterly 54 (6):629-640.
    In this paper we show some non-elementary speed-ups in logic calculi: Both a predicative second-order logic and a logic for fixed points of positive formulas are shown to have non-elementary speed-ups over first-order logic. Also it is shown that eliminating second-order cut formulas in second-order logic has to increase sizes of proofs super-exponentially, and the same in eliminating second-order epsilon axioms. These are proved by relying on results due to P. Pudlák.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  7. Toshiyasu Arai (2007). On the Consistency Proofs. Journal of the Japan Association for Philosophy of Science 34 (2):91-99.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  8. Toshiyasu Arai (2006). Epsilon Substitution Method for [Image] -FIX. Journal of Symbolic Logic 71 (4):1155 - 1188.
    In this paper we formulate epsilon substitution method for a theory $\Pi _{2}^{0}$-FIX for non-monotonic $\Pi _{2}^{0}$ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  9. Toshiyasu Arai (2005). Ideas in the Epsilon Substitution Method for -FIX. Annals of Pure and Applied Logic 136 (1-2):3-21.
    Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert’s Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,…. The problem is to show that the approximating process terminates. After Gentzen’s innovation, Ackermann [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 162–194] succeeded in proving the termination of the process for the (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  10. Toshiyasu Arai (2004). Proof Theory for Theories of Ordinals II: Π3-Reflection. Annals of Pure and Applied Logic 129 (1-3):39-92.
    This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  11. Toshiyasu Arai (2004). Proof Theory for Theories of Ordinals II:< I> Π_< Sub> 3-Reflection. Annals of Pure and Applied Logic 129 (1):39-92.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  12. Toshiyasu Arai (2004). Wellfoundedness Proofs by Means of Non-Monotonic Inductive Definitions I: Π₂⁰-Operators. Journal of Symbolic Logic 69 (3):830-850.
    In this paper, we prove the wellfoundedness of recursive notation systems for reflecting ordinals up to Π₃-reflection by relevant inductive definitions.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  13. Toshiyasu Arai (2003). Avigad Jeremy. Update Procedures and the 1-Consistency of Arithmetic. Mathematical Logic Quarterly, Vol. 48 (2002), Pp. 3–13. [REVIEW] Bulletin of Symbolic Logic 9 (1):45-47.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  14. Toshiyasu Arai (2003). Epsilon Substitution Method for ID1(Π10∨Σ10). Annals of Pure and Applied Logic 121 (2-3):163-208.
    Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert's Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,… . The problem is to show that the approximating process terminates. After Gentzen's innovation, Ackermann 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints as an Ariadne's (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Toshiyasu Arai (2003). Epsilon Substitution Method for< I> ID< Sub> 1(< I> Π_< Sub> 1< Sup> 0∨< I> Σ< Sub> 1< Sup> 0). [REVIEW] Annals of Pure and Applied Logic 121 (2):163-208.
    Direct download  
     
    My bibliography  
     
    Export citation  
  16. Toshiyasu Arai (2003). Proof Theory for Theories of Ordinals—I: Recursively Mahlo Ordinals. Annals of Pure and Applied Logic 122 (1-3):1-85.
    This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  17. Toshiyasu Arai (2002). Buchholz Wilfried. Notation Systems for Infinitary Derivations. Archive for Mathematical Logic, Vol. 30 No. 5–6 (1991), Pp. 277–296. Buchholz Wilfried. Explaining Gentzen's Consistency Proof Within Infinitary Proof Theory. Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, KGC'97, Vienna, Austria, August 25–29, 1997, Proceedings, Edited by Gottlob Georg, Leitsch Alexander, and Mundici Daniele, Lecture Notes in Computer Science, Vol. 1289, Springer, Berlin, Heidelberg, New York, Etc., 1997 ... [REVIEW] Bulletin of Symbolic Logic 8 (3):437-439.
    Direct download  
     
    My bibliography  
     
    Export citation  
  18. Toshiyasu Arai (2002). Epsilon Substitution Method for Theories of Jump Hierarchies. Archive for Mathematical Logic 41 (2):123-153.
    We formulate epsilon substitution method for theories (H)α0 of absolute jump hierarchies, and give two termination proofs of the H-process: The first proof is an adaption of Mints M, Mints-Tupailo-Buchholz MTB, i.e., based on a cut-elimination of a specially devised infinitary calculus. The second one is an adaption of Ackermann Ack. Each termination proof is based on transfinite induction up to an ordinal θ(α0+ ω)0, which is best possible.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  19. Toshiyasu Arai (2002). On the Slowly Well Orderedness of Εo. Mathematical Logic Quarterly 48 (1):125-130.
    For α < ε0, Nα denotes the number of occurrences of ω in the Cantor normal form of α with the base ω. For a binary number-theoretic function f let B denote the length n of the longest descending chain of ordinals <ε0 such that for all i < n, Nαi ≤ f . Simpson [2] called ε0 as slowly well ordered when B is totally defined for f = K · . Let |n| denote the binary length of the (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  20. Toshiyasu Arai (2002). Review: Wilfried Buchholz, Notation Systems for Infinitary Derivations ; Wilfried Buchholz, Explaining Gentzen's Consistency Proof Within Infinitary Proof Theory ; Sergei Tupailo, Finitary Reductions for Local Predicativity, I: Recursively Regular Ordinals. [REVIEW] Bulletin of Symbolic Logic 8 (3):437-439.
  21. W. Buchholz, S. Tupailo & Toshiyasu Arai (2002). Three Papers on Proof Theory. Bulletin of Symbolic Logic 8 (3):437-438.
     
    My bibliography  
     
    Export citation  
  22. Itay Neeman, Alexander Leitsch, Toshiyasu Arai, Steve Awodey, James Cummings, Rod Downey & Harvey Friedman (2002). 2001 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium'01. Bulletin of Symbolic Logic 8 (1):111-180.
    Direct download  
     
    My bibliography  
     
    Export citation  
  23. Toshiyasu Arai (2000). A Bounded Arithmetic for Frege Systems. Annals of Pure and Applied Logic 103 (1-3):155-199.
    In this paper we introduce a system AID of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss’ propositional consistency proof of Frege systems F in Buss 3–29). We show that AID proves the soundness of F , and conversely any Σ 0 b -theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ 1 b -faithful interpretations between AID+Σ 0 b -CA and (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  24. Toshiyasu Arai (2000). Buss Sam. Preface. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pv. [REVIEW] Bulletin of Symbolic Logic 6 (4):463-464.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  25. Toshiyasu Arai (2000). Buss Samuel R.. First-Order Proof Theory of Arithmetic. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 79–147. [REVIEW] Bulletin of Symbolic Logic 6 (4):465-466.
    Direct download  
     
    My bibliography  
     
    Export citation  
  26. Toshiyasu Arai (2000). Buss Samuel R.. An Introduction to Proof Theory. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pv, Pp. 1–78. [REVIEW] Bulletin of Symbolic Logic 6 (4):464-465.
    Direct download  
     
    My bibliography  
     
    Export citation  
  27. Toshiyasu Arai (2000). Constable Robert L.. Types in Logic, Mathematics and Programming. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 683–786. [REVIEW] Bulletin of Symbolic Logic 6 (4):476-477.
    Direct download  
     
    My bibliography  
     
    Export citation  
  28. Toshiyasu Arai (2000). Fairtlough Matt and Wainer Stanley S.. Hierarchies of Provably Recursive Functions. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 149–207. [REVIEW] Bulletin of Symbolic Logic 6 (4):466-467.
    Direct download  
     
    My bibliography  
     
    Export citation  
  29. Toshiyasu Arai (2000). Japaridze Giorgi and Jongh Dick De. The Logic of Provability. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 475–546. [REVIEW] Bulletin of Symbolic Logic 6 (4):472-473.
    Direct download  
     
    My bibliography  
     
    Export citation  
  30. Toshiyasu Arai (2000). Jäger Gerhard and Stärk Robert F.. A Proof-Theoretic Framework for Logic Programming. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 639–682. [REVIEW] Bulletin of Symbolic Logic 6 (4):475-476.
    Direct download  
     
    My bibliography  
     
    Export citation  
  31. Toshiyasu Arai (2000). Ordinal Diagrams for Π3-Reflection. Journal of Symbolic Logic 65 (3):1375 - 1394.
    In this paper we introduce a recursive notation system O(Π 3 ) of ordinals. An element of the notation system is called an ordinal diagram. The system is designed for proof theoretic study of theories of Π 3 -reflection. We show that for each $\alpha in O(Π 3 ) a set theory KP Π 3 for Π 3 -reflection proves that the initial segment of O(Π 3 ) determined by α is a well ordering. Proof theoretic study for such theories (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  32. Toshiyasu Arai (2000). Ordinal Diagrams for Recursively Mahlo Universes. Archive for Mathematical Logic 39 (5):353-391.
    In this paper we introduce a recursive notation system $O(\mu)$ of ordinals. An element of the notation system is called an ordinal diagram following G. Takeuti [25]. The system is designed for proof theoretic study of theories of recursively Mahlo universes. We show that for each $\alpha<\Omega$ in $O(\mu)$ KPM proves that the initial segment of $O(\mu)$ determined by $\alpha$ is a well ordering. Proof theoretic study for such theories will be reported in [9].
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. Toshiyasu Arai (2000). Pudlák Pavel. The Lengths of Proofs. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 547–637. [REVIEW] Bulletin of Symbolic Logic 6 (4):473-475.
    Direct download  
     
    My bibliography  
     
    Export citation  
  34. Toshiyasu Arai (2000). Pohlers Wolfram. Subsystems of Set Theory and Second-Order Number Theory. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 209–335. [REVIEW] Bulletin of Symbolic Logic 6 (4):467-469.
    Direct download  
     
    My bibliography  
     
    Export citation  
  35. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: An Introduction to Proof Theory. [REVIEW] Bulletin of Symbolic Logic 6 (4):464-465.
    Direct download  
     
    My bibliography  
     
    Export citation  
  36. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: The Lengths of Proofs. [REVIEW] Bulletin of Symbolic Logic 6 (4):473-475.
    Direct download  
     
    My bibliography  
     
    Export citation  
  37. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: Subsystems of Set Theory and Second-Order Number Theory. [REVIEW] Bulletin of Symbolic Logic 6 (4):467-469.
    Direct download  
     
    My bibliography  
     
    Export citation  
  38. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: Gödel's Functional ("Dialectica") Interpretation. [REVIEW] Bulletin of Symbolic Logic 6 (4):469-470.
    Direct download  
     
    My bibliography  
     
    Export citation  
  39. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: Hierarchies of Provably Recursive Functions. [REVIEW] Bulletin of Symbolic Logic 6 (4):466-467.
    Direct download  
     
    My bibliography  
     
    Export citation  
  40. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: A Proof-Theoretic Framework for Logic Programming. [REVIEW] Bulletin of Symbolic Logic 6 (4):475-476.
    Direct download  
     
    My bibliography  
     
    Export citation  
  41. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: The Logic of Provability. [REVIEW] Bulletin of Symbolic Logic 6 (4):74-75.
    Direct download  
     
    My bibliography  
     
    Export citation  
  42. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: First-Order Proof Theory of Arithmetic. [REVIEW] Bulletin of Symbolic Logic 6 (4):465-466.
    Direct download  
     
    My bibliography  
     
    Export citation  
  43. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: Realizability. [REVIEW] Bulletin of Symbolic Logic 6 (4):470-471.
    Direct download  
     
    My bibliography  
     
    Export citation  
  44. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: Preface. [REVIEW] Bulletin of Symbolic Logic 6 (4):463-464.
    Direct download  
     
    My bibliography  
     
    Export citation  
  45. Toshiyasu Arai (2000). Review: Samuel R. Buss, Handbook of Proof Theory: Types in Logic, Mathematics and Programming. [REVIEW] Bulletin of Symbolic Logic 6 (4):476-477.
    Direct download  
     
    My bibliography  
     
    Export citation  
  46. Toshiyasu Arai (2000). Troelstra AS. Realizability. Handbook of Proof Theory, Edited by Buss Samuel R., Studies in Logic and the Foundations of Mathematics, Vol. 137, Elsevier, Amsterdam Etc. 1998, Pp. 407–473. [REVIEW] Bulletin of Symbolic Logic 6 (4):470-471.
    Direct download  
     
    My bibliography  
     
    Export citation  
  47. G. Japaridze, D. De Jongh & Toshiyasu Arai (2000). REVIEWS-The Logic of Provability. Bulletin of Symbolic Logic 6 (4):472-472.
     
    My bibliography  
     
    Export citation  
  48. A. Troelstra & Toshiyasu Arai (2000). REVIEWS-Realizability. Bulletin of Symbolic Logic 6 (4):470-471.
     
    My bibliography  
     
    Export citation  
  49. Toshiyasu Arai (1998). Consistency Proof Via Pointwise Induction. Archive for Mathematical Logic 37 (3):149-165.
    We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down $\alpha\mapsto\alpha [1]$ in ordinals. Also a generalization to theories $ID_q$ of finitely iterated inductive definitions is proved.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  50. Toshiyasu Arai (1998). Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection. Annals of Pure and Applied Logic 95 (1-3):93-184.
    We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 53